The mCRL2 behavioural specification language and tools, including new developments

Title:   The mCRL2 behavioural specification language and tools, including new developments

Speaker: Prof. Jan Friso Groote, Technical University Eindhoven

Venue:   Room 334, Building 5, Institute of Software, CAS

Time:    Thursday May 30, 15:00

 

Abstract: The mCRL2 language originated in 1990 to specify communicating systems including data and time in a process algebraic style.  Behavioural properties can be denoted using the modal mu-calculus with data and time, as it stands the most expressive logic for this purpose.  The language and the logic have been provided with a complete mathematical underpinning, as well with a powerful toolset for analysis purposes.  The tools are open source and free for use (www.mcrl2.org).

 

In this talk a short overview will be given of the language, its capabilities and its increasingly widespread use.  Furthermore, some of the new developments will be addressed, namely probabilities, counterexamples/witnesses for arbitrarily complex behaviour properties and its use to verify global properties of newly developed industrial software.

 

Bio: Jan Friso Groote obtained a PhD at CWI and the University of Amsterdam in the

area of operational semantics and process algebra in 1991.  Since 1998, he works as a full

professor at Eindhoven University of Technology.  His main interest is in modelling

and analysis of especially embedded software, with a focus on delivering correct

efficiently.  He is the father of the mCRL2 language and toolset.