Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.14581 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911009862582272 |
|---|---|
| author | Blohm, Pauline Schulz, Felix Willemsen, Lisa Remke, Anne Herber, Paula |
| author_facet | Blohm, Pauline Schulz, Felix Willemsen, Lisa Remke, Anne Herber, Paula |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_14581 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata Blohm, Pauline Schulz, Felix Willemsen, Lisa Remke, Anne Herber, Paula Systems and Control 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. |
| title | Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2506.14581 |