Dogfooding the structural operational semantics of mCRL2
The mCRL2 language is a formal specification language that is used to specify and model the behavior of distributed systems and protocols. With the accompanying toolset, it is possible to simulate, visualize, analyze and verify behavioral properties of mCRL2 models automatically. The semantics of the mCRL2 language is defined formally using Structural Operational Semantics (SOS) but implemented manually in the underlying toolset using C++.
Like with most formal languages, the underlying toolset was created with the formal semantics in mind but there is no way to actually guarantee that the implementation matches the intended semantics.
To validate that the implemented behavior for the mCRL2 language corresponds to its formal semantics, we describe the SOS deduction rules of the mCRL2 language, and perform the transformation from the mCRL2’s SOS deduction rules to a Linear Process Specification. As our transformation directly takes the SOS deduction rules and transforms them into mCRL2 data equations, we are basically feeding the mCRL2 toolset its own formal language definition.
This report describes
the semantics for the untimed fragment of the mCRL2 language,
the transformation of the deduction rules into data equations including the underlying design decisions and
the experiments that have been conducted with our semantic transformation.
Despite its formal characterization, thorough study and broad use in many areas, our semantic dogfooding approach revealed a number of (subtle) differences between the mCRL2’s intended semantics, the defined semantics and its actual implementation.
Technical details
With our approach we capture the untimed semantics of mCRL2 in (roughly) 1000 lines of mCRL2 code.
- Type of verification
Simulation/Validation
- Equipment (computers, CPU, RAM)
2.8 GHz Intel Core Duo, Mac OS-X 10.6.8, 4GB 800 MHz
- mCRL2 toolset
SVN revision 9500-9800.
- Models
The model is available as an appendix of [SRGW11].
- Organizational context
- Contact person:
Frank Stappers, Technische Universiteit Eindhoven, The Netherlands.
- Other people involved:
Michel Reniers (TU/e Eindhoven)
Jan Friso Groote (Technische Universiteit)
Sven Weber (ASML)
- Institution:
Technische Universiteit Eindhoven, The Netherlands.
- Industrial partner:
The project was a cooperation with ASML in Veldhoven, The Netherlands.