Advertisement

The Choice of TLA+/TLC: Comparing Formal Methods

  • Eric Verhulst
  • Raymond T. Boute
  • José Miguel Sampaio Faria
  • Bernhard H. C. Sputh
  • Vitaliy Mezhuyev
Chapter

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.

Keywords

Model Checker Linear Temporal Logic Concurrent System Linear Temporal Logic Formula State Model Checker 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer Science+Business Media, LLC 2011

Authors and Affiliations

  • Eric Verhulst
    • 1
  • Raymond T. Boute
    • 2
  • José Miguel Sampaio Faria
    • 3
  • Bernhard H. C. Sputh
    • 4
  • Vitaliy Mezhuyev
    • 4
  1. 1.Altreonic NVLeuvenBelgium
  2. 2.Department of Information TechnologyUniversiteit Gent Faculty of EngineeringGentBelgium
  3. 3.MazarefesPortugal
  4. 4.Open License SocietyLeuvenBelgium

Personalised recommendations