Scope
Modelling techniques, aiming at the accurate description of systems
and their relevant properties, are typically developed with formal
analysis and formal verification in mind. To show that a developed
approach actually scales to real systems, large case studies are essential.
To share insight and information concerning the development of
models we regularly run workshops on Models for formal Analysis of
Real Systems (MARS). They focus the modelling effort itself, rather
than the subsequent analysis and verification.
This webpage provides not only links to the workshops, it also
presents all models presented at the workshops. The models come
free of charge and we encourage everybody to use them. New models and
adapted versions of existing models (e.g. same model in a different
formalism) are most welcome.
Please send your submission to
model-submission@mars-workshop.org.
photograph courtesy NASA
Workshops
The workshop aims at discussing lessons learnt while creating large
models. Examples are:
|
photograph courtesy NASA
Repository
The process of developing a detailed and accurate model usually takes
a large amount of time, often months or years; without even starting a
formal analysis. When publishing the results on a formal analysis in a
scientific paper, details of the model have to be skipped due to lack
of space.
The models presented during the MARS workshops are made available in a perennial form, so that they can be used by others and that the experiments are reproducible. The list of models is expected to grow as time passes, and to be as diverse as possible. The repository of models is hosted by Inria (France). |