Statistical model checking of dynamic networks of stochastic hybrid automata

Alexandre David, Kim G. Larsen, Axel Legay, Danny Bøgsted Poulsen

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

14 Citationer (Scopus)

Abstract

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 repeated output races between the dynamic evolving components of a system. As specification language we present a quantified extension of the logic Metric Temporal Logic (MTL). As a main contribution of this paper, the statistical model checking engine of UPPAAL has been extended to the setting of dynamic networks of hybrid systems and quantified MTL. We demonstrate the usefulness of the extended formalisms 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.

OriginalsprogEngelsk
TidsskriftElectronic Communications of the EASST
Vol/bind66
ISSN1863-2122
DOI
StatusUdgivet - 2013

Fingeraftryk

Dyk ned i forskningsemnerne om 'Statistical model checking of dynamic networks of stochastic hybrid automata'. Sammen danner de et unikt fingeraftryk.

Citationsformater