Dear colleagues,
This is important for the community to enrich the benchmark of the Model
Checking Contes.
So, do not hesitate to submit your models… Moreover, if you plan to submit a
tool, submitting some
of your benchmark models is of interest to see haw other tool do compete with
these ;-).
===========================================================
MODEL CHECKING CONTEST 2017 - (1/2) - CALL FOR MODELS
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:
- the present Call for Models (http://mcc.lip6.fr/cfm.php),
- the Call for Tools (http://mcc.lip6.fr/cft.php),
- and the Contest itself.
CALL FOR MODELS
At the core of the Model Checking Contest is a collection of models
(http://mcc.lip6.fr/models.php) 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
available from http://mcc.lip6.fr/archives/ModelSubmissionKit.tar.gz.
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 are provided. For information about
the PNML format, please refer to the web site http://www.pnml.org and
contact [email protected] if help is needed. For information
about Nested-Unit Petri nets, please refer to http://mcc.lip6.fr/nupn.php
and contact [email protected] if help is needed.
- A LaTeX form that must be filled in to provide summary information about
the model, its origin, its size, etc. See http://mcc.lip6.fr/models.php
for examples of such a form.
- 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. These properties can be expressed informally in English or given
as XML files. Submitted properties, which are most useful to produce
meaningful benchmarks, will be reviewed by the Formula Board.
IMPORTANT DATES
Dec. 15, 2016: publication of the present Call for Models
Feb. 15, 2017: deadline for model submission
Apr. 15, 2017: individual notification of model acceptance/rejection
June 1, 2017: on-line publication of the selected MCC'2017 models
June 27, 2017: announcement of MCC'2017 results during the Petri Net
conference (Zaragoza, Spain)
COMMITTEES
General Chairs
Didier Buchs - Univ. Geneva, Switzerland
Fabrice Kordon - UPMC, France
Model Board
Hubert Garavel - Inria/LIG, France
Fabrice Kordon - UPMC, France
Lom Messan Hillah - Univ. Paris Ouest, France
Formula Board
Loïg Jezequel - Univ. Nantes, France
Emmanuel Paviot-Adet - Univ. Paris 5, France
César Rodriguez - Univ. Paris 13, France
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
