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

Coherence Prefix 

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