The demands on the functionality and flexibility of embedded control systems are steadily increasing. At the same time, they are more and more used in critical infrastructures, for example, controlling the supply of energy or water, and in safety-critical systems such as self-driving cars and other autonomous vehicles. With that, we increasingly use embedded control systems not only for our convenience or for profit, but also trust our lives and personal well-being to these systems. At the same time, learning components are nowadays often used to cope with dynamic environments. This makes it crucial to ensure the safety, performance, and resilience of these systems under all circumstances. Qualitative analysis techniques such as deductive verification can provide safety guarantees for hybrid systems, however, they typically only consider the worst case scenario. In contrast, quantitative analysis techniques like analytical reachability analysis or statistical model checking (SMC) can provide statistical guarantees for safety or performance properties even in the presence of uncertainty, however, they might not provide guarantees for all possible scenarios.
The integration of learning components and uncertainties further complicates formal verification of hybrid systems. Qualitative analysis techniques often rely on abstractions, such as contracts, to handle learning components or uncertainties. While these abstractions are necessary to provide safety guarantees, they usually abstract from all quantitative information, yielding imprecise and overly pessimistic results. In contrast, quantitative techniques exploit statistical information like the distribution of events or failure and repair times. However, they suffer from state-space explosion, in particular if learning components have to be verified to ensure safety under all circumstances or with high accuracy. Furthermore, quantitative analyses techniques typically do not provide us with PhD Symposium of the 19th International Conference on Integrated Formal Methods (iFM) at the University of Manchester, UK, 12 November 2024. Envelope pauline.blohm@uni-muenster.de (P. Blohm); paula.herber@uni-muenster.de (P. Herber); anne.remke@uni-muenster.de (A. Remke) techniques for modular reasoning.
To ensure the safety and resilience of hybrid systems even in the presence of learning and in uncertain environments, we aim at combining the strengths of qualitative analysis with the strength of quantitative analysis. We focus on hybrid systems modelled in Simulink as it is widely adopted for embedded control systems that combine discrete and continuous behavior. Previous work of one of the co-authors has presented an approach for a qualitative analysis of Simulink models via a transformation to Differential Dynamic Logic (dL) [1,2] which is implemented in the tool Simulink2dL. The resulting dL Model can then be analyzed using Deductive Verification to obtain formal guarantees that a system satisfies a given Safety Property. Our aim is to complement this with efficient and scalable quantitative analysis [3,4,5] and also to combine these techniques to provide an approach for comprehensive safety, resilience and performance analysis for intelligent hybrid systems. The concept of the thesis is shown in Fig. 1 and consists of four main parts:
1. We plan to provide an automated transformation Simulink2SHA from Simulink to Stochastic Hybrid Automata. With this transformation, we define a formal semantics for Simulink, and it gives us access to established Quantitative Analysis techniques, such as reachability analysis or (statistical) model checking.
the Simulink model to model uncertainties like component failure or sensor noise. With that, we can also investigate resilience and performance of a model under verification. 3. We aim at investigating how Qualitative and Quantitative Properties for the dL and SHA models can be derived from safety, resilience and performance requirements. 4. We plan to provide a technique to combine Qualitative Analysis results (e.g. from deductive verification) with a Quantitative Analysis for (potentially learning) Simulink models. In particular, we aim at investigating two different approaches: a) the integration of shielded SMC-based learning, which has been proposed by one of the co-authors in previous work [6], and b) the use of contracts or other domain-specific abstractions to safely integrate learning components, as has been proposed by two of the co-authors in [2,7].
As a first step, we have presented an approach for a manual transformation from Simulink to SHA, which has been accepted at iFM 2024 [8]. Open research problems we plan to address in this thesis are how to model uncertainties such that the resulting models are still analyzable, how to capture qualitative and quantitative properties of intelligent systems appropriately and also how to combine qualitative with quantitative analysis techniques for SHA with learning components. One key challenge is that, while modular reasoning would be highly desirable to handle complex systems, there exists no established concept to include quantitative and statistical information in contracts.
There have been quite some efforts to enable the formal verification of systems that are modeled in Simulink [9,10,11,12,13,14,15]. Yet, all of these approaches, including the Simulink Design Verifier [16], are limited to discrete subsets of Simulink. Formal verification methods that support hybrid systems modeled in Simulink are, e.g., proposed in [1,17,18,19,20,21]. However, they either focus on techniques for a special class of systems and do not provide general transformation rules for a broader set of blocks or focus on the qualitative analysis of safety properties and they neither take stochastic components nor learning into consideration.
There also has been a number of works on statistical model checking (SMC) for Simulink, for example [22,23,24]. Still they do not provide a stochastic model with formal semantics and thus cannot make use of more advanced quantitative analysis techniques. In [25], the authors propose a transformation from Simulink into stochastic timed automata (STA) and perform SMC with UPPAAL SMC on the resulting network of STA. However, they do not consider stochastic blocks and transform a given Simulink model into a deterministic STA model where all probabilities are one.
There also exists a broad variety of approaches to formally ensure safety of learning components using shielding or runtime monitoring [26,27,28]. These approaches do not directly support Simulink though, and they do not consider formal analysis techniques that take stochastic failures and learning into account.
Uppaal Stratego [29] uses priced timed automata to model stochastic behavior, and provides tooling for statistical model checking [30], timed games [31] and learning-based strategy synthesis [32]. While Uppaal Stratego comes with a graphical interface and is designed for usability, the underlying formalisms are less expressive than stochastic hybrid automata, in particular w.r.t. continuous system behavior governed by differential equations and controlled by continuous and stochastic variables.
Finally, there has been some work on combining rigorous formal and statistical methods. In [33], the authors incorporate statistical hypothesis testing to compute promising configurations of program verifiers automatically. However, they do not support hybrid systems, and they do not consider both safety and performance properties. In [34], the authors present a formal framework for an integrated qualitative and quantitative model-based safety analysis. However, they do not support hybrid systems and do not consider deductive verification methods.
The first step towards safe and resilient hybrid system is enabling a quantitative analysis for (stochastic) Simulink models. As Simulink does not offer elaborate quantitative analysis, such as reachability analysis or statistical model checking, a transformation into a formal model is desired. To tackle this problem, we are currently working on a modular approach to transform Simulink models into SHA. In [8], we present an approach that enables us to transform a subset of Simulink models to SHA and analyze the SHA using the tool RealySt [3] to obtain reachability probabilities for critical safety properties. This is an important first step towards ensuring safety and resilience of hybrid systems in the presence of uncertainties. However, it still has some limitations, e.g. we only provide transformation rules for a subset of Simulink blocks and the parallel composition has to be performed manually. To tackle these limitations, we are currently working on a tool to automatically transform a given Simulink model to an SHA using the transformation rules provided in [8]. Additionally, we plan to define transformation rules for a larger subset of Simulink blocks and provide better support for the integration of stochasticity into Simulink models, e.g. by providing parameterized subsystems that model specific stochastic behaviour.
As next steps, we plan to address the research challenges defined above, namely the integration of stochastic and learning components in Simulink, the derivation of qualitative and quantitative properties that are important for safety, resilience and performance of intelligent Simulink models in uncertain and dynamic environments, and the development of combined quantitative and quantitative analysis techniques that enable us to formally analyze these properties.