Introduction

The Model Checking Contest @ PETRI NETS aims at evaluating tools for the modeling and model checking of concurrent systems. The now traditional examinations mostly focus on some performance aspects (e.g. covering of some type of properties, time and memory consumption, etc.). The objective of the "live event" is to consider another aspect of tools: their usability for the design of and analysis of models. In particular, we focus on:

• Usability (including documentation aspects),
• Easy installation,
• Capability of the formalism for modeling,
• Ergonomic aspects,
• etc.

This event is opened to teams of advanced students or researchers that would select a tool to use (among the ones which participated in the Model Checking Contest and agreed to also participate in the "live event"). They will have a limited time to solve a problem presented at Milano during the conference.

The "live event" will take place in Milano on June 25, 2013, from 9h00 to 15h00. We will handle 12 teams at most. Results will be given during the Banquet dinner on June 27, 2013 in the evening.

Participating teams will have to model a problem and evaluate its properties in a textual report. To do so, they will use one of the proposed tool. Le "Live Event" will nominate the best study of the problem on the one hand, and the most appreciated tool among the ones that were used, on the other hand.

Participating tools

So far, the following tools have accepted to participate:

• Alpina (Univ. Geneva, Switzerland): it is an Eclipse plug-in,
• cunf (École Normale Supérieure de Cachan): it can be used either as a standalone tool or integrated with the CosyVerif environment,
• ITS-Tools (Univ. P. & M. Curie, France): it is an Eclipse plug-in,
• lola (Univ. Rostock, germany): as a standalone tool or in UML2oWFN,
• marcie (Univ. Cottbub, germany): this model checker comes with the snoopy environment,
• pnxdd (Univ. P. & M. Curie, France): it comes with the CosyVerif environment.
• sara (Univ. Rostock, germany): as a standalone tool or online,

The idea is to have at least one team per participating tool.

Registering to the MCC'2013 Live Event

To cope with organization matters, participating teams must register to Fabrice Kordon before June 15, 2013.

IMPORTANT: each team must select the tool they will use, when registering to the MCC'2013 Live Event.

Organization of the MCC'2013 Live Event

The procedure of the MCC'2013 live event will be:

• 09h00: distribution of the textual specifications of the problem to be solved,
  • Each team must model the problem with the selected tool and check for its properties,
  • At least, each team must try to solve the proposed properties
  • Each team must also report about the modeling and verification into a questionnaire form also provided at the beginning of the event.
• 15h00: teams deliver a report and also answer questions about the tool they use,
• 15h30: Presentation of the results of the Model Checking Contest.

A computer room will be available on site. Teams may also use their own computers.

Evaluation criteria

Evaluation criteria for the modeling and analysis of the problem are:

• Readability of models,
• Correctness of the models with regards to the specification,
• How comfortable the input notation is,
• etc.

Evaluation criteria for tools are:

• How ergonomic the tool is,
• How easy to install (if needed) the tool is,
• How clear the documentation is,
• How easy results are interpreted,
• etc.