Jeroen Keiren: Validation of supervisory control synthesis tool CIF using model checker mCRL2


Event Details


Abstract by Michel Reniers:

We propose a method to show how model checking may be used to verify that a synthesized supervisor indeed is safe (w.r.t. safety requirements used in the synthesis procedure), nonblocking and controllable. To achieve this we propose a method for transforming networks of extended finite automata that interact through shared events, in the form of a CIF model, into an mCRL2 specification.
The approach is illustrated using a case dealing with the coordination of maintenance procedures for a high-end printer.