fond

jQuery Multi Level CSS Menu Css3Menu.com

Model Checking Contest @ Petri Nets 2017
7th edition, Zaragoza, Spain, June 27, 2017
Call for Models
Last Updated
June 27, 2017

Goals

The Model Checking Contest (MCC) is a yearly event that assesses existing verification tools for concurrent systems 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, contrary to most scientific publications, in which different benchmarks are executed on different platforms.

The Model Checking Contest is organized in three steps:

Call for Models

At the core of the Model Checking Contest is a collection of models accumulated from the previous editions of the contest. This collection currently comprises 56 different models, which have been already used and cited in 30 scientific publications.

For the 2017 edition, we kindly ask the scientific community (beyond the developers of verification tools) to propose novel models. Each model should be representative of a non-trivial academic or industrial problem that involves concurrency aspects, and may belong to very diverse fields such as software or hardware design, networking, biology, etc.

All submitted models will be reviewed by the Model Board and we expect a dozen new models to be selected and added to the MCC collection. The authors of the selected models will be acknowledged on the Model Checking Contest web site.

All submitted models should be kept confidential until the list of selected models has been published. This is to ensure that the 2017 models are not known in advance by the tool developers participating in the Model Checking Contest.

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 are expected to become part of the public domain. If your model is proprietary, do not submit it. Detailed information is available from http://mcc.lip6.fr/rules.php.

Submission Details

A model can be either a "classical" P/T net, a Nested-Unit Petri net, or a colored Petri net (with/without guards on transitions, cartesian product on colors, and successor/predecessor functions). For a colored net, an equivalent "unfolded" P/T net may be provided as well.

A model may depend on one or many parameters that enable scaling (e.g., in the number of places, transitions, tokens, colors, etc.). To each parameterized model are associated as many "instances" (typically, between 2 and 20) as there are different combinations of values considered for the parameters of this model; each non-parameterized model has a single associated instance.

Detailed instructions for submission are given in the model submission kit.

To submit a model, four types of files should be provided:

Important Dates

Committees

General Chairs

Model Board

  • Fabrice Kordon - UPMC, France

    • Formula Board