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

9 December 2002

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 254-263
https://doi.org/10.1109/real.1991.160381

Abstract

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.

Keywords

This publication has 2 references indexed in Scilit:

Safety analysis of timing properties in real-time systems
IEEE Transactions on Software Engineering, 1986
Automatic verification of finite-state concurrent systems using temporal logic specifications
ACM Transactions on Programming Languages and Systems, 1986