2015/11/03 by Alexandre David, David, Alexandre, Kim G. Larsen +5
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · doi:10.14279/tuj.eceasst.66.893
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/15
In this paper we present a modelling formalism for dynamic networks of stochastic hybrid automata. In particular, our formalism is based on primitives for the dynamic creation and termination of hybrid automata components during the execution of a system. In this way we allow for natural modelling of concepts such as multiple threads found in various programming paradigms, as well as the dynamic evolution of biological systems. We provide a natural stochastic semantics of the modelling formalism based on re- peated output races between the dynamic evolving components of a system. As specification language we present a quantified extension of the logic Metric Tempo- ral Logic (MTL). As a main contribution of this paper, the statistical model checking engine of U PPAAL has been extended to the setting of dynamic networks of hybrid systems and quantified MTL. We demonstrate the usefulness of the extended for- malisms in an analysis of a dynamic version of the well-known Train Gate example, as well as in natural monitoring of a MTL formula, where observations may lead to dynamic creation of monitors for sub-formulas.