We are pleased to announce that 9 tools participate this year (with newwbies):
cunf, greatspn, helena, lola, marcie, pnmc, pnxdd, stratagem, tapaal
You must either download the call for tool submission or patch your virtual machine if you already modified it (instructions provided).
PNML files are also available for each model basis for testing purposes.
(to be published when tools are submitted).
Results for the MCC@Petri Net 2014
- The HTML report,
- The sides presented in Tunis.
If you want to cite the 2014 MCC report, please proceed as follows (bibtex entry):
@misc{mcc:2014,
Author = {F. Kordon and H. Garavel and L-M. Hillah and F. Hulin-Hubard and A. Linard and
M. Beccuti and S. Evangelista and A. Hamez and N. Lohmann and E. Lopez and
E. Paviot-Adet and C. Rodriguez and C. Rohr and J. Srba},
Howpublished = {{http://mcc.lip6.fr/2014}},
Lastchecked = {2014},
Title = {{HTML results from the Model Checking Contest @ Petri Net (2014 edition)}},
Urldate = {2014},
year = {2014}}
This should look like to this (useful for those who prefer word-like word processors ;-):
Objectives
The Model Checking Contest is a yearly scientific event dedicated to the assessment of formal verification tools for concurrent systems.
The Model Checking Contest has two different parts: the Call for Models, which gathers Petri net models proposed by the scientific community, and the Call for Tools, which benchmarks verification tools developed within the scientific community.
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).
The Model Checking Contest is composed of two calls: a call for models and a call for tool participation.
After three editions in 2011, 2012 and 2013, this is the fourth one that will take place at PETRI NETS 2014 in Tunis.
Examinations for Model Checkers
Several examinations are proposed:
- State space generation: tools will have to generate the state space and provide data on its size,
- Evaluation of reachability properties: tools will have to process verified and unverified reachability properties, stating for each one if it is verified or not,
- Evaluation of Linear Temporal Logic properties (LTL): tools will have to process verified and unverified causal properties, stating for each one if it is verified or not,
- Evaluation of Computation Tree Logic properties (CTL): tools will have to process verified and unverified causal properties, stating for each one if it is verified or not.
Important dates
The Model Checking Contest will have several steps:
- publication of the «Known» models: October 30, 2013 (see the full list)
- Call for model: October 30, 2013
- Model submission: December 15, 2013 (see the call for models)
- Publication of submission procedure: March 3, 2014
- Tool submission: April 30, 2014
- Announcement of results: June 24, 2014
Results From Previous Editions
- MCC'2013 @ MIlano: slides - HTML report - PDF report (CoRR)
- MCC'2012 @ Hamburg: slides - report (CoRR)
- MCC'2011 @ Newcastle: slides - report (ToPnoC link)