Clairvoyance, capricious timing faults, causality, and real-time specifications

The authors examine the issues of satisfiability, clairvoyance, the demonstrable existence of timing faults, and event causality, all in the context of formal methods for real-time systems. Representative languages and logics are introduced to illustrate the points. The authors introduce SRSL, a simplified specification language used to illustrate the issues involved. They examine these issues in a particular specification language, Modechart. An action-free subset of Modechart is shown to be satisfiable and to obviate the need for clairvoyance. A technique for eliminating nonlinearizable computations from a specification language is shown. The usefulness of the ideas is illustrated by their use in a Modechart simulator