Model checking using the mcrl2 tool set

The first IPA online course day will take place Tuesday, April 20^th, starting at 10:00.

The course day will be on model checking using the mcrl2 tool set, and be presented by Tim Willemse and Jan Friso Groote.

Content

Modern computing systems typically consist of many components running in parallel, and interacting with each other and their environment. For a correct design of a modern computing system, it is therefore essential to be able to specify its intended behaviour and to analyse and reason about this behaviour.

Process algebraic modelling and verification using modal formulas is very versatile and effective for this purpose. Although it is in practice restricted to finite instances, it is a grandiose tool to quickly increase the confidence in the correctness of a distributed algorithm, or to identify problems in it.

In the morning session, we will present a process algebra using which one can formally specify system behaviour. Moreover, we will introduce a modal (fixed point) logic to reason about system behaviour and briefly go into the algorithmic aspects of model checking for this logic.

In the afternoon session the techniques will be applied to simple, but intricate distributed protocols and algorithms.

IPA’s Advanced Courses

IPA organises Advanced Courses on each of its major research fields: Algorithmics and Complexity, Formal Methods and Software Technology. Each of these Advanced Courses intends to give an overview of (part of) the research of IPA in this specific field.

The Advanced Courses focus on subject areas where successful research is being conducted by groups in IPA, with some prominent (inter)national speakers as well. Course components consist of lectures mixed with active training (exercises, assignments, etc.).

Outside pandemic times, these Advanced Courses are scheduled as five consecutive course days on site, typically at TU/e. For now, we instead schedule a series of standalone online course days for each of the three research fields.

Required for Credit

As part of the IPA educational programme, IPA PhD students are required to follow the three advanced courses but are exempted for the advanced course that covers the field of specialisation of the student (but welcome to follow it). Following the Advanced Course for a field and obtaining credit for it (2 ECTS) normally requires attending at least 4 course days from that field’s course week; in pandemic times, it requires attending 4 course days from the course day series for the field.

Registration and preparation

Please register ASAP (we just ask for your e-mail, first and last name, affiliation, and background (IPA / non-IPA, PhD student / staff member).

Registration closes Monday April 19^th 13:00, after which the meeting link (likely MS Teams) and details will be sent around.

NB: participants are expected to download the toolset at www.mcrl2.org before the course day.

Background

Book: J.F. Groote and M.R. Mousavi.  Modeling and analysis of communicating systems. The MIT press. 2014.

The site www.mcrl2.org also contains links to over 60 Coursera lectures on mCRL2.

The mCRL2 toolset is open source and has no restrictions on its use, also not for commercial purposes.

Schedule

The overall schedule of the course days is as follows: course days will start at 10.00 and last until approximately 16.00 hours. There will be a short break in the morning and afternoon, and a longer lunch break at, roughly, 12.15-13.30.

IPAndemic online events beyond April

We are hoping for a second thematic afternoon online event in May.

A next course day is tentatively planned for early June.

Overall, we plan to offer 1–2 short days or half-days every 3–4 weeks, alternating between course days and thematic afternoons.