IIIT Hyderabad Publications |
|||||||||
|
Verifying Timed CTL Contracts for Continuous Pure Signal I/O Automata by encoding as Virtual EnvironmentsAuthors: Santosh Arvind Adimoolam,Venkatesh Choppella, PVR Murthy Date: 2013-07-07 Report no: IIIT/TR/2013/26 AbstractIn components that react to continuous time pure signals, timing constraints about input signals can succinctly be expressed in Timed Computational Tree Logic (TCTL). We prove that a class of Timed CTL assume-guarantee pairs, where the assumptions are timed constraints about continuous signals, can be veried by processing the gurantees as queries on certian timed automata encodings of the assumptions. We call the timed automata encoding of an assumption as Virtual environment (VE). The class of guarantees encompass all safety properties and some time bounded liveness properties. We define Continuous Signal Input-Output Automata (CPSIOA), a class of timed automata and a subset of hybrid input-output automata, for modeling components that react to continuous time pure signals. The class of TCTL assume-guarantee pairs are used as interface contracts among CPSIOA component models. Full report: pdf Centre for Software Engineering Research Lab |
||||||||
Copyright © 2009 - IIIT Hyderabad. All Rights Reserved. |