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
- download the tool submission documentation,
- Since the MCC'2013 relies on BenchKit, you should have a look there,
- a disk mage is ready for you with all the required elements (except for
"surprise models") installed. You may access it here.
If you want to use your own disk image, please find here an archive with all models data (but the "surprise models"), this archive is to be uncompressed in the home directory of the mcc user, - and of course the flyer for this call here.
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:
- the "property manual",
- the ANTLR BNF,
- the XML metamodel.
Deadline
The deadline for submission of tools for the Model Checking Contest is
May 1st, 2013 May 6, 2013.