
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jeffrey J.P. Tsai, Eric Y.T. Juan, Avinash Sahay, "Model and Algorithm for Efficient Verification of HighAssurance Properties of RealTime Systems," IEEE Transactions on Knowledge and Data Engineering, vol. 15, no. 2, pp. 405422, March/April, 2003.  
BibTex  x  
@article{ 10.1109/TKDE.2003.1185842, author = {Jeffrey J.P. Tsai and Eric Y.T. Juan and Avinash Sahay}, title = {Model and Algorithm for Efficient Verification of HighAssurance Properties of RealTime Systems}, journal ={IEEE Transactions on Knowledge and Data Engineering}, volume = {15}, number = {2}, issn = {10414347}, year = {2003}, pages = {405422}, doi = {http://doi.ieeecomputersociety.org/10.1109/TKDE.2003.1185842}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Knowledge and Data Engineering TI  Model and Algorithm for Efficient Verification of HighAssurance Properties of RealTime Systems IS  2 SN  10414347 SP405 EP422 EPD  405422 A1  Jeffrey J.P. Tsai, A1  Eric Y.T. Juan, A1  Avinash Sahay, PY  2003 KW  Composition verification KW  state space explosion KW  timed automata KW  labeled transition systems KW  IOtraces KW  IOTfailures KW  IOTstates KW  state space condensation. VL  15 JA  IEEE Transactions on Knowledge and Data Engineering ER   
Abstract—In this paper, we present a new compositional verification methodology for efficiently verifying highassurance properties such as reachability and deadlock freedom of realtime systems. In this methodology, each component of realtime 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 statespace graph which is formalized as a new statespace 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 IOTfailure equivalence and IOTstate equivalence. To show the performance of our methodology, we developed a verification tool RTIOTA and carried out experiments on some benchmarks such as CSMA/CD protocol, a railroad crossing, an alternating bitprotocol, etc. Specifically, we look at the time taken to generate the statespace, 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 stateexplosion problem.
[1] R. Alur, C. Courcoubetis, and D. Dill, "ModelChecking in Dense RealTime," Information and Computation, pp. 234, vol. 104, 1993.
[2] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183235, 1994.
[3] K. Bartlett, R. Scantlebury, and P. Wilkinson, "A Note on Reliable FullDuplex Transmission over HalfDuplex Links," Comm. ACM, vol. 12, no. 5, pp. 260261, 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. 4565, 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. 259303, Mar. 1994.
[6] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “UPPAAL: A ToolSuite for Automatic Verification of RealTime 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. 77121, 1985.
[8] O. Bernholtz, M.Y. Vardi, and P. Wolper, “An AutomataTheorectic Approach to BranchingTime Model Checking,” Computer Aided Verification, pp. 142155, 1994.
[9] G. Berthelot, "Checking Properties of Nets Using Transformations," Advances in Petri Nets, vol. 222, Lecture Notes in Computer Science, pp. 1940. SpringerVerlag, 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. 111126, 1991.
[11] E. Brinksma and T. Bolognesi, "Introduction to the ISO Specification Language LOTOS," Computer Networks and ISDN Systems, vol. 14, pp. 2559, 1987.
[12] A. Bouajjani, J. Fernandez, and N. Halbwachs, “Minimal Model Generation,” Proc. The Second Workshop ComputerAided 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 ComputerAided Verification, 1997.
[14] G. Bucci and E. Vicario, “Compositional Validation of TimeCritical 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. 7998, 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. 5160,New York: ACM Press, June 1993.
[18] J.A. Feldman, “A Programming Methodology for Distributed Computing (Among Other Things),” Comm. ACM, vol. 22, pp. 353368, 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 PetriNetBased 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 RealTime Systems Using Delay Time Petri Nets,” IEEE Trans. Software Eng., vol. 27, no. 5, pp. 422448, May 2001.
[22] E.Y.T. Juan and J.J.P. Tsai, Compositional Verification of Concurrent and RealTime Systems. Kluwer Academic, 2002.
[23] I. Kang and I. Lee, “An Efficient State Space Generation for Analysis of RealTime Systems,” Proc. Int'l Symp. Software Testing and Analysis, 1996.
[24] L. Lamport, “What Good is Temporal Logic?” Information Processing, pp. 657668, 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. 137151, 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. 517521.
[28] A.U. Shankar and S.S. Lam, “Distributed Computing,” TimeDependent Distributed Systems: Proving Safety, Liveliness and RealTime Properties, pp. 6179, 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 LongLived Software Systems,” IBM J. Research and Development, vol. 28, pp. 5259, 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. 141150, 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 ComputerAided 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 RealTime 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 RealTime System Specification,” IEEE Trans. Software Eng., vol. 21, no. 1, pp. 3249, Jan. 1995.
[38] J.J.P. Tsai, ”Dependability of Artificial Intelligence Systems,” IEEE Trans. Knowledge and Data Eng., vol. 7, no. 1, pp. 13, Feb. 1995.
[39] J.J.P. Tsai, Y. Bi, S.J.H. Yang, and R.A.W. Smith, Distributed RealTime 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. 8899, Mar. 1996.
[41] J.J.P. Tsai and E.Y.T. Juan, “Modeling and Verification of HighAssurance Properties of SafetyCritical Systems,” The Computer J., vol. 44, no. 6, pp. 504530, 2001.
[42] A. Valmari, "Compositional Analysis With PlaceBordered Subnets," Proc. 15th Int'l Conf. Application and Theory of Petri Nets, pp. 531547, 1994.
[43] A. Valmari, "The Weakest DeadlockPreserving Congruence," Information Processing Letters, pp. 341346, vol. 53, 1995.
[44] M.Y. Vardi and P. Wolper, “An AutomataTheoretic Approach to Automatic Program Verification,” Proc. First Symp. Logic in Computer Science, pp. 322331, 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. 523531, vol. 23, no. 2, Mar. 1993.