Formal methods for real-time systems
Douglas A. Stuart, Aloysius K. Mok · 1996
Computers are increasingly being used to control safety-critical systems which depend on the absolute timing of system events for their correctness. Formal specification and verification is one approach to assuring that such systems are correct. Mechanical verification can enhance the utility of formal methods by increasing their applicability and reliability. This work will focus on a particular mechanical verification technique, model checking, in the context of a specific specification language environment, RTL and Modechart. RTL is a first order logic for reasoning about the times of occurrences of system events. Modechart is a specification language introduced to organize RTL specifications. Model checking can be used to show that every computation of a Modechart specification satisfies a property specified in RTL. Computation graphs will be introduced to represent the set of all computations of a Modechart specification for model checking. Decision procedures for a number of classes of RTL formulas with respect to Modechart specifications will also be introduced. One of the disadvantages of model checking as a verification technique is that it is extremely susceptible to the state explosion problem. One focus of this work is presenting different techniques for mitigating the state explosion problem. These include substituting computation graph reachability queries for more complex RTL formulas, using monitor modes, using partial computation graphs, exploiting determinism, and using simulation-verification.