Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata

TL;DR

This paper introduces a formal analysis method for Simulink models incorporating uncertainties, using stochastic hybrid automata to enable safety and performance evaluation through quantitative techniques.

Contribution

It extends the semantics of Simulink with stochastic hybrid automata to model uncertainties and applies formal analysis methods to embedded control systems.

Findings

Effective modeling of uncertainties as stochastic subsystems

Formal semantics extension enables safety analysis

Case studies demonstrate practical applicability

Abstract

Simulink is widely used in industrial design processes to model increasingly complex embedded control systems. Thus, their formal analysis is highly desirable. However, this comes with two major challenges: First, Simulink models often provide an idealized view of real-life systems and omit uncertainties such as, aging, sensor noise or failures. Second, the semantics of Simulink is only informally defined. In this paper, we present an approach to formally analyze safety and performance of embedded control systems modeled in Simulink in the presence of uncertainty. To achieve this, we 1) model different types of uncertainties as stochastic Simulink subsystems and 2) extend an existing formalization of the Simulink semantics based on stochastic hybrid automata (SHA) by providing transformation rules for the stochastic subsystems. Our approach gives us access to established quantitative analysis techniques, like statistical model checking and reachability analysis. We demonstrate the applicability of our approach by analyzing safety and performance in the presence of uncertainty for two smaller case studies.