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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Introduction: OpenComRTOS Role in a Unified Systems Engineering Methodology Kapitel lesen Erstes Kapitel lesen

2011 | OriginalPaper | Buchkapitel

3. The Choice of TLA+/TLC: Comparing Formal Methods

verfasst von : Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev

Erschienen in: Formal Development of a Network-Centric RTOS

Verlag: Springer US

Einloggen

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

search-config
loading …

Abstract

This book provides a thorough description of OpenComRTOS and of the formal models built for its implementation. Such models were written in TLA +  and verified with the TLC model checker. The choice of TLA + /TLC was one of the fundamental initial decisions of the project. In effect, over the last years, several languages, techniques, and tools have been developed and made available by the formal methods community. Typically, different formalisms are best suited for different domains of application, and their comparison is not straightforward. It can be a significantly subjective exercise. This chapter addresses this issue, describing the selection process followed in this project.

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 Requirements and Specifications for the OpenComRTOS Project
Nächstes Kapitel Basic Formal Specification in TLA+
Fußnoten
1
The actual implementation of the marking can be done using an unused bit of the field next of the node.
 
2
This mail happen for two reasons: (a) another concurrent process could have deleted the node in the mean time or (b) there was some error in the assignment of the node to delete and it simply does not belong to the linked list.
 
3
“Empty” is not an exact term. Once the memory location has been freed it can be in a multiplicity of different states that may lead to the referred error. The actual behavior of a process in this scenario depends on the details of the implementation.
 
4
Recall that the comparison is made between the value of the node’s next field previously recorded and the present one. Even if the composition of the list has not changed in the mean time, the values will not match because the present reference is marked while the value previously recorded is not. This is due to decision of marking a node by a change in an unless unused bit of the next filed of the node. In any case, if other implementation scheme would not cause this comparison to fail the process would continue to (VId) and would then forcedly be sent back to (IId), continuing as announced in (8).
 
5
For example, the CAS primitive is supported as the “CASA” and “CASXA” operations in Sparc V9 (SPARC International 1994), and as “lock cmpxchg” in Intel Itanium (Intel Corporation 2002).
 
6
See Sect. 3.2.4.
 
7
Together with the standard modules Naturals and Extends.
 
8
This has no effect in the definitions made in the module; it can, however, be taken as an hypothesis in the construction of proofs.
 
9
Strictly speaking, there is an exception: IId and IIId were grouped into a single action.
 
10
Note the use of “possible instance”. In fact, the configuration file may have many instances by changing the definitions of the constants in it. The TLA +  model remains, however, unchanged.
 
11
More rigorously, it asserts that the formula follows logically from the definitions in this module, the definitions in the extended modules Naturals, Sequences, and FiniteSets, and the rules of TLA + .
 
12
In our case, this feature is really useful since variable proc encapsulates many fields.
 
13
For differentiation each process is assigned a unique instantiation number. This is done automatically, and the user does not need to worry about it. If necessary, each process can refer to its own instantiation number via the predefined local variable _pid.
 
14
No intermediate levels can created, i.e. the scope of a global variable cannot be restricted to a subset of processes and the scope of a local one to specific blocks of statements.
 
15
if and only if.
 
16
This notation is inspired in (Dijkstra 1975).
 
17
This is not mandatory though, for some properties it can be achieved with an assertion clause through the construction: proctype monitor() assert(invariant) , but this looks a “dirtier” solution.
 
18
It can be perfectly valid, for instance, for server processes to enter a wait state after a transition is completed, immune to the fact that all user processes have terminated.
 
19
And after Sect. 3.4.1, naturally, if you are not familiar with Promela.
 
20
Note that operations like reads and writes are executed atomically.
 
21
See also Table 3.1 on page 29.
 
22
Recall that a never claim that checks for the invariance of system property p can be written in Promela as:
 
23
if ::CNkey=10... ::CNkey=50 fi
 
24
See Sect. 3.2.4.
 
25
Several sources of inspiration were used for this exercise; most notably, Sifakis (2010).
 
26
In the figure, □ is used if both systems are given an equivalent classification and \(diamond\) otherwise.
 
28
As a curiosity, you can, for instance, see page 51.
 
Metadaten
Titel
The Choice of TLA+/TLC: Comparing Formal Methods
verfasst von
Eric Verhulst
Raymond T. Boute
José Miguel Sampaio Faria
Bernhard H. C. Sputh
Vitaliy Mezhuyev
Copyright-Jahr
2011
Verlag
Springer US
Buch
Formal Development of a Network-Centric RTOS

Print ISBN: 978-1-4419-9735-7

Electronic ISBN: 978-1-4419-9736-4

Copyright-Jahr: 2011

DOI
https://doi.org/10.1007/978-1-4419-9736-4_3