Proving Determinacy of the PharOS Real-Time Operating System

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{AzaiezDLLM16,
  author       = {Selma Azaiez and
                  Damien Doligez and
                  Matthieu Lemerre and
                  Tomer Libal and
                  Stephan Merz},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Proving Determinacy of the PharOS Real-Time Operating System},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {70--85},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_4},
  doi          = {10.1007/978-3-319-33600-8\_4},
  timestamp    = {Sat, 09 Apr 2022 12:45:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/AzaiezDLLM16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}