This Article 
 Bibliographic References 
 Add to: 
Model and Algorithm for Efficient Verification of High-Assurance Properties of Real-Time Systems
March/April 2003 (vol. 15 no. 2)
pp. 405-422

Abstract—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.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-Checking in Dense Real-Time," Information and Computation, pp. 2-34, vol. 104, 1993.
[2] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[3] K. Bartlett, R. Scantlebury, and P. Wilkinson, "A Note on Reliable Full-Duplex Transmission over Half-Duplex Links," Comm. ACM, vol. 12, no. 5, pp. 260-261, May 1969.
[4] T. Basten and M. Voorhoeve, "An Algebraic Semantics for Hierarchical P/T Nets," Proc. 16th Int'l Conf. Application and Theory of Petri Nets, pp. 45-65, Lecture Notes in Computer Science 935, 1995.
[5] J. Bengt, “Compositional Specification and Verification of Distributed Systems,” ACM Trans. Programming Languages and Systems, vol. 16, no. 2, pp. 259-303, Mar. 1994.
[6] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “UPPAAL: A Tool-Suite for Automatic Verification of Real-Time Systems,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[7] J.A. Bergstra and J.W. Klop, “Algebra of Communicating Processes with Abstraction,” Theoretical Computer Science, vol. 37, no. 1, pp. 77-121, 1985.
[8] O. Bernholtz, M.Y. Vardi, and P. Wolper, “An Automata-Theorectic Approach to Branching-Time Model Checking,” Computer Aided Verification, pp. 142-155, 1994.
[9] G. Berthelot, "Checking Properties of Nets Using Transformations," Advances in Petri Nets, vol. 222, Lecture Notes in Computer Science, pp. 19-40. Springer-Verlag, 1987.
[10] F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten, “The Failure of Failures in a Paradigm for Asynchronous Communication,” Proc. Concurrency '91, pp. 111-126, 1991.
[11] E. Brinksma and T. Bolognesi, "Introduction to the ISO Specification Language LOTOS," Computer Networks and ISDN Systems, vol. 14, pp. 25-59, 1987.
[12] A. Bouajjani, J. Fernandez, and N. Halbwachs, “Minimal Model Generation,” Proc. The Second Workshop Computer-Aided Verification, 1990.
[13] M. Bozga, O. Maler, A. Pnueli, and S. Yovince, “Some Progress in the Symbolic Verification of Timed Automata,” Proc. Int'l Workshop Computer-Aided Verification, 1997.
[14] G. Bucci and E. Vicario, “Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, pp. 969–992, Dec. 1995.
[15] S. Campos, E. Clarke, and M. Minea, “Symbolic Techniques for Formally Verifying Industrial Systems,” Science of Computer Programming, vol. 29, pp. 79-98, 1997.
[16] Y. Chen, W. Tsai, and D. Chao, “Dependency Analysis—A Petri Net Based Techniques for Synthesizing Large Concurrent Systems,” IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 4, 1993.
[17] S. Duri, U. Buy, R. Devarapalli, and S.M. Shatz, "Using State Space Reduction Methods for Deadlock Analysis in Ada Tasking," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker, eds., [37], pp. 51-60,New York: ACM Press, June 1993.
[18] J.A. Feldman, “A Programming Methodology for Distributed Computing (Among Other Things),” Comm. ACM, vol. 22, pp. 353-368, 1979.
[19] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[20] E. Juan, J.J.P. Tsai, and T. Murata, "Compositional Verification of Concurrent Systems Using Petri-Net-Based Condensation Rules," ACM Trans. Programming Languages and Systems, vol. 20, no. 5, Sept. 1998.
[21] E.Y.T. Juan, J.J.P. Tsai, T. Murata, and Y. Zhou, “Reduction Methods for Real-Time Systems Using Delay Time Petri Nets,” IEEE Trans. Software Eng., vol. 27, no. 5, pp. 422-448, May 2001.
[22] E.Y.T. Juan and J.J.P. Tsai, Compositional Verification of Concurrent and Real-Time Systems. Kluwer Academic, 2002.
[23] I. Kang and I. Lee, “An Efficient State Space Generation for Analysis of Real-Time Systems,” Proc. Int'l Symp. Software Testing and Analysis, 1996.
[24] L. Lamport, “What Good is Temporal Logic?” Information Processing, pp. 657-668, 1983.
[25] L. Leonard and G. Leduc, “Revised Draft on Enhancements to LOTOS,” A Formal Definition of Time in LOTOS, 1994.
[26] N.A. Lynch and M.R. Tuttle, "Hierarchical Correctness Proofs for Distributed Algorithms," Proc. Sixth Symp. Principles of Distributed Computing, pp. 137-151, ACM, New York, 1987.
[27] R.E. Bryant, "Symbolic Simulation—Techniques and Applications," Proc. 27th ACM/IEEE Design Automation Conf. (DAC 90), IEEE Press, 1990, pp. 517-521.
[28] A.U. Shankar and S.S. Lam, “Distributed Computing,” Time-Dependent Distributed Systems: Proving Safety, Liveliness and Real-Time Properties, pp. 61-79, 1987.
[29] A.P. Sistla, L. Milliades, and V. Gyuris, “SMC: A Symmetry Based Model Checker for Verification of Liveness Properties,” Proc. CAV'97, pp. 464–467, 1998.
[30] R.E. Strom and N. Halim, “A New Programming Methodology for Long-Lived Software Systems,” IBM J. Research and Development, vol. 28, pp. 52-59, 1984.
[31] K.C. Tai and P.V. Koppol, “An Incremental Approach ro Reachability Analysis of Distributed Programs,” Proc. Seventh Int'l Workshop Software Specification and Design, pp. 141-150, 1993.
[32] A. Tanenbaum, Computer Networks. Prentice Hall, 1988.
[33] S. Tasiran, R. Alur, R.P. Kurshan, and R.K. Brayton, “Verifying Abstractions of Timed Systems,” Proc. Seventh Conf. Concurrency Theory, 1996.
[34] S. Tasiran and R. Brayton, “STARI: A Case Study in Compositional and Hierarchical Timing Verification,” Proc. Int'l Workshop Computer-Aided Verification, 1997.
[35] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[36] J. J. P. Tsai and S. J. H. Yang,Monitoring and Debugging of Distributed Real-Time Systems. Washington, DC: IEEE Computer Society Press, 1995.
[37] J.J.P. Tsai, S.J.H. Yang, and Y.H. Chang, ”Timing Constraint Petri Nets and their Application to Schedulability Analysis of Real-Time System Specification,” IEEE Trans. Software Eng., vol. 21, no. 1, pp. 32-49, Jan. 1995.
[38] J.J.P. Tsai, ”Dependability of Artificial Intelligence Systems,” IEEE Trans. Knowledge and Data Eng., vol. 7, no. 1, pp. 1-3, Feb. 1995.
[39] J.J.P. Tsai, Y. Bi, S.J.H. Yang, and R.A.W. Smith, Distributed Real-Time Systems: Monitoring, Debugging, and Visualization. John Wiley and Sons, 1996.
[40] J.J.P. Tsai, Y. Bi, and S.J.H. Yang, ”Debugging for Timing Constraints Violation,” IEEE Software, pp. 88-99, Mar. 1996.
[41] J.J.P. Tsai and E.Y.T. Juan, “Modeling and Verification of High-Assurance Properties of Safety-Critical Systems,” The Computer J., vol. 44, no. 6, pp. 504-530, 2001.
[42] A. Valmari, "Compositional Analysis With Place-Bordered Subnets," Proc. 15th Int'l Conf. Application and Theory of Petri Nets, pp. 531-547, 1994.
[43] A. Valmari, "The Weakest Deadlock-Preserving Congruence," Information Processing Letters, pp. 341-346, vol. 53, 1995.
[44] M.Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” Proc. First Symp. Logic in Computer Science, pp. 322-331, 1986.
[45] M. Zhou, K. McDermott, and P.A. Patel, "Petri Net Synthesis and Analysis of a Flexible Manufacturing System Cell," IEEE Trans. Systems, Man, and Cybernetics, pp. 523-531, vol. 23, no. 2, Mar. 1993.

Index Terms:
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 and Data Engineering, vol. 15, no. 2, pp. 405-422, March-April 2003, doi:10.1109/TKDE.2003.1185842
Usage of this product signifies your acceptance of the Terms of Use.