This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Simulation-Verification: Biting at the State Explosion Problem
July 2001 (vol. 27 no. 7)
pp. 599-617

Abstract—Simulation and verification are the two conventional techniques for the analysis of specifications of real-time systems. While simulation is relatively inexpensive in terms of execution time, it only validates the behavior of a system for one particular computation path. On the other hand, verification provides guarantees over the entire set of computation paths of a system, but is, in general, very expensive due to the state-space explosion problem. In this paper, we introduce a new technique: Simulation-verification combines the best of both worlds by synthesizing an intermediate analysis method. This method uses simulation to limit the generation of a computation graph to that set of computations consistent with the simulation. This limited computation graph, called a simulation-verification graph, can be one or more orders of magnitude smaller than the full computation graph. A tool, XSVT, is described which implements simulation-verification graphs. Three paradigms for using the new technique are proposed. The paper illustrates the application of the proposed technique via an example of a robot controller for a manufacturing assembly line.

[1] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[2] R. Alur and D.L. Dill,“The theory of timed automata,” Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 28-73. Springer-Verlag, 1991.
[3] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” Proc. IEEE Real-Time Systems Symp., 1993.
[4] H. Ben-Abdallah, I. Lee, and J.-Y. Choi, “A Graphical Language with Formal Semantics for the Specification and Analysis of Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., pp. 276-286, 1995.
[5] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[6] S. Campos, E. Clarke, W. Marrero, and M. Minea, “Computing Quantitive Characteristics of Finite-State Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., pp. 276-286, 1994.
[7] D. Clarke, I. Lee, and H. Xie, “Versa: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems,” Technical Report MS-CIS-93-77, Univ. of Pennsylvania, Dept. of Computer and Information Science, Sept. 1993.
[8] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[9] P.C. Clements, C.L. Heitmeyer, B.G. Labaw, and A.T. Rose, “MT: A Toolset for Specifying and Analyzing Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., Dec. 1993.
[10] P. Clements, “Requirements Definition Languages for Real-Time Embedded Systems,” PhD thesis, The Univ. of Texas at Austin, 1993.
[11] D. Craigen, S. Gerhart, and T. Ralston, “An International Survey of Industrial Applications of Formal Methods, Volume 1 Study Methodology,” Technical Report PB93-178556/AS, Technical Report 5546-93-9581, US Naval Research Laboratory, Washington, DC; Technical Report Info-0474-1, Atomic Energy Control Board of Canada, Ontario, Nat'l Technical Information Service, Springfield, VA, 1993.
[12] D. Craigen, S. Gerhart, and T. Ralston, “An International Survey of Industrial Applications of Formal Methods, Volume 2 Case Studies,” Technical Report PB93-178564/AS, Technical Report 5546-93-9582, US Naval Research Laboratory, Washington, DC; Technical Report Info-0474-2, Atomic Energy Control Board of Canada, Ontario, Nat'l Technical Information Service, Springfield, VA, 1993.
[13] W.M. Elseaidy, R. Cleaveland, and J.W. Baugh, “Verifying an Intelligent Structural Control System: A Case Study,” Proc. IEEE Real-Time Systems Symp., pp. 271-275, Dec. 1994.
[14] E. Emerson, A. Mok, A. Sistla, and J. Srinivasan, “Quantitative Temporal Reasoning,” Workshop Automatic Verification of Finite-state Systems, 1989.
[15] R. Gerber and I. Lee, “Ccsr: A Calculus for Communicating Shared Resources,” Proc. Int'l Conf. Concurrency Theory, CONCUR '90, Aug. 1990.
[16] R. Gerber and I. Lee, “A Resource-Based Prioritized Bisimulation for Real-Time Systems,” Technical Report MS-CIS-90-69, Univ. of Pennsylvania, Dept. of Computer and Information Science, Sept. 1990.
[17]  S.L. Gerhart, D. Craigen, and T. Ralston, “Experience with Formal Methods in Critical Systems,” IEEE Software, Jan. 1994, pp. 21-28.
[18] Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, M.J.C. Gordon and T.F. Melham, eds. Cambridge Univ. Press, 1993.
[19] H. Hanson, “Time and Probability in Formal Design of Distributed Systems,” PhD thesis, Uppsala Univ., 1991.
[20] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: The Next Generation," Proc. Real-Time Systems Symp., IEEE CS Press, 1995.
[21] A.T.H. Ho, “The Modechart Tableau Simulator,” master's thesis, Univ. of Texas at Austin, 1994.
[22] J. Hooman, “Specification and Compositional Verification of Real-Time Systems,” PhD thesis, Eindhoven Univ. of Tech nology, 1991.
[23] F. Jahanian and A.K. Mok, “Modechart: A Specification Language for Real-Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 10, Oct. 1994.
[24] F. Jahanian and A.K. Mok, “Modechart: A Specification Language for Real-Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 10, Oct. 1994.
[25] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. IEEE Real-Time Systems Symp., pp. 12-21, Dec. 1988.
[26] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[27] L. Lamport, “The Temporal Logic of Actions,” Technical Report 79, Digital Systems Research Center, Dec. 1991.
[28] I. Lee and P. Brémond-Grégoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems,” Technical Report MS-CIS-93-08, Jan. 1993.
[29] N. Lynch and H. Attiya, “Using Mappings to Prove Timing Properties,” Distributed Computing, vol. 6, no. 2, pp. 121-139, 1992.
[30] D. Mandrioli, S. Morasca, and A. Morzenti, “Generating Test Cases for Real-Time Systems from Logic Specifications,” ACM Trans. Computer Systems, vol. 13, no. 4, pp. 365-398, Nov. 1995.
[31] Z. Manna, O. Maler, and A. Pnueli, “The Theory of Timed Automata,” Proc. REX Workshop Real-Time: Theory in Practice, June 1991.
[32] J. Ostroff, Temporal Logic for Real-Time Systems. John Wiley and Sons, 1989.
[33] S. Owre, N. Shankar, and J. Rushby, “User Guide for the PVS Specification and Verification System,” technical report, Computer Science Lab., SRI Int'l, Menlo Park, Calif., 1993.
[34] L.C. Paulson, “Introduction to Isabelle,” Technical Report 280, Univ. of Cambridge, Computer Laboratory, 1993.
[35] G.M. Reed and A.W. Roscoe, "A Timed Model for Communicating Sequential Processes," Theoretical Computer Science, vol. 58, pp. 249-261, June 1988.
[36] A. Rose, M. Perez, and P. Clements, “Modechart Toolset User's Guide,” Technical Report NRL/MRL/5540-94-7427, Center for Computer High Assurance Systems, Naval Research Lab, Washington, D.C., Feb. 1994.
[37] D. Stuart, “Implementing a Verifier for Real-Time Systems,” Proc. Real-Time Systems Symp., pp. 62-71, Dec. 1990.
[38] D.A. Stuart, “Formal Methods for Real-Time Systems,” PhD thesis, The Univ. of Texas at Austin, 1996.

Index Terms:
Real-time systems, formal methods, specification, verification, timing constraints, Modechart, requirements analysis, simulation.
Citation:
Douglas A. Stuart, Monica Brockmeyer, Aloysius K. Mok, Farnam Jahanian, "Simulation-Verification: Biting at the State Explosion Problem," IEEE Transactions on Software Engineering, vol. 27, no. 7, pp. 599-617, July 2001, doi:10.1109/32.935853
Usage of this product signifies your acceptance of the Terms of Use.