Extended communicating finite state machines (ECFSM) are a fundamental model of computation, and despite (or perhaps due to) their simplicity they can be found at the core of many verification tools. Unfortunately, various extensions and enrichments of this basic model have led to tool sets with different input languages, which make their results largely uncomparable.
Recently, two very different input formalisms for model checking tool sets have been reconciled. In the process, semantic subtleties could be identified, leading to a better understanding of shortcomings in existing specifications written in those languages. Additionally, otherwise unnoticed bugs and performance bottlenecks in the tool sets could be identified and fixed, leading to more robust tools, and a better understanding of their relative performance.
The aim of this project is to continue this work with another input language, namely the one from well-known symbolic model checking tool NuSMV.