[ecoop-info] Call for models (Model Checking Contest 2016)

[Announcements of FME events]

MODEL CHECKING CONTEST 2016 - (1/2) - CALL FOR MODELS

http://mcc.lip6.fr

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 2016 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 2016 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 lom-messan.hillah at lip6.fr if help is needed. For information 
     about Nested-Unit Petri nets, please refer to http://mcc.lip6.fr/nupn.php
     and contact hubert.garavel at inria.fr 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

   Nov. 03, 2015: publication of the present Call for Models

   Jan. 30, 2016: deadline for model submission

   Apr. 15, 2016: individual notification of model acceptance/rejection

   June 1, 2016: on-line publication of the selected MCC'2016 models

   June 21, 2016: announcement of MCC'2016 results during the Petri Net
	conference (Torun, Poland)

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
	
	


--------------------------------------------------------------------------------------
Fabrice Kordon		
Université Pierre & Marie Curie
LIP6/MoVe, Bureau 26/25-212
4 place Jussieu, 75252 Paris Cedex 05
http://lip6.fr/Fabrice.Kordon/

-------------- next part --------------
_______________________________________________
events mailing list
events at fmeurope.org
http://fmeurope.hosting.west.nl/mailman/listinfo/events