
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Douglas A. Stuart, Monica Brockmeyer, Aloysius K. Mok, Farnam Jahanian, "SimulationVerification: Biting at the State Explosion Problem," IEEE Transactions on Software Engineering, vol. 27, no. 7, pp. 599617, July, 2001.  
BibTex  x  
@article{ 10.1109/32.935853, author = {Douglas A. Stuart and Monica Brockmeyer and Aloysius K. Mok and Farnam Jahanian}, title = {SimulationVerification: Biting at the State Explosion Problem}, journal ={IEEE Transactions on Software Engineering}, volume = {27}, number = {7}, issn = {00985589}, year = {2001}, pages = {599617}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.935853}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  SimulationVerification: Biting at the State Explosion Problem IS  7 SN  00985589 SP599 EP617 EPD  599617 A1  Douglas A. Stuart, A1  Monica Brockmeyer, A1  Aloysius K. Mok, A1  Farnam Jahanian, PY  2001 KW  Realtime systems KW  formal methods KW  specification KW  verification KW  timing constraints KW  Modechart KW  requirements analysis KW  simulation. VL  27 JA  IEEE Transactions on Software Engineering ER   
Abstract—Simulation and verification are the two conventional techniques for the analysis of specifications of realtime 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 statespace explosion problem. In this paper, we introduce a new technique: Simulationverification 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 simulationverification graph, can be one or more orders of magnitude smaller than the full computation graph. A tool, XSVT, is described which implements simulationverification 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, “ModelChecking for RealTime Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[2] R. Alur and D.L. Dill,“The theory of timed automata,” RealTime: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 2873. SpringerVerlag, 1991.
[3] R. Alur, T.A. Henzinger, and P.H. Ho, “Automatic Symbolic Verification of Embedded Systems,” Proc. IEEE RealTime Systems Symp., 1993.
[4] H. BenAbdallah, I. Lee, and J.Y. Choi, “A Graphical Language with Formal Semantics for the Specification and Analysis of RealTime Systems,” Proc. IEEE RealTime Systems Symp., pp. 276286, 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 FiniteState RealTime Systems,” Proc. IEEE RealTime Systems Symp., pp. 276286, 1994.
[7] D. Clarke, I. Lee, and H. Xie, “Versa: A Tool for the Specification and Analysis of ResourceBound RealTime Systems,” Technical Report MSCIS9377, Univ. of Pennsylvania, Dept. of Computer and Information Science, Sept. 1993.
[8] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A SemanticsBased Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 3672.
[9] P.C. Clements, C.L. Heitmeyer, B.G. Labaw, and A.T. Rose, “MT: A Toolset for Specifying and Analyzing RealTime Systems,” Proc. IEEE RealTime Systems Symp., Dec. 1993.
[10] P. Clements, “Requirements Definition Languages for RealTime 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 PB93178556/AS, Technical Report 5546939581, US Naval Research Laboratory, Washington, DC; Technical Report Info04741, 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 PB93178564/AS, Technical Report 5546939582, US Naval Research Laboratory, Washington, DC; Technical Report Info04742, 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 RealTime Systems Symp., pp. 271275, Dec. 1994.
[14] E. Emerson, A. Mok, A. Sistla, and J. Srinivasan, “Quantitative Temporal Reasoning,” Workshop Automatic Verification of Finitestate 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 ResourceBased Prioritized Bisimulation for RealTime Systems,” Technical Report MSCIS9069, 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. 2128.
[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. WongToi, "HyTech: The Next Generation," Proc. RealTime 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 RealTime Systems,” PhD thesis, Eindhoven Univ. of Tech nology, 1991.
[23] F. Jahanian and A.K. Mok, “Modechart: A Specification Language for RealTime Systems,” IEEE Trans. Software Eng., vol. 20, no. 10, Oct. 1994.
[24] F. Jahanian and A.K. Mok, “Modechart: A Specification Language for RealTime 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 RealTime Systems Symp., pp. 1221, Dec. 1988.
[26] F. Jahanian and A. K.L. Mok,“Safety analysis of timing properties in realtime systems,”IEEE Trans. Software Eng., vol. SE12, 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émondGrégoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of ResourceBound RealTime Systems,” Technical Report MSCIS9308, Jan. 1993.
[29] N. Lynch and H. Attiya, “Using Mappings to Prove Timing Properties,” Distributed Computing, vol. 6, no. 2, pp. 121139, 1992.
[30] D. Mandrioli, S. Morasca, and A. Morzenti, “Generating Test Cases for RealTime Systems from Logic Specifications,” ACM Trans. Computer Systems, vol. 13, no. 4, pp. 365398, Nov. 1995.
[31] Z. Manna, O. Maler, and A. Pnueli, “The Theory of Timed Automata,” Proc. REX Workshop RealTime: Theory in Practice, June 1991.
[32] J. Ostroff, Temporal Logic for RealTime 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. 249261, June 1988.
[36] A. Rose, M. Perez, and P. Clements, “Modechart Toolset User's Guide,” Technical Report NRL/MRL/5540947427, Center for Computer High Assurance Systems, Naval Research Lab, Washington, D.C., Feb. 1994.
[37] D. Stuart, “Implementing a Verifier for RealTime Systems,” Proc. RealTime Systems Symp., pp. 6271, Dec. 1990.
[38] D.A. Stuart, “Formal Methods for RealTime Systems,” PhD thesis, The Univ. of Texas at Austin, 1996.