Claim OwnershipFrom Symmetric Nets to Symmetric Nets with Bags (2015 edition, full HD)
Subscribed: 2Played: 6
Subscribe
Description
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.
17 Episodes
Reverse
This sequence starts with a general overview of the tutorial. Then, 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.
This sequence presents the syntax and semantics of Symmetric nets, 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.
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.
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.
Properties to be satisfied by the system must be expressed in a formal language. A first approach is introduced with
LTL (Linear Time Logic) properties.
Another logic allows for expressing properties on a tree of possible futures: CTL (Computational Tree Logic) properties.
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.
This short sequence starts with a general overview of the last part of the tutorial. Then, the most essential feature
of Symmetric Nets is presented through the running example. It exhibits the intrinsic symmetries of both markings and
firings in such models.
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.
The next step towards the definition of the reduced graph consists in defining subclasses of markings as well as
symbolic markings, that represent a complete subclass.
In order to express the behaviour of the system between symbolic markings, a similar approach is necessary, thus
defining a symbolic firing rule.
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.
This approach of Symbolic Reachability Graph is further improved in this sequence by defining static subclasses, where
all elements within a same subclass have the same behaviour.
When these elements are so distinct that they show only individual behaviour, partial symmetries, as presented in this
sequence, must be used to reduce the Symbolic Reachability Graph. These notions are roughly defined in this section.
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.
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.
To complete the presentation of Symmetric nets with Bags, a more advanced example is presented.
Comments
Download from Google Play
Download from App Store
United States