The MoDeST Tool Environment
H. Bohnenkamp, J.-P. Katoen, H. Hermanns (Univ. d. Saarlandes), P. R. D'Argenio (Univ. Nacional de Córdoba, AR)
The specification language modest covers a wide spectrum of modelling concepts, ranging from plain labelled transition systems to stochastic systems like Generalised Semi-Markov Decision Processes. modest possesses a rigid, process-algebra style semantics, and yet provides modern and flexible specification constructs. modest specifications constitute a coherent starting-point to analyse distinct system characteristics with various techniques, e.g., model checking to assess functional correctness and discrete-event simulation to establish the system's reliability. Analysis results thus refer to the same system specification, rather than to different (and potentially incompatible) specifications of system perspectives like in the UML.
The tool motor (modest Tool enviRonment) is aimed to provide the means to analyse and evaluate modest specifications. The tool is written in the C++ programming language. The tool provides (i) interfacing capabilities for connection to existing tools for specific projected models, and (ii) also means for enhancement by native algorithms for analysis of (classes) of modest specifications. In earlier work, motor has been connected to möbius, a performance evaluation tool suite that has been developed at the University of Illinois at Urbana-Champaign, US. Currently we are working on a state-space generator for modest and aim at connecting modest via motor to the PRISM tool, a model-checker for probabilistic timed systems, developed at the University Birmingham, UK. Furthermore, we plan to connect modest to the UPPAAL model checker.
H. Bohnenkamp, J.-P. Katoen, H. Hermanns (Univ. d. Saarlandes), P. R. D'Argenio (Univ. Nacional de Córdoba, AR)
The specification language modest covers a wide spectrum of modelling concepts, ranging from plain labelled transition systems to stochastic systems like Generalised Semi-Markov Decision Processes. modest possesses a rigid, process-algebra style semantics, and yet provides modern and flexible specification constructs. modest specifications constitute a coherent starting-point to analyse distinct system characteristics with various techniques, e.g., model checking to assess functional correctness and discrete-event simulation to establish the system's reliability. Analysis results thus refer to the same system specification, rather than to different (and potentially incompatible) specifications of system perspectives like in the UML.
The tool motor (modest Tool enviRonment) is aimed to provide the means to analyse and evaluate modest specifications. The tool is written in the C++ programming language. The tool provides (i) interfacing capabilities for connection to existing tools for specific projected models, and (ii) also means for enhancement by native algorithms for analysis of (classes) of modest specifications. In earlier work, motor has been connected to möbius, a performance evaluation tool suite that has been developed at the University of Illinois at Urbana-Champaign, US. Currently we are working on a state-space generator for modest and aim at connecting modest via motor to the PRISM tool, a model-checker for probabilistic timed systems, developed at the University Birmingham, UK. Furthermore, we plan to connect modest to the UPPAAL model checker.