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 sim...

Full description

Saved in:
Bibliographic Details
Main Authors: Stuart, D.A., Clements, P.C.
Format: Conference Proceeding
Language:English
Subjects:
Computational modeling
Concurrent computing
Condition monitoring
Contracts
Information technology
Interleaved codes
Logic design
Real time systems
Specification languages
Timing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
DOI:10.1109/REAL.1991.160381