| Title: |
Proving Determinacy of the PharOS Real-Time Operating System |
| Authors: |
Azaiez, Selma; Doligez, Damien; Lemerre, Matthieu; Libal, Tomer; Merz, Stephan |
| Contributors: |
Commissariat à l'énergie atomique et aux énergies alternatives (CEA); Programming languages, types, compilation and proofs (GALLIUM); Inria Paris-Rocquencourt; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria); Microsoft Research - Inria Joint Centre (MSR - INRIA); Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation Redmond, Wash.; Proof search and reasoning with logic specifications (PARSIFAL); Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX); École polytechnique (X); Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X); Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Saclay; Proof-oriented development of computer-based systems (MOSEL); Department of Formal Methods (LORIA - FM); Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS); Modeling and Verification of Distributed Algorithms and Systems (VERIDIS); Max-Planck-Institut für Informatik (MPII); Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Centre Inria de l'Université de Lorraine; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM); Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS); Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró |
| Source: |
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016 ; https://inria.hal.science/hal-01322335 ; Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩ |
| Publisher Information: |
CCSD; Springer |
| Publication Year: |
2016 |
| Collection: |
Université de Lorraine: HAL |
| Subject Terms: |
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
| Subject Geographic: |
Linz; Austria |
| Description: |
International audience ; 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. |
| Document Type: |
conference object |
| Language: |
English |
| DOI: |
10.1007/978-3-319-33600-8_4 |
| Availability: |
https://inria.hal.science/hal-01322335; https://inria.hal.science/hal-01322335v1/document; https://inria.hal.science/hal-01322335v1/file/final.pdf; https://doi.org/10.1007/978-3-319-33600-8_4 |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.63E23990 |
| Database: |
BASE |