You may get the pdf version of the Call for Models here.
Goals
The Model Checking Contest is a yearly event, jointly held with the Petri Nets conference, that gathers developers of formal verification tools for concurrent systems. The first goal of the Model Checking Contest is to enable the assessment of existing tools on a set of models (i.e., benchmarks) proposed by the scientific community. All tools are compared on the same benchmarks and using the same computing platform, so that a fair comparison can be made, which is not possible using traditional scientific publications, which use different benchmarks executed on different platforms.
The second goal of the Model Checking Contest is to infer conclusions about the respective efficiency of verification techniques for Petri nets (decision diagrams, partial orders, symmetries, etc.) depending to the particular characteristics of models under analysis. Through the feedback on tools efficiency, we aim at identifying which techniques can best tackle a given class of models. Finally, the Model Checking Contest seeks to be a friendly place where developers meet, exchange, and collaborate to enhance their verification tools.
Call for Models
The Model Checking Contest is organized in successive steps: the first step is the present Call for Models. The next steps will be the Call for Tools (March 2014) and the Contest itself. We kindly ask the community (and not only tool developers) to propose models on which the verification tools will be assessed. The list of models used in the previous editions (2011, 2012, and 2013) is available here.
All submitted models will be reviewed by the call for model organizers (Hubert Garavel, Lom Hillah, Fabrice Kordon) and a representative subset of them will be selected. For the 2014 edition, we expect to retain a dozen new models, which will be added to those models already used in the previous editions.
The organizers of the Model Checking Contest will do their best efforts to ensure that the models submitted to the 2014 edition are not known in advance by tool developers participating to the contest. These models will be «surprise» models, whereas models submitted to the previous editions of the Model Checking Contest are now known to tool developers.
Submitting One (or Many) Model(s)
By submitting a model, you explicitly allow the organizers of the Model Checking Contest to freely use this model and publish it on the web. Submitted models should be in the public domain. If your model is proprietary or confidential, do not submit it.
The names of authors of selected models will be acknowleged on the Model Checking Contest web site. Each model can be:
- either a «classical» P/T net
- or a colored Petri net (with/without non-equal guards on transitions, cartesian product on colors, and successor/predecessor functions). For a colored net, an equivalent «unfolded» P/T net can be provided as well.
A model may depend on one or many parameters, which provide scaling capabilities (e.g., in the number of places, transitions, tokens, colors, etc.) and thus modify the size of the corresponding marking graph. To submit a model, four types of files should be provided:
- A PNML file describing the model. If the model is parameterized and exists in different instances, or if it is colored and has an equivalent P/T net, then several PNML files can be provided. The PNML reference site is http://www.pnml.org. If help is needed, please contact lom-messan.hillah@lip6.fr.
- A LaTeX form that must be filled in to provide summary information about the model, its origin, its size, etc. An example of filled form is available here.
- If possible, a picture of the model to be included in the LaTeX form.
- If possible, a set of relevant properties (typically, invariants, bounds, reachability, LTL or CTL formulas) that can be evaluated on this model.
The forms as well as detailed instructions for submission are given in the model submission kit here.
Deadline
The deadline for submission of model for the Model Checking Contest is December 15, 2013.