# Fabrice Kordon Podcasts

Fabrice Kordon public
[search 0]
More
show episodes

F
From Symmetric Nets to Symmetric Nets with Bags

### 1From Symmetric Nets to Symmetric Nets with Bags

Daily+

Nowadays, systems tend to be more and more distributed. Distribution brings a huge complexity and a strong need to deduce possible (good and bad) behaviors on the global system, from the known behavior 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 analyzing such systems are Petri nets. M ...

show series

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.10 - Functions Used in SBN and Firing Rule8:48

8:48 8:48

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.

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.09 - Symmetric Nets with Bags (PDF)

Models can be made easier to describe by enhancing parametrisation and reducing interleaving. To do so, Symmetric Nets with Bags are introduced, that allow for manipulating bags of values instead of individual values.

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.09 - Symmetric Nets with Bags9:13

9:13 9:13

Models can be made easier to describe by enhancing parametrisation and reducing interleaving. To do so, Symmetric Nets with Bags are introduced, that allow for manipulating bags of values instead of individual values.

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.06 - The Symbolic Reachability Graph (PDF)

The previous sequences have set all the basis necessary for the construction of the Symbolic Reachability Graph. It takes advantage of the symmetry between markings, and between firings, so as to study the behaviour at a symbolic level.

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.06 - The Symbolic Reachability Graph8:18

8:18 8:18

The previous sequences have set all the basis necessary for the construction of the Symbolic Reachability Graph. It takes advantage of the symmetry between markings, and between firings, so as to study the behaviour at a symbolic level.

F
From Symmetric Nets to Symmetric Nets with Bags

### 13.03 - Symmetries to Reduce the Reachability Graph of SN10:11

10:11 10:11

In this sequence, symmetries of both markings and firings are formally defined. Symmetries are a powerful tool to reduce the size of the reachability graph, thus making it amenable.

F
From Symmetric Nets to Symmetric Nets with Bags

### 12.01 - Introduction to Practical Work (PDF)

This short session is an introduction to practicals with the CosyVerif verification platform. It briefly introduces the underlying principles, the technical requirements for the installation, which are necessary to do the exercises.

F
From Symmetric Nets to Symmetric Nets with Bags

### 12.01 - Introduction to Practical Work11:59

11:59 11:59

This short session is an introduction to practicals with the CosyVerif verification platform. It briefly introduces the underlying principles, the technical requirements for the installation, which are necessary to do the exercises.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.05 - The reachability graph for SN analysis (PDF)

After having modelled a system using Petri nets, the objective is to verify it satisfies some interesting properties. To do so, the construction of the reachability graph is introduced, which exhaustively explores all possible states of the system.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.05 - The reachability graph for SN analysis12:31

12:31 12:31

After having modelled a system using Petri nets, the objective is to verify it satisfies some interesting properties. To do so, the construction of the reachability graph is introduced, which exhaustively explores all possible states of the system.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.04 - Modelling with Symmetric Nets (PDF)

This sequence presents a complete small example, where a simple train system with conditions to avoid trains collisions is modelled step-by-step. It thus shows the modelling approach process when using Symmetric nets.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.04 - Modelling with Symmetric Nets7:27

7:27 7:27

This sequence presents a complete small example, where a simple train system with conditions to avoid trains collisions is modelled step-by-step. It thus shows the modelling approach process when using Symmetric nets.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.03 - Syntax and semantics of SN (PDF)

The syntax and semantics of Symmetric nets are defined, so that a rigorous presentation of their firing rule can be given, together with an example. The specific basic colour functions that are used in Symmetric nets are also detailed.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.03 - Syntax and semantics of SN22:50

22:50 22:50

The syntax and semantics of Symmetric nets are defined, so that a rigorous presentation of their firing rule can be given, together with an example. The specific basic colour functions that are used in Symmetric nets are also detailed.

F
From Symmetric Nets to Symmetric Nets with Bags

### 11.02 - Introduction14:58

14:58 14:58

The characteristics of different kinds of Petri nets, from Place/Transition nets to Coloured nets, are put into light and motivate the focus of this tutorial on Symmetric nets. These are then informally introduced.