Skip to Main content Skip to Navigation
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 de l'École normale supérieure, 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 metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-01408208
Contributor : Timothy Bourke <>
Submitted on : Saturday, December 3, 2016 - 4:35:45 PM
Last modification on : Tuesday, September 22, 2020 - 3:48:55 AM
Long-term archiving on: : Monday, March 20, 2017 - 6:49:19 PM

File

final-extended.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01408208, version 1

Citation

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⟩

Share

Metrics

Record views

313

Files downloads

238