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.
Cite
CITATION STYLE
Azaiez, S., Doligez, D., Lemerre, M., Libal, T., & Merz, S. (2016). Proving determinacy of the PharOS real-time operating system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9675, pp. 70–85). Springer Verlag. https://doi.org/10.1007/978-3-319-33600-8_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
