| Home | Rules | CfP | Call for Models | Organizers | MCC 2011 |
|---|
We are pleased to publish the results of the MCC 2012 @ PETRI NETS:
The slides presented in Hamburg on June 26, 2012 The raw report published at CoRR (Cornell Research Repository)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.
Several classes of models will be provided:
Academic models: P/T Nets (1-bounded,
k-bounded), and colored Nets (1 and k-bounded per color, with and without
non-equal guards on transitions, with and without cartesian product on colors,
with and without successor/predecessor functions) - for Colored nets, P/T
equivalent nets will be provided, "Case studies" P/T Nets.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.
Several examinations are proposed:
State Space Generation: tools will have to
generate the state space and provide data on its size, Deadlock detection: tools will have to check
if there is at least one deadlock in the system, 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 temporal logic properties:
tools will have to process verified and unverified causal properties, stating
for each one if it is verified or not.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.
The Model Checking Contest will have several steps:
Call for Models - running until October 30, 2011 - closed Call for Tool Submission - until May 20, 2012 Announcement of results - June 26, 2012