Skip to Main content Skip to Navigation
New interface
Conference papers

Soundness of the Quasi-Synchronous Abstraction

Guillaume Baudart 1, 2 Timothy Bourke 1, 2 Marc Pouzet 1, 2, 3 
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : Many critical real-time embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasi-synchronous abstraction was introduced by P. Caspi for model-checking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: the only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other. We formalize the relation between the real-time model and the quasi-synchronous abstraction by introducing the notion of a unitary discretisation. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and timing parameters to recover soundness.
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Timothy Bourke Connect in order to contact the contributor
Submitted on : Saturday, December 3, 2016 - 4:35:45 PM
Last modification on : Thursday, March 17, 2022 - 10:08:45 AM
Long-term archiving on: : Monday, March 20, 2017 - 6:49:19 PM


Files produced by the author(s)


  • HAL Id : hal-01408208, version 1


Guillaume Baudart, Timothy Bourke, Marc Pouzet. Soundness of the Quasi-Synchronous Abstraction. Formal Methods in Computer-Aided Design (FMCAD), Oct 2016, Mountain View, CA, United States. pp.9-16. ⟨hal-01408208⟩



Record views


Files downloads