HomeRulesCfPCall for ModelsOrganizersMCC 2011
Model Checking Contest @ PETRI NETS 2012
Hamburg, Germany, June 25-29 2012
Call for Tool Submission closed
Participating models are: alpina, crocodile, helena, ITS-tools, lola-binstore, lola-bloom, marcie, neco, pnxdd, sara.

Results of the MCC 2012

We are pleased to publish the results of the MCC 2012 @ PETRI NETS:

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 a first edition @ SUMO'2011 within the context of the PETRI NETS and ACSD conferences, we are preparing a second edition with more features for PETRI NET 2012 in Hamburg. This first edition shown interesting outcomes to be published in an report (possibly in ToPNoC). Lessons learned allow us focus on more properties and models for this next occurrence.

According to the success of the contest and the quality of results, a report paper will be published in ToPNoC and thus officially state some clues for potential users of our technologies. This report will not only focus on performances but will provide a tentative classification of properties and techniques that have been analyzed during the contest.

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.

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: