Classification schemes to aid in the analysis of real-time systems

ABSTRACT

This paper presents three sets of classification schemes for processes, properties, and transitions that can be used to assist in the analysis of real-time systems. These classification schemes are discussed in the context of ASTRAL, which is a formal specification language for real-time systems. Eight testbed systems were specified in ASTRAL, and their proofs were performed to determine proof patterns that occur most often. The specifications were then examined in an attempt to derive specific characteristics that could be used to statically identify each pattern within a specification. Once the classifications were obtained, they were then used to provide systematic guidance for analyzing real-time systems by directing the prover to the proof techniques most applicable to each proof pattern. This paper presents the set of classification schemes that were developed and discusses how they can be used to assist the proof process.

REFERENCES

• 1: Alex Borgida , John Mylopoulos , Raymond Reiter, On the Frame Problem in Procedure Specifications, IEEE Transactions on Software Engineering, v.21 n.10, p.785-798, October 1995 [doi>10.1109/32.469460]
• 2: Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997 [doi>10.1109/32.629494]
• 3: Crow, J., S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS", Proc. Workshop on Industrial-Strength Formal Specification Techniques, (Apr., 1995).
• 4: Thomas R. Dean , James R. Cordy, A Syntactic Theory of Software Architecture, IEEE Transactions on Software Engineering, v.21 n.4, p.302-313, April 1995 [doi>10.1109/32.385969]
• 5: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 6: Robert E. Filman , Daniel P. Friedman, Coordinated computing: tools and techniques for distributed software, McGraw-Hill, Inc., New York, NY, 1984
• 7: Heitmeyer, C. and N. Lynch, "The Generalized Railroad Crossing: a Case Study in Formal Verification of Real-Time Systems", Proc. 15th Real-Time Systems Symposium, 120- 131 (Dec., 1994).
• 8: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, Temporal proof methodologies for timed transition systems, Information and Computation, v.112 n.2, p.273-337, Aug 1 1994 [doi>10.1006/inco.1994.1060]
• 9: Paul Z. Kolano, The ASTRAL Specifications of 8 Real-Time Systems, University of California at Santa Barbara, Santa Barbara, CA, 1999
• 10: Paul Z. Kolano, Proof Assistance for Real-Time Systems Using an Interactive Theorem Prover, Proceedings of the 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, p.315-333, May 26-28, 1999
• 11: Paul Zachary Kolano , Richard Kemmerer, Tools and techniques for the design and systematic analysis of real-time systems, 1999
• 12: Paul Z. Kolano , Zhe Dang , Richard A. Kemmerer, The design and analysis of real-time systems using the ASTRAL software development environment, Annals of Software Engineering, v.7 n.1-4, p.177-210, 1999 [doi>10.1023/A:1018934104631]
• 13: Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
• 14: Formal Development of Reactive Systems - Case Study Production Cell, January 1995
• 15: Nancy A. Lynch , Frits W. Vaandrager, Forward and Backward Simulations for Timing-Based Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.397-446, June 03-07, 1991
• 16: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 17: Official 1996 Olympic Web Site, http://www.atlanta.olympic.org (1996).
• 18: Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
• 19: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 20: Paul T. Ward , Stephen J. Mellor, Structured Development for Real-Time Systems, Prentice Hall Professional Technical Reference, 1991

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.5 PATTERN RECOGNITION
      I.5.2 Design Methodology
          Subjects: Classifier design and evaluation

Additional Classification:
  C. Computer Systems Organization

  D. Software
  D.2 SOFTWARE ENGINEERING
  D.4 OPERATING SYSTEMS
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

General Terms:
Design, Measurement, Performance, Theory

Keywords:
ASTRAL, analysis guidance, formal methods, formal specification and verification, real-time systems, system classification, timing requirements