Dogfooding the structural operational semantics of mCRL2

F.P.M. Stappers, M.A. Reniers, J.F. Groote, S. Weber

Onderzoeksoutput: Boek/rapportRapportAcademic

68 Downloads (Pure)


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 (i) the semantics for the untimed fragment of the mCRL2 language, (ii) the transformation of the deduction rules into data equations including the underlying design decisions and (iii) 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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's87
StatusGepubliceerd - 2011

Publicatie series

NaamComputer science reports
ISSN van geprinte versie0926-4515


Duik in de onderzoeksthema's van 'Dogfooding the structural operational semantics of mCRL2'. Samen vormen ze een unieke vingerafdruk.

Citeer dit