The Choice of TLA+/TLC: Comparing Formal Methods
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.