Modelling and Description of Stochastic Timed Systems

The Modeling and Description Language for Stochastic and Timed Systems (Modest) is a specification formalism for the modelling and analysis of hybrid, real-time, distributed and stochastic systems. The language is rooted in classical process algebra, i.e. the specification of models is compositional. Basic activities are expressed with atomic actions, more complex behaviour with constructs for sequential composition, nondeterministic choice, parallel composition with CSP-style synchronisation, looping and exception handling. A special construct exists to describe probabilistic choice. Clocks, variables and random variables are used to describe stochastic real-time aspects. All constructs and language concepts have a pleasant syntax, inspired by Promela, LOTOS, FSP, and Java.

The Modest Toolset supports the modelling and analysis of Modest models. At the core of the toolset is the model of networks of stochastic hybrid automata (SHA) for which several variations of analysis are supported. Application cases studied with Modest span Zigbee Energy Consumption, Train Control Reliability, Lacquer Production Scheduling, and Electric Power Grid Stability, among others.