首页 | 本学科首页   官方微博 | 高级检索  
     


A compositional modelling and analysis framework for stochastic hybrid systems
Authors:Ernst Moritz Hahn  Arnd Hartmanns  Holger Hermanns  Joost-Pieter Katoen
Affiliation:1. Saarland University – Computer Science, Campus E1 3, 66123, Saarbrücken, Germany
2. LS2: Software Modelling and Verification, RWTH Aachen University, 52056, Aachen, Germany
Abstract:The theory of hybrid systems is well-established as a model for real-world systems consisting of continuous behaviour and discrete control. In practice, the behaviour of such systems is also subject to uncertainties, such as measurement errors, or is controlled by randomised algorithms. These aspects can be modelled and analysed using stochastic hybrid systems. In this paper, we present HModest, an extension to the Modest modelling language—which is originally designed for stochastic timed systems without complex continuous aspects—that adds differential equations and inclusions as an expressive way to describe the continuous system evolution. Modest is a high-level language inspired by classical process algebras, thus compositional modelling is an integral feature. We define the syntax and semantics of HModest and show that it is a conservative extension of Modest that retains the compositional modelling approach. To allow the analysis of HModest models, we report on the implementation of a connection to recently developed tools for the safety verification of stochastic hybrid systems, and illustrate the language and the tool support with a set of small, but instructive case studies.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号