Database of Research Tools Developed Using CADP

MOTOR (MODEST Tool Environment)

Organisation: University of Saarbrücken (Germany)

Functionality: Transformation, analysis and validation of MODEST models

Tools used: CADP (Construction and Analysis of Distributed Processes)
Möbius

Period: 2007

Description: 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 interest.

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.

Conclusions: 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.

Publications: [Bohnenkamp-Hermanns-Katoen-07] 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 the CADP Web 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 the CADP Web site in PDF or PostScript

Contact:
Holger Hermanns
Saarland University
Department of Computer Science
Campus Saarbrücken
Bldg. E1 3, Room 501
66123 Saarbrücken
Tel: +49 681 302 5631
Fax: +49 681 302 5636
Email: [email protected]
Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Last modified: Thu Feb 11 12:23:11 2021.

Back to the CADP research tools page