Depending on the system to model and analyse, using place/transition nets
may easily be cumbersome and error-prone. Hence, it might be convenient to use
some class of high-level nets. Coloured Petri nets enjoy the use of a
high-level language to describe data while the net structure captures the flow
of information. Although they provide very nice means for modelling, their
generality has the drawback of the difficulty to apply efficient analysis
In this tutorial, we focus on symmetric nets which are high-level nets with
a limited set of allowed data types, allowing for efficient state space
analysis. We also tackle their extension to symmetric nets with bags for which
analysis can still be applied.
The tutorial will present the underlying theory, the verification
approaches, typical applications, and will put these into practice through
hands-on sessions using the CosyVerif verification environment.