Petri Nets 2010, ACSD 2010 - Braga, Portugal

PETRI NETS 2010

ACSD 2010

Braga, Portugal, June 21-25, 2010
Petri Nets 2010, ACSD 2010 - Braga, Portugal

Tutorials | TT3: State space exploration of Coloured Petri Nets and the ASAP model checking platform

Authors: Lars Michael Kristensen1, Michael Westergaard2
1Department of Computer Engineering, Bergen University College, Norway, lmkr@hib.no
2Department of Computer Science, University of Aarhus, Denmark, mw@cs.au.dk


Abstract: State space exploration is one of the main approaches to model-based verification of concurrent systems and it has been one of the most successfully applied analysis methods for Coloured Petri Nets (CP-nets or CPNs). The basic idea of state space exploration is to compute all reachable states and state changes of the system under consideration and represent these as a directed graph. Using state space exploration, it is possible to automatically model check a wide range of behavioral properties of concurrent systems. The development and application of efficient state space methods is an active area of research, and with the large suite of techniques available today it is possible to apply state space methods to industrial systems.

This tutorial will provide a comprehensive road-map to the theoretical foundation of state space methods for Coloured Petri Nets, the available state space methods, the implementation in computer tools, and the practical application for verification of concurrent systems. In particular, the tutorial will present the ASAP model checking platform which constitute the next generation of computer tool support for state space exploration of CPN models. ASAP is intended to replace the widely used state space tool of CPN Tools. The vision of the ASAP model checking platform is to provide an efficient and open computer tool suited for research, educational, and industrial use of state space exploration and model checking. Experimental results have demonstrated that ASAP outperforms the state space tool of CPN Tools by several orders of magnitude.

The tutorial will be based upon research results obtained in the ASCoVeCo research project (2006-2010) undertaken by the presenters and sponsored by the Danish Research Council for Technology and Production. Further information about the ASCoVeCo research project and the ASAP model checking platform is available via: www.daimi.au.dk/~ascoveco

Tutorial Outline:

  1. Introduction
    • Introduction to state space methods for CP-nets and the research area
    • The practical application of state space methods
    • Overview of the ASAP model checking platform and comparison with other tools
  2. User perspective on application of state space methods
    • Managing verification projects: models, queries, jobs, and results
    • Creating and executing verification jobs: the JoSEL language
    • Checking safety properties and performing CTL/LTL model checking
  3. Advanced state space methods
    • Compact in-memory storage: hash compaction and the comback method
    • External memory storage and delayed duplicate detection
    • Distributed state space exploration and state space separation
  4. Research perspective on development of state space methods
    • The CPN Tools simulator interface
    • Example of integrating new methods into ASAP: the sweep-line method revisited
    • Conducting benchmarking and obtaining experimental results
    • Current state and future plans for ASAP

The tutorial will be a mixture of conventional lectures and live demonstrations of the ASAP model checking platform. ASAP will also be registered for the tool presentations at the conference. This will allow the conference participants to install ASAP on their laptops and obtain help from the developers in getting started using the tool.

Intended audience: The tutorial will be of interest to both researchers and PhD students working on state space exploration and model checking, and to practitioners working with the application of state space methods for verification of concurrent systems. The level of the tutorial will be intermediate and basic knowledge of high-level Petri nets will be assumed.

Speaker's biography:
Lars Michael Kristensen is a Professor in Computer Engineering at Bergen University College. He has more than 10 years of research experience in development and application of formal methods to concurrent systems. A main focus has been the theoretical foundation of state space methods and their implementation in computer tools, in particular in the context of Coloured Petri Nets. Important research contributions have been the development of the sweep-line state space space method, the development of two variants of the stubborn set partial-order method, and the development of the ComBack method. A strong focus has also been on evaluating the research results in industrial cooperation projects. He acted as researcher in the development of the state space tools of Design/CPN and CPN Tools, and he is the scientific leader of the ASCoVeCO project in the context of which the ASAP model checking platform is being developed. He has recently co-authored a new textbook on Coloured Petri Nets to be published by Springer-Verlag. In 2007 he received the Danish Independent Research Councils' Young Researcher's Award.

Michael Westergaard is a post-doctoral researcher at Aarhus University, where he is working with state space methods. He acts as the technical leader in the development of the ASAP model checking platform. He is interested in not only developing state space methods, but more importantly making advanced and efficient methods available to non-experts and sees tool-development as an integral part of this. He received a PhD from Aarhus University in 2007. As part of his PhD work he contributed to the development of the ComBack state space method and extensions to the sweep-line method. Furthermore, he developed the BritNEY tool for domain-specific behavioral visualization of concurrent systems.