An efficient state space generation for analysis of real-time systems

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. In this paper, we present an algorithm that produces a compact representation of reachable state space of a real-time system. The algorithm yields a small state space, but still retains enough timing information for analysis. To avoid the state explosion which can be caused by simply adding time values to states, our algorithm first uses history equivalence and transition bisimulation to collapse states into equivalent classes. In this approach, equivalent states have identical observable events although transitions into the states may happen at different times. The algorithm then augments the resultant state space with timing relations that describe time distances between transition executions. For example, the relation @(tr1) + 3 ≤ @(tr2) ≤ @(tr1) + 5 means that transition tr2 is taken 3 to 5 time units before transition tr2 is taken. This is used to analyze timing properties such as minimum and maximum time distances between events. To show the effectiveness of our algorithm, we have implemented the algorithm and are currently comparing it to other existing techniques which generate state space for real-time systems.

REFERENCES

• 1: R Alur, C. Courcoubetis, and D. Dill. Model Checking for Real4ime Systems. In Proc. of lEEE Symposium on Logic in Computer Science, 1990.
• 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. In Proc. of lEEE Real-Time Systems Symposium, 1992.
• 3: Rajeev Alur , Costas Courcoubetis , Nicolas Halbwachs , David L. Dill , Howard Wong-Toi, Minimization of Timed Transition Systems, Proceedings of the Third International Conference on Concurrency Theory, p.340-354, August 24-27, 1992
• 4: Duncan Clarke, Insup Lee, and Hong-Liang Xie. VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems. Journal of Computer and Software Engineering, 3(2), April 1995.
• 5: W.M. Elseaidy, R. Cleaveland, and J.W. Baugh Jr. Verifying an Intelligent Structural Control System: A Case Study. In Proc. of IEEE Real-Time Systems Symposium, 1994.
• 6: C. L. Heitmeyer , R. D. Jeffords , B. G. Labaw, Comparing different approaches for specifying and verifying real-time systems, Proceedings of the tenth IEEE workshop on Real-time operating systems and software, p.122-129, March 1993, New York, New York, United States
• 7: Thomas A. Henzinger , Pei Ho , Howard Wong-Toi, A User Guide to HyTech, Cornell University, Ithaca, NY, 1995
• 8: F. Jahanian and D. A. Stuart. A Method for Verifying Properties of Modechart Specifications. In Proc. oflEEE Real-Time Systems Symposium, 1988.
• 9: Inhye Kang, Real-time system analysis based on state-space exploration, University of Pennsylvania, Philadelphia, PA, 1997
• 10: Inhye Kang and Insup Lee. State Minimization for Concurrent System Analysis Based on State Space Exploration. In Proceedings of Conference on Computer Assurance, June 1994.
• 11: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 12: Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Compiling Real-Time Specifications into Extended Automata, IEEE Transactions on Software Engineering, v.18 n.9, p.794-804, September 1992 [doi>10.1109/32.159837]
• 13: J. S. Ostroff, Deciding Properties of Timed Transition Models, IEEE Transactions on Parallel and Distributed Systems, v.1 n.2, p.170-183, April 1990 [doi>10.1109/71.80145]
• 14: Alan C. Shaw, Communicating Real-Time State Machines, IEEE Transactions on Software Engineering, v.18 n.9, p.805-816, September 1992 [doi>10.1109/32.159840]
• 15: Mihalis Yannakakis , David Lee, An Efficient Algorithm for Minimizing Real-time Transition Systems, Proceedings of the 5th International Conference on Computer Aided Verification, p.210-224, June 28-July 01, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools

General Terms:
Algorithms, Design, Experimentation, Management, Theory