Since Symmetric Nets with Bags allow for manipulating bags of values, they make use of new functions on colours and on
	bags in their firing rule. These functions are explained and examplified.

Since Symmetric Nets with Bags allow for manipulating bags of values, they make use of new functions on colours and on bags in their firing rule. These functions are explained and examplified.

S3.09 Functions Used in Symmetric Nets with Bags and Firing Rules

Nowadays, systems tend to be more and more distributed. Distribution brings a huge complexity and a strong need to
      deduce possible (good and bad) behaviours on the global system, from the known behaviour of its actors. For such
      systems, we know that classical development methods are not adequate since the coverage of possible executions is too
      low. This is an old observation that led people to investigate the use of formal methods. One good candidate for
      analysing such systems is Petri nets. More specifically, 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 techniques. 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 presents the underlying theory, the verification approaches, typical applications, and
      puts these into practice through hands-on sessions using the CosyVerif verification environment.

Nowadays, systems tend to be more and more distributed. Distribution brings a huge complexity and a strong need to deduce possible (good and bad) behaviours on the global system, from the known behaviour of its actors. For such systems, we know that classical development methods are not adequate since the coverage of possible executions is too low. This is an old observation that led people to investigate the use of formal methods. One good candidate for analysing such systems is Petri nets. More specifically, 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 techniques. 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 presents the underlying theory, the verification approaches, typical applications, and puts these into practice through hands-on sessions using the CosyVerif verification environment.

Share S3.09 Functions Used in Symmetric Nets with Bags and Firing Rules

Sign up to save your podcasts

S3.09 Functions Used in Symmetric Nets with Bags and Firing Rules

S3.09 Functions Used in Symmetric Nets with Bags and Firing Rules