This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Efficient and User-Friendly Verification
January 2002 (vol. 51 no. 1)
pp. 61-83

A compositional verification method from a high-level resource-management standpoint is presented for dense-time concurrent systems and implemented in the tool of SGM (State-Graph Manipulators) with graphical user interface. SGM packages sophisticated verification technology into state-graph manipulators and provides a user interface which views state-graphs as basic data-objects. Hence, users do not have to be verification theory experts and do not have to trace inside state-graphs to analyze state and path properties to make the best use of verification theory. Instead, users can construct their own verification strategies based on observation on the state-graph complexity changes after experimenting with some combinations of manipulators. Moreover, SGM allows users to control the complexity of state-graphs through iterative state-graphs merging and reductions before they become out of control. Reduction techniques specially designed for the context of state-graph iteration composition and shared variable manipulations are developed and used in SGM. Experiments on different benchmarks to show SGM performance are reported. An algorithm based on group theory to pick a manipulator combination is presented.

[1] M. Abadi and L. Lamport, “An Old-Fashioned Recipe for Real Time,” Proc. REX Workshop, Real-Time Theory in Practice, pp. 1-27, June 1991.
[2] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, “An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness,” Proc. IEEE Int'l Conf. Real-Time Systems Symp. (RTSS '92), 1992.
[3] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[4] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” Proc. IEEE Real-Time Systems Symp., 1993.
[5] F. Balarin, “Approximate Reachability Analysis of Timed Automata,” Proc. Real-Time Systems Symp. (RTSS '96), pp. 52-61, Dec. 1996.
[6] F. Balarin, K. Petty, A.L. Sangiovanni-Vincentelli, and P. Varaiya, “Formal Verification of the PATHO Real-Time Operating System,” Procs. 33rd Conf. Decision and Control (CDC '94), Dec. 1994.
[7] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Y. Wang, and C. Weise, “New Generation of UPPAAL,” Proc. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[8] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[9] A. Cimatti, F. Clarke, E. Giunchiglia, and M. Roveri, “NuSmv: A Reimplementation of Smv,” Proc. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[10] E. Clarke, O. Grumberg, M. Minea, and D. Peled, “State-Space Reduction Using Partial-Ordering Techniques,“ Int'l J. Software Tools for Technology, vol. 2, no. 3, pp. 279-287, 1999.
[11] 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.
[12] C. Daws and S. Yovine, “Reducing the Number of Clock Variables of Timed Automata,” Proc. Real-Time Systems Symp., pp. 73-81, Dec. 1996.
[13] A.J. Dill, D.L. Drexler, A.J. Hu, and C.H. Yang, “Protocol Verification as a Hardware Design Aid,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors, 1992.
[14] D. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,” Proc. Int'l Conf. Computer-Aided Verification, 1989.
[15] E.A. Emerson and A.P. Sistla, “Utilizing Symmetry When Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach,” ACM Trans. Programming Languages and Systems, vol. 19, no. 4, pp. 617-638, July 1997.
[16] J.C. Fernandez, “Aldebaran: A Tool for Verification of Communicating Processes,” Technical Report Spectre C14, LGI-IMAG Gre noble, 1989.
[17] J.-C. Fernandez and L. Mounier, “On the Fly Verification of Behavioral Equivalences and Preorders,” Proc. Third Int'l. Workshop Computer-Aided Verification, July 1991.
[18] P. Godefroid and D. Pirottin, “Refining Dependencies Improves Partial-Order Verification Methods,” Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 438-449, June 1993.
[19] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real-Time Systems,” Proc. IEEE Logics in Computer Science, 1992.
[20] I.N. Herstein, Topics in Algebra, second ed. Lexington, Mass.: Xerox College Publishing, 1975.
[21] K. Hoffman and R. Kunze, Linear Algebra, second ed. Englewood Cliffs, N.J.: Prentice Hall, 1971.
[22] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[23] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[24] P.-A. Hsiung and F. Wang, “A State-Graph Manipulator Tools for Real-Time System Specification and Verification,” Proc. Int'l Conf. Real-Time Computing Systems and Applications (RTCSA '98), 1998.
[25] P.-A. Hsiung and F. Wang, “User-Friendly Verification,” Proc. 1999 Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols/Protocol Specification, Testing, and Verification (FORTE/PSTV) J. Wu, S.T. Chanson, Q. Gao, eds., Oct. 1999.
[26] IEEE, ANSI/IEEE 802.3, ISO/DIS 8802/3, IEEE CS Press, 1985.
[27] C.N. Ip and D.L. Dill, “Better Verification through Symmetry,” Formal Methods in System Design, vol. 9, 1996.
[28] L. Lamport, “A Fast Mutual Exclusion Algorithm,” ACM Trans. Computer Systems, vol. 5, no. 1, pp. 1–11, 1987.
[29] F. Laroussine and K.G. Larsen, “Compositional Model Checking of Real Time Systems,” Proc. Sixth Int'l Conf. Concurrency Theory (CONCUR '95), pp. 27-41, Aug. 1995.
[30] F. Larsen, K. Larsson, P. Petterson, and Y. Wang, “Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction,” Proc. Int'l Real-Time Systems Symp. (RTSS '97), 1997.
[31] K.G. Larsen, P. Petterson, and W. Yi, “Compositional and Symbolic Model-Checking of Real-Time Systems,” Proc. 16th IEEE Real-Time Systems Symp., pp. 76-87, Dec. 1995.
[32] K.G. Larsen, B. Steffen, and C. Weise, “Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints,” Hybrid System III, pp. 604-615, 1996.
[33] R. Mateescu and H. Garavel, “XTL: A Meta-Language and Tool for Temporal Logic Model-Checking,” Procs. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[34] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[35] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[36] H. Miller and S. Katz, “Saving Space by Fully Exploiting Invisible Transitions,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.
[37] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794-804, Sept. 1992.
[38] K. Petty, “The PATHO Operating System and User's Guide,” technical report, Univ. of California, Berkeley, 1993.
[39] A. Tanenbaum, Computer Networks. Prentice Hall, 1988.
[40] S. Tripakis and S. Yovine, “Analysis of Timed Systems Based on Time-Abstracting Bisimulations,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.
[41] F. Wang and P.-A. Hsiung, “Automatic Verification on the Large,” Proc. Third IEEE Int'l Symp. High Assurance Systems Eng. (HASE), Nov. 1998.

Index Terms:
Verification, compositional verification, model-checking, real-time systems, timed automata, formal methods, software engineering.
Citation:
Farn Wang, Pao-Ann Hsiung, "Efficient and User-Friendly Verification," IEEE Transactions on Computers, vol. 51, no. 1, pp. 61-83, Jan. 2002, doi:10.1109/12.980017
Usage of this product signifies your acceptance of the Terms of Use.