fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Call for Tools Participation
Last Updated
Apr. 26, 2013
Deadline extention up to May 6, 2013
Grammar for formulas has been fixed to allow quoted identifiers on Apr. 23, 2013
Please check for the last version of the disk image published on Apr. 17, 2013
Please check for the last version of BenchKit published on Apr. 17, 2013
The call for tool participation is closed

Procedure

After the call for model, the second call of the Model Checking Contest is the submission of Tools to be evaluated against the benchmark made of the MCC'2011 and MCC'2012 models, enriched with the models submitted during the first step of MCC'20123. To submit a tool, please respect the following procedure

Of course, you may add your own data in the disk image. Typically, you may want to install the models in your format if you do not use PNML.

CAUTION: to participate in the "surprise models" category, your tool must be able to load PNML since these will not be known in advance.

Once the disk image is ready, have it reachable via an URL you provide to us using this link .

To operate manually the virtual machine

If you can operate BenchKit, you may use it to run your tool on a local machine. However, when tuning your tool to the system, this may not be convenient.

Thus, you may use VirtualBox (Mac, PC under widowns) as well as qemu on a Linux machine by invoking the following command. The format of the provided disk image should be compatible with these two virtualization environment.

The command to be used by BenchKit for the MCC (under Linux) will be:

$ qemu-kvm -vnc :42 -enable-kvm -smp 1 -cpu host -daemonize -k fr -m 2048 -drive file=mcc2013.vmdk -redir tcp:2222::22

You may want to delete the -demonize option to get the default screen where outputs of your VM are propagated. You may also connect using a VNC server (port 42).

Be careful: it seems that some browser do not expand correctly the file. If you have troubles booting the disk image, please proceed as follow in a bash terminal:
   $ wget http://mcc.lip6.fr/archives/mcc2013.vmdk.bz2
   $ tar xjfv mcc2013.vmdk.bz2

To log in, you do:

$ ssh -p 2222 -i <bk-public-key> mcc@localhost

where <bk-public-key> is the name of the file containing the public key for mcc.

To copy files, you do:

$ scp -P 2222 <your files> mcc@localhost:<your target>

Executing the BenchKit_head.sh file in a realistic manner

BenchKit will operate your tool via a ssh on the mcc login. It will then operate a list of command that is sketched there:

export BK_INPUT="CSRepetitions-COL-02"
export BK_EXAMINATION="StateSpace"
export BK_TOOL="MyTool"
export BK_RESULT_DIR="/tmp"
export BK_LOG_FILE="$BK_RESULT_DIR/the_log_file".$$

# this is specific to your benchmark or test

export BIN_DIR="$HOME/BenchKit/bin"

# this is for BenchKit: explicit launching of the test

cd /home/mcc/BenchKit/INPUTS/CSRepetitions-COL-02
echo "====================================================================="
echo " Generated by BenchKit 1.0"
echo " Executing tool $BK_TOOL:"
echo " Test is $BK_INPUT, examination is $BK_EXAMINATION"
echo "====================================================================="
echo
echo "--------------------"
echo "content from stdout:"
echo
echo "START "`date +%s`
bash /home/mcc/BenchKit/BenchKit_head.sh 2> STDERR;
echo "STOP "`date +%s`
echo
echo "--------------------"
echo "content from stderr:"
echo
cat STDERR ;

Of course, environment variable values are replaces in the following way:

About the Properties to be Verified

Properties are already stored in the submission kit. All these properties could be used in the model checking contest, together with some new ones.

You can access to the information concerning properties to be evaluated during the evaluation procedure:

Deadline

The deadline for submission of tools for the Model Checking Contest is May 1st, 2013 May 6, 2013.