IIIT Hyderabad Publications |
|||||||||
|
Employing Timed CTL assumptions in modular verication of invariant properties of real time component based systemsAuthors: Santosh Arvind Adimoolam,Venkatesh Choppella, PVR Murthy Date: 2013-11-11 Report no: IIIT/TR/2013/42 AbstractThe extant assume-guarantee approaches for real time systems use timed language or equivalently timed automata based specifications of assumptions. But discharging timed automata assumptions on environment models requires simulation-checking. On the other hand, discharging an assumption in Timed Computational Tree Logic (TCTL) can be done by processing the assumption as a model-checking query on the environment timed automaton. The region-explosion problem is encountered in both simulation-checking and TCTL model checking. But, while efficient tool support is there for countering region-explosion in TCTL model checking, there is no efficient tool support for the same in case of simulation checking. Therefore, in this paper we present a method for employing TCTL assumptions in modular assume-guarantee verification of invariant properties of real-time component based systems. So as to accommodate TCTL assume-guarantees, we instantiate boolean input and output variables for timed automata representing a continuous pure signal interface.We also address complexity issues arising by instantiating boolean input-output variables. This paper only deals with invariant guarantees (like safety guarantees), with the hope of extending it to liveness guarantees in case of bounded response systems. Full report: pdf Centre for Software Engineering Research Lab |
||||||||
Copyright © 2009 - IIIT Hyderabad. All Rights Reserved. |