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)

1 CEA - Commissariat à l'énergie atomique et aux énergies alternatives
2 GALLIUM - Programming languages, types, compilation and proofs
3 MSR - INRIA - Microsoft Research - Inria Joint Centre
4 PARSIFAL - Proof search and reasoning with logic specifications
5 MOSEL - Proof-oriented development of computer-based systems
6 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

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.

Domaines: Logique en informatique [cs.LO]

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz. Proving Determinacy of the PharOS Real-Time Operating System. 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⟩. ⟨hal-01322335⟩