Issue No.02 - March/April (2003 vol.15)
Jeffrey J.P. Tsai , IEEE
<p><b>Abstract</b>—In this paper, we present a new compositional verification methodology for efficiently verifying high-assurance properties such as reachability and deadlock freedom of real-time systems. In this methodology, each component of real-time systems is initially specified as a timed automaton and it communicates with other components via synchronous and/or asynchronous communication channels. Then, each component is analyzed by a generation of its state-space graph which is formalized as a new state-space representation model called Multiset Labeled Transition Systems (MLTSs). Afterward, the state spaces of the components are hierarchically composed and simplified through a composition algorithm and a set of condensation rules, respectively, to get a condensed state space of the system. The simplified state spaces preserve equivalence with respect to deadlock and reachable states. Such equivalence is assured by our reduction theories called IOT-failure equivalence and IOT-state equivalence. To show the performance of our methodology, we developed a verification tool RT-IOTA and carried out experiments on some benchmarks such as CSMA/CD protocol, a rail-road crossing, an alternating bit-protocol, etc. Specifically, we look at the time taken to generate the state-space, the size of the state space, and the amount of reduction achieved by our condensation rules. The results demonstrate the strength of our new technique in dealing with the state-explosion problem.</p>
Composition verification, state space explosion, timed automata, labeled transition systems, IO-traces, IOT-failures, IOT-states, state space condensation.
Jeffrey J.P. Tsai, Eric Y.T. Juan, Avinash Sahay, "Model and Algorithm for Efficient Verification of High-Assurance Properties of Real-Time Systems", IEEE Transactions on Knowledge & Data Engineering, vol.15, no. 2, pp. 405-422, March/April 2003, doi:10.1109/TKDE.2003.1185842