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, ENS Paris - École normale supérieure - 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.
Type de document :
Communication dans un congrès
Formal Methods in Computer-Aided Design (FMCAD), Oct 2016, Mountain View, CA, United States. pp.9-16, 2016, Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design. 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/index.html〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01408208
Contributeur : Timothy Bourke <>
Soumis le : samedi 3 décembre 2016 - 16:35:45
Dernière modification le : mardi 6 décembre 2016 - 01:05:58
Document(s) archivé(s) le : lundi 20 mars 2017 - 18:49:19

Fichier

final-extended.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01408208, version 1

Collections

UPMC | INRIA | PSL

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, 2016, Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design. 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/index.html〉. 〈hal-01408208〉

Partager

Métriques

Consultations de
la notice

114

Téléchargements du document

37