Reachability Analysis for Stochastic Hybrid Systems

随机混合系统的可达性分析

• 批准号: 471367371
• 负责人: Professorin Dr. Anne Remke
• 金额: --
• 依托单位: Fakultät für Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/471367371?language=en
• 关键词: Reachability; Analysis; Stochastic; Hybrid; Systems

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.

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