Stochastic, Hybrid and Real-Time Systems: From Foundations To Applications with Modest
Abstract:
Our reliance on complex safety-critical or economically vital systems such as networked automation systems or “smart” power grids increases at an ever accelerating pace. The necessity to study the reliability and performance of these systems is evident, but purely functional models and properties are insufficient in many cases. This has led to the development of integrative approaches that combine probabilities, real-time aspects and continuous dynamics with formal verification.
Today, formal quantitative modelling and analysis is supported by a wide range of tools and formalisms. This variety of different language and tools, however, is a major obstacle for new users seeking to apply formal methods in their field of work.To overcome these problems, the Modest modelling language and its underlying semantic model of stochastic hybrid automata (SHA) have been designed as an overarching formalism of which many well-known and extensively studied models such as Markov decision processes, probabilistic timed systems or hybrid automata are special cases. The construction and analysis of SHA models is supported by the Modest Toolset, enabling a range of different analysis methods, ranging from safety verification for SHA, model checking of timed and probabilistic-timed systems, and simulation of stochastic timed automata.
The Modest Toolset has been used for a variety of applications including really cool safety critical hard real-time wireless control applications for bicycles, and innovative electric power grid control strategies.