Proving Determinacy of the PharOS Real-Time Operating System

Selma Azaiez 1 Damien Doligez 2, 3 Matthieu Lemerre 1 Tomer Libal 4, 3 Stephan Merz 5, 6, 3
4 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
5 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
6 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Executions in the PharOS real-time system are deterministic in the sense that the sequence of local states for every process is independent of the order in which processes are scheduled. The essential ingredient for achieving this property is that a temporal window of execution is associated with every instruction. Messages become visible to receiving processes only after the time window of the sending message has elapsed. We present a high-level model of PharOS in TLA+ and formally state and prove determinacy using the TLA+ Proof System.
Type de document :
Communication dans un congrès
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. Springer, 9675, pp.70-85, 2016, LNCS - Lecture Notes in Computer Science. <10.1007/978-3-319-33600-8_4>
Liste complète des métadonnées

https://hal.inria.fr/hal-01322335
Contributeur : Stephan Merz <>
Soumis le : vendredi 27 mai 2016 - 09:21:24
Dernière modification le : samedi 18 février 2017 - 01:13:43

Fichier

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

Identifiants

Citation

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz. Proving Determinacy of the PharOS Real-Time Operating System. Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. Springer, 9675, pp.70-85, 2016, LNCS - Lecture Notes in Computer Science. <10.1007/978-3-319-33600-8_4>. <hal-01322335>

Partager

Métriques

Consultations de
la notice

238

Téléchargements du document

68