Groupe MeFoSyLoMa

Séminaire du 15 Juin 2012

Lieu

Programme

10h00-12h00: présentation et démonstration d'outils

ObsGraphTool
Objectif: Le but est de vérifier les procédés d'entreprise modélisés avec le modèle Reseau de Petri. L'outils permet de détecter un deadloack après construction du graphe d'observation symbolique associé au modèle à vérifier. Il permet aussi de vérifier la correction d'une composition asynchrone de un ou plusieurs modèles en utilisant le produit synchronisé des SOGs associés à chaque modèle.
Abstract: l'outil ObsGraphTool implemente l'approche de vérification des workflows basé sur le Graphe d'Observation Symbolique. C'est une approche qui présente une abstraction des workflows qui respecte une certaine confidentialité pour la structure interne des procédés d'entreprise (cachée) et qui expose seulement les actions contribuant à une éventuelle composition avec des partenaires. La vérification de l'absence de blocage d'un modèle composé est donc réduite à la vérification de l'absence de blocage du produit synchronisé des abstractions associées aux composantes.
IMITATOR (standing for Inverse Method for Inferring Time AbstracT behaviOR)
Objective: It is a tool for efficient parameter synthesis for Timed Automat.
Abstract: It is based on the inverse method: this semi algorithm generalizes a concrete behavior of a PTA, by synthesizing constraints on the timing parameters.
Thus, this provides the system with a criterion of robustness, and allows timing optimization. IMITATOR has been recently extended to hybrid automata on the one hand, and to stopwatch automata on the other hand, allowing in particular parameter synthesis for scheduling problems.
(Time) Petri Net tools :
Objective : model and analyze the behavior of (Time) Petri nets. This CosyVerif package embeds several existing model-checkers such as K. Wolf's Lola tool, or Berthomieu's Tina tool.
Abstract : These tools allow a wide variety of analysis, from simple behavioral properties (boundedness, reversibility,...) to full temporal logic model-checking. We will show how to use some of these features for low-level Petri nets and their Time extension.

12h00-14h00: Déjeuner

14h00-15h00: Liu Yang, National University of Singapore, "Pervasive Model Checking"

Abstract: Model checking is emerging as an effective software verification method with wide applications. However, still there are a lot research challenges in model checking techniques and in applying model checking techniques. To address these challenges, this talk presents our research contributions in the system modeling, efficient model checking algorithms development and effective reduction techniques. More important, we introduce a process analysis toolkit (PAT, www.patroot.com), which is a self-contained verification framework for specification, simulation and verification of concurrent, real-time and probabilistic systems. PAT architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and so on. Various model checkers have been developed under this new architecture in short time. Since PAT is released 5 years ago, it has attracted 1800+ registered users world wide. Our vision is to achieve pervasive model checking so as to build a framework for realizing different verification techniques, and making model checking as planning, problem-solving, scheduling/services.

15h00-15h30 : Alexis Marechal, SMV - Univ. Genève, "Extending Modular PNML to cover exotic features"

Abstract: Modular PNML is a formalism defined within the framework of the ISO/IEC 15909 standard. Its objective is to cover the characteristics of most modular extensions of Petri nets formalisms. There are two composition mechanisms defined in Modular PNML: fusion of places and transitions, and data types sharing. In this presentation we will present a first attempt at gathering in a single definition some more advanced features of modular formalisms that were defined in the literature. We will also briefly mention how these features could be integrated into an extension of Modular PNML, in order to cover even more modular Petri net formalisms.

Séminaires