Using assertions for validating, verifying and monitoring real-time systems
Sitaram C. V. Raju · 1994
Real-time systems are different from traditional computer systems because they have timing constraints that must always be met. Designing correct real-time systems is not an easy task because it is simply not possible to exhaustively test any large real-time system. In this dissertation we attempt to address this problem by using assertions for validating, verifying and monitoring real-time systems. We first present a prototyping environment for an executable specification scheme called Communicating Real-Time State Machines (CRSMs). The system behavior of CRSMs is characterized by a time-stamped trace of communication events. We present a novel assertion language for specifying safety and timing assertions on the trace of communication events. The prototyping environment consists of a graphical editor for describing CRSMs, a CRSM simulator to observe the execution of the prototype, and an assertion checker for monitoring assertions during simulation. We then describe an automatic verification technique for real-time systems modeled by an expressive subclass of CRSMs. The proposed approach is to represent the behavior of the system by a finite, timed reachability graph. We provide a decision procedure for verifying timing and safety properties (specified in our assertion language) of the reachability graph. We describe an implementation of the verification technique and demonstrate its usefulness on example real-time specifications. Even if a real-time system has been formally specified, verified and then implemented in software it is important that the implementation check for constraint violations states at run-time. The reason is that unexpected conditions at run-time must not cause the real-time system to fail. We describe a run-time environment for monitoring timing constraints in distributed real-time systems. Timing constraints are specified in a subset of our assertion language. Constraint violations are detected at the earliest possible time by deriving and checking intermediate constraints from the user-specified constraints. The major contributions of this dissertation are: a method for checking CRSM simulations, an automatic verification technique for CRSMs, and the development of a run-time monitor for real-time applications. Future work includes the development of a scalable verification method and experimenting with large real-time applications.