Reachability Analysis for Stochastic Hybrid Systems

我们的社会和经济依赖于高度动态和复杂的安全关键系统的良好运行。用户需要能够对此类系统的操作给予高度信任。然而，环境中的不确定性、安全问题以及物理设备中的错误对它们的可靠运行构成了严重威胁。为了提高可靠性，形式化方法旨在提供建模方法和相应的分析技术来检查此类系统的行为。随机混合模型非常适合于自然地模拟各种相关的真实世界系统，其中离散和连续的行为以及随机方面需要被结合考虑。然而，这些模型的表现力将他们的分析变成了一项极具挑战性的任务，目前只有少数方法和工具可用。这种方法利用抽象和近似，计算结果的精度随着模型规模的增大而显著下降。本项目的主要目的是基于分别分析随机混合模型的确定性和随机性的思想，为随机混合模型的可达性分析提供更好的算法方法和工具支持。这一思想以前已经在随机混合Petri网的背景下进行了研究。该项目结合了项目合作伙伴在可达性分析、概率系统和混合Petri网的随机扩展方面的经验，旨在实现这些领域之间的协同效应：我们的目标是首先对模型的非随机部分进行组合可达性分析，然后通过多维集成在第二步重新集成随机模型演化的各个方面。为此，我们将开发基于自动机的随机混合模型的分析技术，并通过提供一种变换将它们的适用性扩展到基于Petri网的模型。除了随机混杂系统之外，我们项目中的模块还将在一定程度上产生双重影响，并增加非随机混杂系统的可达性分析的能力。除了理论上的发展，我们还致力于这些方法的实施和严格的评估。首先，所产生的实施应该为最终用户提供一个可执行的工具，但它也应该作为一个可扩展的软件框架，用于进一步核查方法的快速原型实施。在整个项目中，所开发的方法将在安全关键系统领域的典型案例研究和基准上进行测试。

Our society and economy rely on the well-operation of highly dynamic and complex safety-critical systems. Users need to be able to place a high level of trust in the operation of such systems. However, uncertainty in the environment, security issues, as well as errors in physical devices pose a serious threat to their reliable operation.To increase reliability, formal methods aim at providing modeling approaches and corresponding analysis techniques to examine how such systems behave. Stochastic hybrid models are well-suited to naturally model a wide range of relevant real-world systems, where discrete and continuous behavior as well as random aspects need to be considered in combination. However, the expressivity of such models turns their analysis to a highly challenging task, for which currently only a few methods and tools are available. Such methods make use of abstraction and approximation and the accuracy of the computed results decreases significantly with the size of the model at hand.Our main objective in this project is to provide better algorithmic approaches and tool support for the reachability analysis of stochastic hybrid models, building on the idea to separately analyse the deterministic and the stochastic behavior of such models. This idea has previously been investigate in the context of stochastic hybrid Petri nets. Petri nets are well-suited to model concurrent behaviour and naturally exhibit a large degree of compositionality.The project combines the experience of the project partners on reachability analysis, probabilistic systems and stochastic extensions of hybrid Petri nets aiming at synergy effects between these areas: our aim is to first develop a compositional reachability analysis for the non-stochastic part of the model and to reintegrate the aspects of the stochastic model evolution in a second step via a multi-dimensional integration. We expect this approach to yield an increased efficiency and extended applicability for a larger class of supported models.To do so, we will develop analysis techniques for automata-based stochastic hybrid models and extend their applicability to Petri-net-based models by offering a transformation. In addition to stochastic hybrid systems, modules of our project will partly have double impact and increase also the power of reachability analysis for non-stochastic hybrid systems.In addition to the theoretical developments, we aim at the implementation and rigorous evaluation of these methods. In the first place, the resulting implementation should provide an executable tool for end-users, but it should also serve as an extensible software framework for the fast prototypical implementation of further verification methods. Throughout the project the developed methods will be tested on characteristic case studies and benchmarks from the field of safety-critical systems.