This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Efficient State Space Generation for the Analysis of Real-Time Systems
May 2000 (vol. 26 no. 5)
pp. 453-477

Abstract—State explosion is a well-known problem that impedes analysis and testing based on state-space exploration. This problem is particularly serious in real-time systems because unbounded time values cause the state space to be infinite even for simple systems. In this paper, we present an algorithm that produces a compact representation of the reachable state space of a real-time system. The algorithm yields a small state space, but still retains enough information for analysis. To avoid the state explosion which can be caused by simply adding time values to states, our algorithm uses history equivalence and transition bisimulation to collapse states into equivalent classes. Through history equivalence, states are merged into an equivalence class with the same untimed executions up to the states. Using transition bisimulation, the states that have the same future behaviors are further collapsed. The resultant state space is finite and can be used to analyze real-time properties. To show the effectiveness of our algorithm, we have implemented the algorithm and have analyzed several example applications.

[1] R. Alur, “Techniques for Automatic Verification of Real-Time Systems,” PhD dissertation, Department of Computer Science, Stanford Univ., Aug. 1991.
[2] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[3] 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.
[4] R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi, “Minimization of Timed Transition Systems,” Proc. Int'l Conf. Concurrency Theory, vol. 630, Aug. 1992.
[5] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[6] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[7] 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.
[8] A. Bouajjani, J.-C. Fernandez, N. Halbwachs, and P. Raymond, “Minimal State Graph Generation,” Science of Computer Programming, vol. 18, pp. 247–269 1992.
[9] D. Clarke, I. Lee, and H.-L. Xie, “VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems,” J. Computer and Software Eng., vol. 3, no. 2, Apr. 1995.
[10] C. Draws, A. Olivero, and S. Yovine, “Verifying ET-LOTOS Programs with KRONOS,” Proc. Seventh Int'l Conf. Formal Description Techniques, 1994.
[11] C. Draws and S. Yovine, “Two Examples of Verification of Multirate Timed Automata with KRONOS,” Proc. IEEE Real-Time Systems Symp., Dec. 1995.
[12] 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.
[13] C. Heitmeyer, R. Jeffords, and B. Labaw, “Comparing Different Approaches for Specifying and Verifying Real-Time Systems,” Proc. Tenth IEEE Workshop Real-Time Operating Systems and Software, May 1993.
[14] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for Real-Time Systems," Information and Computation, vol. 111, no. 2, 1994.
[15] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "A User Guide to HyTech," Technical Report CSD-TR-95-1532, Department of Computer Science, Cornell Univ., 1995.
[16] ——,“A graph-theoretic approach for timing analysis and its implementation,”IEEE Trans. Comput., vol. C-36, pp. 961–975, Aug. 1987.
[17] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. IEEE Real-Time Systems Symposium, 1988.
[18] I. Kang, “Real-Time System Analysis based on State-Space Exploration,” PhD dissertation, May 1997.
[19] I. Kang and I. Lee, “State Minimization for Concurrent System Analysis Based on State Space Exploration,” Proc. Conf. Computer Assurance, June 1994.
[20] L. Lamport, “A Fast Mutual Exclusion Algorithm,” ACM Trans. Computer Systems, vol. 5, no. 1, pp. 1–11, 1987.
[21] K.G. Larsen, P. Petterson, and W. Yi, “Model-Checking for Real-time Systems,” Proc. Conf. Fundamentals of Computation Theory, 1995.
[22] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[23] 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.
[24] J.S. Ostroff, “Deciding properties of Timed Transition Models,” IEEE Trans. Paralel and Distributed Systems, vol. 1, no. 2, Apr. 1990.
[25] Z. Prucz, T.T. Soong, and A. Reinhorn, “An Analysis of Pulse Control for Simple Mechanical Systems,” Dynamic Systems, Measurement, and Control, vol. 107, pp. 123–131, Jun. 1985.
[26] S.C.V. Raju, “An automatic Verification Technique for Communicating Real-Time State Machines,” Technical Report 93-04-08, Univ. of Washington, April 1993.
[27] A.C. Shaw, "Communicating Real-Time State Machines," IEEE Trans. Software Eng., Sept. 1992, pp. 805-816.
[28] O. Sokolsky and S. A. Smolka, “Local Model Checking for Real-Time Systems,” Proc. Conf. Computer-Aided Verification, 1995.
[29] M. Yannakakis and D. Lee, “An Efficient Algorithm for Minimizing Real-time Transition Systems,” Proc. Workshop Computer-Aided Verification, 1993.
[30] W. Yi, P. Petterson, and M. Daniels, “Automatic Verification of Real-Time Systems by Constraint Solving,” Proc. Seventh Int'l Conf. Formal Description Techniques, 1994.

Index Terms:
Formal specification, reachability analysis, real-time systems analysis, state space minimization, timed automata.
Citation:
Inhye Kang, Insup Lee, Young-Si Kim, "An Efficient State Space Generation for the Analysis of Real-Time Systems," IEEE Transactions on Software Engineering, vol. 26, no. 5, pp. 453-477, May 2000, doi:10.1109/32.846302
Usage of this product signifies your acceptance of the Terms of Use.