19 July 2016 at Newcastle University, Newcastle upon Tyne, UK
A large number of models that are employed in the field of concurrent systems' design, such as Petri nets, Signal Transition Graphs, gate-level circuits, dataflow structures – all have an underlying static graph structure. Their semantics, however, is defined using additional entities, e.g. tokens or node/arc states, which collectively form the overall state of the system. We jointly refer to such formalisms as Interpreted Graph Models (IGMs).
Workcraft is flexible framework for development of IGMs. It provides a graphical frontend for capturing, (co-)simulation and analysis of IGMs and relies on a number of established backend tools for model checking, synthesis, and verification tasks (Petrify, Punf, Mpsat, etc).
The aim of this tutorial is to overview several IGMs and demonstrate their use to formal modelling and verification of systems and processes from different application domains, such as: