University of Saarbrücken (Germany)
Transformation, analysis and validation of MODEST models
CADP (Construction and Analysis of Distributed Processes)
MODEST (Modeling and Description Language for Stochastic and Timed
Systems) is a specification formalism for describing stochastic
real-time systems. The language has a process algebraic flavour,
promoting the compositional specification of models. Basic activities
are expressed with atomic actions, more complex behaviour with
constructs for sequential composition, nondeterministic choice,
parallel composition with CSP-like synchronization, looping and
exception handling. Quantitative aspects are described using
probabilistic choice, clocks, variables, and random variables. The
syntax is user-friendly, being inspired from Promela, LOTOS, FSP,
and JAVA. MODEST is equipped with a structural operational semantics
mapping programs to stochastic timed automata. The language allows to
describe a wide variety of models, including: ordinary labelled
transition systems, timed automata, probabilistic automata,
stochastic automata, Markov decision processes, and various
combinations thereof. The philosophy underlying MODEST is to describe
a system with one single model and to analyze it by extracting
simpler models that are tailored to the specific properties of
Tool support is essential in order to facilitate the analysis of the different models. MOTOR (MODEST Tool Environment) is a software tool that implements the MODEST semantics and plays a central role in the analysis of MODEST models. The tool works by simplifying and specializing MODEST models using a macro-processor and translating or adapting the models in a way such that the actual analysis work can be carried out by third-party tools, such as PRISM, UPPAAL, or CADP. MOTOR provides two programming interfaces: the AST API, which gives the programmer access to the abstract syntactic representation of the MODEST specification, and the FSNS API, which allows convenient state space exploration by means of first-state/next-state primitives. These two APIs enable modular design and extendability of MOTOR, the former for translation-oriented transformations and the latter for state-oriented approaches. A connection to CADP exists, which allows model checking of untimed, non probabilistic MODEST models.
For handling quantitative analysis, MOTOR is connected to the MÖBIUS performability evaluation environment. MÖBIUS was designed as an integrated tool environment for the analysis of performability and dependability models. It allows specification of models in different formalisms (e.g., Petri net-like formalisms or Markovian process algebra) and provides efficient discrete-event simulation capabilities and numerical solvers, such as Markov chain solvers. The connection of MOTOR to MÖBIUS is achieved by a direct mapping from MODEST constructs onto the programming interface of MÖBIUS, which is quite close to the FSNS API of MODEST. This connection enables the user to perform simulation of MODEST models and to gather performability results.
Compared to other existing discrete-event simulation tools, MODEST
has the advantage of being equipped with a formal semantics. This
ensures the well-definedness of the underlying stochastic model used
for simulation, and makes the simulation results trustworthy, given
that discrete-event simulation is a well-understood technique.
In addition, MODEST provides formal verification capabilities by its
interconnection to specialized tools, such as PRISM, UPPAAL and CADP.
Henrik Bohnenkamp, Holger Hermanns, and Joost-Pieter Katoen.
"Motor: The Modest Tool Environment". In Orna Grumberg and Michael
Huth, editors, Proceedings of the 13th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems
TACAS'2007 (Braga, Portugal), Lecture Notes in Computer Science
volume 4424, pp. 500-504, March 2007.
Full version available from our FTP site in PDF or PostScript
[Hartmanns-Hermanns-Katoen-11] Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. "Probabilistic Analysis of Embedded Systems". In Industrial Handbook, pp. 184-200, Quasimodo Project Deliverable 5.21, 2011.
Available on-line at: http://people.cs.aau.dk/~kgl/China2011/Slides/QuasimodoHandbook.pdf
or from our FTP site in PDF or PostScript
Department of Computer Science
Bldg. E1 3, Room 501
Tel: +49 681 302 5631
Fax: +49 681 302 5636
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|