if ($PAGE == -1) {
echo $LONGSECTION;
} else {
echo $longsections[$PAGE];
}
?>
Call for Model
The first step of the Model Checking Contest is a call for model. The
community (and not only tool developers) may propose models belonging to one
of the categories mentioned above. To do so, please respect the following
procedure.
- download the model submission kit;
- fill the DescModel.tex file to
provide information on the model, you may (if it has a meaning), provide a
picture as a pdf in the model-image.pdf file, please do not touch the
ModelForm.tex file, only fill the macros in the other latex file to
describe your model,
- Elaborate, for each scaling parameter of
your model, the following description files: PNML (If help is needed, please
contact our PNML technical expert: lom-messan.hillah@lip6.fr) for the corresponding P/T model
(mandatory), PNML for the colored model (if possible), non mandatory
properties files for each instance (typically, invariant and bounds) using the
format defined in the model description form (you also have to respect the
naming convention presented in the instructions)
- put all files in a folder, zip it, and send
it as an attached document to mcc-contest-committee@systeme.lip6.fr
The pdf version of the "Call for Model" is available here.
Deadline
The deadline for submission of model for the Model Checking Contest is
October 31, 2011.