Univesité Pierre et Marie CURIE From Symmetric Nets to Symmetric Nets with Bagshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014Nowadays, 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.<br /> One good candidate for analyzing such systems are 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.<br /> 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.<br /> 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.http://vodcast.upmc.fr/images/C014_petri_net_tutorial.pngFrom Symmetric Nets to Symmetric Nets with Bagshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_20143.11 Second Example of SNBhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=19To complete the presentation of Symmetric nets with bags, a more advanced example is presented.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-11.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:31 +0200E_petri_net_tutorial_2014_193.10 Functions Used in SBN and Firing Rulehttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=18Since 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-10.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:32 +0200E_petri_net_tutorial_2014_183.09 Symmetric Nets with Bagshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=17Models 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-09.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:33 +0200E_petri_net_tutorial_2014_173.08 SN and Partial Symmetrieshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=16When 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-08.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:30 +0200E_petri_net_tutorial_2014_163.07 Static Subclasseshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=15This approach of Symbolic Reachability Graph is further improved by defining static subclasses, where all elements within a same subclass have the same behaviour.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-07.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:29 +0200E_petri_net_tutorial_2014_153.06 The Symbolic Reachability Graphhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=14The 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-06.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:26 +0200E_petri_net_tutorial_2014_143.05 Symbolic Firing Rulehttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=13In order to express the behaviour of the system between symbolic markings, a similar approach is necessary, thus defining a symbolic firing rule.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-05.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:27 +0200E_petri_net_tutorial_2014_133.04 Dynamic Subclasses and Symbolic Markingshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=12The 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-04.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:28 +0200E_petri_net_tutorial_2014_123.03 Symmetries to Reduce the Reachability Graph of SNhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=11In 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-03.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:34 +0200E_petri_net_tutorial_2014_113.02 Global vs Local Symmetrieshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=10In this sequence, 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-02.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:35 +0200E_petri_net_tutorial_2014_103.01 Openinghttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=9This short sequence is a general overview of the last part of the tutorial.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-3-01.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:41 +0200E_petri_net_tutorial_2014_92.01 Introduction to Practical Workhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=8This 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-2-01.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:42 +0200E_petri_net_tutorial_2014_81.07 CTL propertieshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=7Another logic allow for expressing properties on a tree of possible futures: CTL (Computational Tree Logic) properties.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-07.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:43 +0200E_petri_net_tutorial_2014_71.06 LTL propertieshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=6Properties to be satisfied by the system must be expressed in a formal language. A first approach is introduced with LTL (Linear Time Logic) properties.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-06.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:40 +0200E_petri_net_tutorial_2014_61.05 The reachability graph for SN analysishttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=5After 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-05.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:39 +0200E_petri_net_tutorial_2014_51.04 Modelling with Symmetric Netshttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=4This 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-04.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:36 +0200E_petri_net_tutorial_2014_41.03 Syntax and semantics of SNhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=3The 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-03.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:37 +0200E_petri_net_tutorial_2014_31.02 Introductionhttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=2The 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.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-02.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:38 +0200E_petri_net_tutorial_2014_21.01 Openinghttp://video.upmc.fr//differe.php?collec=E_petri_net_tutorial_2014&video=1This short sequence is a general overview of the tutorial, and more specifically of the first part.<br /> <a href="http://video.upmc.fr/ressource/doc/E_petri_net_tutorial_2014/session-1-01.pdf"> PDF</a><br /> Thu, 09 Oct 2014 15:43:44 +0200E_petri_net_tutorial_2014_1