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.

The benchmarks on which tools will be assessed are colored Petri nets and P/T nets. A novelty of the MCC 2015 is that some P/T nets are provided with additional information giving a hierarchical decomposition into sequential machines (see the description of Nested-Units Petri nets). Tools may wish to exploit this information to increase performance and scalability.

IMPORTANT: this year, we will process tools on Virtual machines configured with 4 cores and 4 GByte per core. Planned confinement is 60 minutes per run (one examination on one instance of a model).

Important — Update of the image disk provided for submission (April 13, 2015)

Please note that on April 23, 2015, the virtual machine has been updated with the following items:

• Some models have been corrected (erroneous colored markings outlined by some tool developpers)
• The final set of formula for «known» models is out.

You may integrate this upgrade in he following ways:

• either download the new image disk (in the update submission kit), set your binary files into $HOME/BenchKit/bin (when logged as mcc) and replace the defautl BenchKit_head.sh there by yours,
• or download the updated model archive and untar it in your current VM from $HOME (when logged as mcc).

Call for Tools

Important: it is not necessary to have submitted one or many models to the MCC to submit a tool.

The Model Checking Contest is organized in successive steps: after the first step (Call for Models), we launch the Call for Tools, and thus, the Contest itself.

Models processed in this edition are divided in two categories. First, «known» models that are built from the ones used in the past editions. Then «surprise» models ; these will not be published before the tools are submitted. «small instances» of «known» models will be used as a qualification process for submitted tools.

Procedure to Submit One (or Many) Tool(s)

The procedure to submit tool(s) is explained below step by step.

Step 1: initiate the submission

You first have to download the Tool Submission Kit containing all material and instructions for tool integration. It contains a document describing the way formulas are handled this year. More information about formulas (BNF of grammars, as well as formulas themselves) will be provided as soon as possible (we are working on a formula generator that tries to avoid trivially checked formulas).

Meanwhile, an archive with a set of formulas for the first instance of each model is provided to let tools developers test their formula parsers. These formulas are not the definitive ones but do respect the very same syntax.

Step 2: prepare the disk-image to be submitted

You have to integrate your tool in the disk image to be executed in a virtual machine. Please note that you may put several tools (or versions of your tool if you want to submit several variants) in the same image (see the instructions in the tool submission manual).

To install extra software, you have access to the root account in this VM (see documentation). You should install your stuff in the mcc home directory (see documentation). Instructions to perform these operations are provided in the tool submission kit manual located in the Tool Submission Kit.

All the required information concerning formulas is provided in the formula manual located in the Tool Submission Kit. Some changes have been made since last year (based on the discussions that took place in Tunis) but the format remains close to what was done in the past. Please note that if formulas are provided in both XML and textual format, a parser is provided for XML only, the text being a way for a human to read formulas easily.

Step 3: finalize the submission

You have to upload a zipped version of your disk image. To initiate the process, please contact Fabrice Kordon via this link (you must provide the name of your tool) to get an access to a location where you may update your VM (this location is dedicated to you only). You will then receive detailed instructions for uploading.

Deadlines

The deadlines for submission of tools for the Model Checking Contest are

• Opening of the call : February 13, 2015 (the call, manual for integrating formulas, list of «known» models),
• First draft set of formulas : March 13, 2015 (formulas for the first instance of «known» models),
• Delivery of formulas : April 2, 2015 (all formulas for this year for «known» models),
• Tool submission : April 30, 2015,
• «Suprise» models : May 30, 2015 (together with their formulas).