Towards Quantitative Analysis of Simulink Models Using Stochastic Hybrid Automata
摘要
Model-driven development frameworks such as MATLAB Simulink are widely used in industrial design processes to conquer the increasing complexity of embedded control systems such as self-driving cars or critical infrastructures. As these systems are often safety-critical, formal methods to ensure safety, performance and resilience are highly desirable, in particular also in the presence of unknown and uncertain environments. The semantics of Simulink is, however, only informally defined. In this paper, we present a modular approach to transform stochastic Simulink models to stochastic hybrid automata (SHA). Our key idea is threefold: 1) We provide transformation rules that map Simulink blocks to SHA templates, 2) we map distributed signal flow to a discrete event synchronization mechanism, and 3) we present a parallel composition algorithm. Our transformation gives us access to established quantitative analysis techniques such as reachability analysis and statistical model checking. We show the feasibility of our approach using a temperature control system with a stochastic failure and repair model.