fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Home Page
Last Updated
Apr. 26, 2013
The MCC'2013 Results have been published
"Surprise Models" are: HouseConstruction, IBMB2S565S3960, QuasiCertifProtocol, Vasy2003.
The full archives with formulas can be found there.
The Call for Tool Participation is closed
The Call for Models is closed

Results for the MCC@Petri Net 2013

Objectives

When modeling a system with formal methods, such as Petri Nets, one may have several questions such as: "To verify highly concurrent systems, should we use a symmetry-based or a partial order-based model checker?" or "For models with large variable domains, should we use decision diagram-based, or a symmetry-based model checker?"

Results that help to answer these questions are spread among numerous papers in numerous conferences. Moreover, as benchmarks are executed over several platforms and composed of different models, conclusions are not easy.

The objective of the Model Checking Contest is to compare the efficiency of techniques according to characteristics of models. To do so, the Model Checking Contest compares tools on several classes of models with scaling capabilities (e.g. values that set up the "size" of its associated state space). Through the feedback on tools efficiency according to the selected benchmarks, we aim at identifying the techniques that can tackle a given type of problem identified in a "typical mode", for a given class of problem (e.g. state space generation, deadlock detection, reachability analysis, causal analysis).

After two editions in 2011 and 2012, this is the third one that will take place at PETRI NET 2013 in Milano.

Results from previous editions

Types of Models

Several classes of models will be provided:

All models will be provided as PNML files. The two types of models will be provided with a detailed set of characteristics that tools can exploit when possible. For colored Nets, a P/T unfolded equivalent P/T net will be provided in most cases.

IMPORTANT: you may submit a tool that is not working on Petri nets provided the models in your formalism are Kripke equivalent to those of the Model Checking Contest.

Case studies are proposed to evaluate the possibilities of a tool in a "push-button" mode. Thus, they will not be known before submission time and, to participate, tools will have to parse the PNML format (for P/T nets only), PNML for colored nets will also be provided but this is not mandatory for tools to support it.

Examinations for Model Checkers

Several examinations are proposed:

Each examination will be processed for all the scaling values of benchmark models. CPU and memory consumption will be measured and reported. Formulae will be provided in a dedicated language for which a BNF in ANTLR format will be provided.

Tools will have to provide results as well as an identification of the techniques activated during their execution.

Steps of the Model Checking Contest

The Model Checking Contest will have several steps: