FMT - UT


ITA - KUN


Philips


Progress

The General Purpose Specification Language MoDeST

Modest is a specification language for probabilistic, stochastic, and timed systems. Its purpose is to provide a single framework from which different semantical models can be derived from. Among the target formalisms are the following:
  • Labelled transition systems
  • Probabilistic transition systems (Markov decision processes)
  • Timed automata
  • Probabilistic timed automata
  • Discrete- and Continuous-time Markov chains
  • Interactive Markov chains
  • Generalized Semi-Markov processes
  • Stochastic Automata
The MoDeST language has been influenced by some other languages that have been around some time. There are some similarities to Promela, the specification language for the verification environment SPIN. The language is also influenced by FSP, as described in "Kramer/McGee: Concurrency: State Models and Java Programs". There is a touch of CSP and LOTOS in it, when it comes to parallelism and synchronsiation, but also traces of ACP can be found. The description of the timed behaviour is influenced by Timed Automata and UPPAAL. The description of the stochastic behaviour has some similarities to SPADES.

The design objective of MoDeST is: from everything just the best.

MoDeST has a well defined formal semantics, which is described in D'Argenio, Hermanns, Katoen, Klaren: MoDeST - A Modelling and Description Language for Stochastic Timed Systems.

The MoDeST Tool

The MoDeST Tool is supposed to provide a representation of MoDeST specifications in software. The architecture of the MoDeST Tool is to provide an API which provides all information about the considered MoDeST model. This API is supposed to be used by other software modules which bridge to other tools: verification tools or simulators. Currently we plan to develop modules for the following target tools:
  • CADP, a software suite for the modeling and verification of distributed systems.
  • ETMCC, a model checker for CTMCs
  • UPPAAL, a model checker for timed automata

Status Quo

Currently, the MoDeST tool has the following capabilities:
  • An interactive command line interface to the user. The user is presented a list of enabled transitions. The user can choose a transition which has to be fired next.
  • A state space generator which produces labelled transition systems in either BCG, Dot, or plain ascii format. The BCG format allows already a connection to the verification tools provided by the CADP suite.
  • a compiler which translates Modest specifications in C++, which are then linked to Mobius. Mobius is the used to simulate Modest models.



May 6, 2004
Henrik Bohnenkamp