
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Inhye Kang, Insup Lee, YoungSi Kim, "An Efficient State Space Generation for the Analysis of RealTime Systems," IEEE Transactions on Software Engineering, vol. 26, no. 5, pp. 453477, May, 2000.  
BibTex  x  
@article{ 10.1109/32.846302, author = {Inhye Kang and Insup Lee and YoungSi Kim}, title = {An Efficient State Space Generation for the Analysis of RealTime Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {26}, number = {5}, issn = {00985589}, year = {2000}, pages = {453477}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.846302}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  An Efficient State Space Generation for the Analysis of RealTime Systems IS  5 SN  00985589 SP453 EP477 EPD  453477 A1  Inhye Kang, A1  Insup Lee, A1  YoungSi Kim, PY  2000 KW  Formal specification KW  reachability analysis KW  realtime systems analysis KW  state space minimization KW  timed automata. VL  26 JA  IEEE Transactions on Software Engineering ER   
Abstract—State explosion is a wellknown problem that impedes analysis and testing based on statespace exploration. This problem is particularly serious in realtime 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 realtime 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 realtime 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 RealTime Systems,” PhD dissertation, Department of Computer Science, Stanford Univ., Aug. 1991.
[2] R. Alur, C. Courcoubetis, and D. Dill, “ModelChecking for RealTime Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[3] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. WongToi, “An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness,” Proc. IEEE Int'l Conf. RealTime Systems Symp. (RTSS '92), 1992.
[4] R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. WongToi, “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. 334, 1995.
[6] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183235, 1994.
[7] 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.
[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 ResourceBound RealTime Systems,” J. Computer and Software Eng., vol. 3, no. 2, Apr. 1995.
[10] C. Draws, A. Olivero, and S. Yovine, “Verifying ETLOTOS 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 RealTime 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 RealTime Systems Symp., pp. 271275, Dec. 1994.
[13] C. Heitmeyer, R. Jeffords, and B. Labaw, “Comparing Different Approaches for Specifying and Verifying RealTime Systems,” Proc. Tenth IEEE Workshop RealTime Operating Systems and Software, May 1993.
[14] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for RealTime Systems," Information and Computation, vol. 111, no. 2, 1994.
[15] T.A. Henzinger, P.H. Ho, and H. WongToi, "A User Guide to HyTech," Technical Report CSDTR951532, Department of Computer Science, Cornell Univ., 1995.
[16] ——,“A graphtheoretic approach for timing analysis and its implementation,”IEEE Trans. Comput., vol. C36, pp. 961–975, Aug. 1987.
[17] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. IEEE RealTime Systems Symposium, 1988.
[18] I. Kang, “RealTime System Analysis based on StateSpace 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, “ModelChecking for Realtime Systems,” Proc. Conf. Fundamentals of Computation Theory, 1995.
[22] R. Milner, Communication and Concurrency, PrenticeHall, Englewood Cliffs, N.J., 1989.
[23] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling RealTime Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794804, 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 RealTime State Machines,” Technical Report 930408, Univ. of Washington, April 1993.
[27] A.C. Shaw, "Communicating RealTime State Machines," IEEE Trans. Software Eng., Sept. 1992, pp. 805816.
[28] O. Sokolsky and S. A. Smolka, “Local Model Checking for RealTime Systems,” Proc. Conf. ComputerAided Verification, 1995.
[29] M. Yannakakis and D. Lee, “An Efficient Algorithm for Minimizing Realtime Transition Systems,” Proc. Workshop ComputerAided Verification, 1993.
[30] W. Yi, P. Petterson, and M. Daniels, “Automatic Verification of RealTime Systems by Constraint Solving,” Proc. Seventh Int'l Conf. Formal Description Techniques, 1994.