Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Proving Determinacy of the PharOS Real-Time Operating System

verfasst von : Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz

Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Encoding TLA into Many-Sorted First-Order Logic
Nächstes Kapitel A Rigorous Correctness Proof for Pastry
Fußnoten
2
The standard module Functions defines the domain restriction of a function as https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-33600-8_4/418581_1_En_4_IEq30_HTML.gif .
 
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.
 
Literatur
1.
2.
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)
3.
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)
4.
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)CrossRef
5.
Kopetz, H., Bauer, G.: The time-triggered architecture. Proc. IEEE 91(1), 112–126 (2003)CrossRef
6.
Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)MATH
7.
Lamport, L.: Byzantizing paxos by refinement. In: Peleg, D. (ed.) Distributed Computing. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011)CrossRef
8.
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
9.
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)
10.
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)
11.
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)CrossRef
12.
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)
13.
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)CrossRef
14.
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)CrossRef
15.
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)CrossRef
16.
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)CrossRef
Metadaten
Titel
Proving Determinacy of the PharOS Real-Time Operating System
verfasst von
Selma Azaiez
Damien Doligez
Matthieu Lemerre
Tomer Libal
Stephan Merz
Copyright-Jahr
2016
Buch
Abstract State Machines, Alloy, B, TLA, VDM, and Z

Print ISBN: 978-3-319-33599-5

Electronic ISBN: 978-3-319-33600-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-33600-8_4