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

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. Keywords Formal methods, formal specification and verifi...

• Type: Conference
• Year: 2000
• Where: ISSTA
• Authors: Paul Z. Kolano, Richard A. Kemmerer
• Keywords: Classification Schemes, ISSTA 2000, Proof Pattern, Real-time Systems, Software Engineering