Parametrized semantics for fault tolerant real-time systems

J.A.A. Coenen, J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Abstract

Motivated by the close relation between real-time and fault tolerance, we investigate the foundations of a formal framework to specify and verify real-time distributed systems that incorporate fault tolerance techniques. Therefore a denotational semantics is presented to describe the real-time behaviour of distributed programs in which concurrent processes communicate by synchronous message passing. In this semantics we allow the occurrence of faults, due to faults of the underlying execution mechanism, and we describe the effect of these faults on the real-time behaviour of programs. Whenever appropriate we give alternative choices for the definition of the semantics. The main idea is that making only very weak assumptions about faults and their effect upon the behaviour of a program in the semantics, any hypothesis about faults must be made explicit in the correctness proof of a program. Next we introduce two parameters in the semantics that restrict the way in which variables and communication channels can be affected by faults. These parameters provide an easy way to incorporate some interesting fault hypotheses within the semantics.
Original languageEnglish
Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems
EditorsJ. Vytopil
Place of PublicationNorwell MA
PublisherKluwer Academic Publishers
Pages51-78
ISBN (Print)0-7923-9332-5
Publication statusPublished - 1993

Fingerprint Dive into the research topics of 'Parametrized semantics for fault tolerant real-time systems'. Together they form a unique fingerprint.

Cite this