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:
- Which formalism is chosen, and why?
- Which abstractions have to be made and why?
- How are characteristics of the system modelled?
- Were there any complications while modelling?
- How is the accuracy of the model measured?
The workshops emphasise modelling over verification. In particular, we usually
invite papers that may lay the basis for future formal analysis.
The workshops bring together researchers from different communities that all
aim at verifying real systems and are developing formal models for such systems.
|
|
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).
|