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.
This work was supported by the French BGLE Project ADN4SE. It was also partly funded by the Microsoft Research-Inria Joint Centre, France.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
The standard module Functions defines the domain restriction of a function as
. - 3.
For simplicity, messages are identified with the sending instruction.
- 4.
Alternatively, we could have used a single variable and represented the system state as a record in set SystemState.
.References
Alur, R., Dill, D.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Aussaguès, C., David, V.: A method and a technique to model and ensure timeliness in safety critical real-time systems. In: 4th International Conference Engineering of Complex Computer Systems (ICECCS 1998), Monterey, CA, U.S.A., pp. 2–12. IEEE Computer Society (1998)
Azmy, N., Merz, S., Weidenbach, C.: A rigorous correctness proof for pastry. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ). LNCS, vol. 9675, pp. 86–101. Springer, Heidelberg (2016)
Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA\(^{+}\) proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147–154. Springer, Heidelberg (2012)
Kopetz, H., Bauer, G.: The time-triggered architecture. Proc. IEEE 91(1), 112–126 (2003)
Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)
Lamport, L.: Byzantizing paxos by refinement. In: Peleg, D. (ed.) Distributed Computing. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011)
Lemerre, M., David, V., Aussagus, C., Vidal-Naquet, G.: Equivalence between schedule representations: theory and applications. In: Real-Time and Embedded Technology and Applications Symposium, RTAS 2008, pp. 237–247. IEEE, April 2008
Lemerre, M., Ohayon, E.: A model of parallel deterministic real-time computation. In : Proceedings of 33rd IEEE Real-Time Systems Symposium (RTSS 2012), San Juan, PR, U.S.A., pp. 273–282. IEEE Computer Society (2012)
Lemerre, M., Ohayon, E., Chabrol, D., Jan, M., Jacques, M.-B.: Method and tools for mixed-criticality real-time applications within PharOS. In: 14th IEEE International Symposium Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, Newport Beach, CA, U.S.A., pp. 41–48. IEEE Computer Society (2011)
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)
Louise, S., Lemerre, M., Aussaguès, C., David, V.: The OASIS kernel: a framework for high dependability real-time systems. In: 13th IEEE International Symposium High-Assurance Systems Engineering (HASE 2011), Boca Raton, FL, U.S.A., pp. 95–103. IEEE Computer Society (2011)
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. CACM 58(4), 66–73 (2015)
Pfeifer, H., von Henke, F.W.: Modular formal analysis of the central guardian in the time-triggered architecture. Reliab. Eng. Syst. Saf. 92(11), 1538–1550 (2007)
Rushby, J.: An overview of formal verification for the time-triggered architecture. In: Damm, W., Olderog, E.-R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 2469, pp. 83–105. Springer, Heidelberg (2002)
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)
Acknowledgements
Jael Kriener contributed to this work by writing initial specifications and proofs of PharOS executions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Azaiez, S., Doligez, D., Lemerre, M., Libal, T., Merz, S. (2016). Proving Determinacy of the PharOS Real-Time Operating System. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-33600-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33599-5
Online ISBN: 978-3-319-33600-8
eBook Packages: Computer ScienceComputer Science (R0)