MODEL CHECKING CONTEST 2019 - (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 the fairest comparison possible 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 <http://mcc.lip6.fr/cfm.php>), - the Call for Tools (http://mcc.lip6.fr/cft.php <http://mcc.lip6.fr/cft.php>), - and the Contest itself. NOVELTY IN 2019 The MCC will jointly take place with the TOOLympics 2019, that will gather a dozen established competitions to celebrate their achievements in the field of Tools and Algorithms for the Construction and Analysis of System (TACAS). The MCC will be part of TOOLympics as one of the involved competitions, in Prague, April 6-7, 2019. Consequently, participants of the MCC should pay close attention to the deadlines in the calls as they occur very early for the 2019 edition. CALL FOR MODELS At the core of the Model Checking Contest is a collection of models (http://mcc.lip6.fr/models.php <http://mcc.lip6.fr/models.php>) accumulated from the previous editions of the contest. This collection currently comprises 90 different models, which have been already used and cited in more than 67 scientific publications. For the 2019 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 2018 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 <http://mcc.lip6.fr/rules.php>. SUBMISSION DETAILS A model can be either a "classical" P/T net[1], a Nested-Unit Petri net [2,3], or a colored Petri net [4,5,6] (with/without guards on transitions, cartesian product on colors, and successor/predecessor functions). For a colored net, an equivalent "unfolded" P/T net [7] 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 <http://mcc.lip6.fr/archives/ModelSubmissionKit.tar.gz>. To submit a model, four types of files should be provided, two of which are required. Required files: - A PNML [8,9] 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 <http://www.pnml.org/> and contact [email protected] <mailto:[email protected]> if help is needed. For information about Nested-Unit Petri nets, please refer to http://mcc.lip6.fr/nupn.php <http://mcc.lip6.fr/nupn.php> and contact [email protected] <mailto:[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 <http://mcc.lip6.fr/models.php> for examples of such a form. Recommended files: - 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 - Sept. 10, 2018: publication of the present Call for Models - Nov. 23, 2018: deadline for model submission (for the MCC'2019) - Dec. 4, 2018: individual notification of model acceptance/rejection - Jan. 31, 2019: on-line publication of the selected MCC'2019 models - April 6-7, 2019: announcement of MCC'2019 results during the TOOLympics 2019 at TACAS'19 (Prague, Czech Republic). COMMITTEES General Chairs Didier Buchs - Univ. Geneva, Switzerland Fabrice Kordon - Sorbonne Université/LIP6, France Model Board Hubert Garavel - Inria/LIG, France Lom Messan Hillah - Univ. Paris Nanterre, France Fabrice Kordon - Sorbonne Université, France Formula Board Loïg Jezequel - Univ. Nantes, France Emmanuel Paviot-Adet - Univ. Paris 5, France César Rodriguez - Univ. Paris 13, France REFERENCES [1] C. A. Petri and W. Reisig. Petri net. Scholarpedia, 3(4):6477, 2008. Online. http://www.scholarpedia.org/article/Petri_net <http://www.scholarpedia.org/article/Petri_net> [2] H. Garavel. Nested-unit petri nets: A structural means to increase efficiency and scalability of verification on elementary nets. In Petri Nets, volume 9115 of Lecture Notes in Computer Science, pages 179–199. Springer, 2015. [3] NUPN manual page. Online. http://cadp.inria.fr/man/nupn.html <http://cadp.inria.fr/man/nupn.html> [4] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Computers, 42(11):1343–1360, 1993. [5] ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 1: Concepts, definitions and graphical notation. ISO/IEC 15909-1:2004, 2004. [6] ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 1: Concepts, definitions and graphical notation, AMENDMENT 1: Symmetric Nets. ISO/IEC 15909-1:2004/Amd.1:2010, 2010. [7] F. Kordon, A. Linard, and E. Paviot-Adet. Optimized colored nets unfolding. In FORTE, volume 4229 of Lecture Notes in Computer Science, pages 339–355. Springer, 2006. [8] SO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 2: Transfer format. ISO/IEC 15909-2:2011, 2011. [9] L. M. Hillah, E. Kindler, F. Kordon, L. Petrucci, and N. Trèves. A primer on the Petri Net Markup Language and ISO/IEC 15909-2. Petri Net Newsletter, 76:9–28, Oct. 2009. -------------------------------------------------------------------------------------- Fabrice Kordon Sorbonne Université Campus Pierre & Marie Curie LIP6/MoVe, Bureau 26/25-212 4 place Jussieu, 75252 Paris Cedex 05 http://lip6.fr/Fabrice.Kordon/ <http://lip6.fr/Fabrice.Kordon/>
---- [[ 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] ]]
