Title: A Service-Oriented Approach for Decomposing and Verifying Hybrid System Models
Abstract: The design of fault free hybrid control systems, which combine discrete and continuous behavior, is a challenging task. Their hybrid behavior and further factors make their design and verification challenging: These systems can consist of multiple interacting components, and commonly used design languages, like MATLAB Simulink do not directly allow for the verification of hybrid behavior. By providing hybrid contracts, which formally define the interface behavior of hybrid system components in differential dynamic logic ( ), and providing a decomposition technique, we enable compositional verification of Simulink models with interacting components. This enables us to use the interactive theorem prover KeYmaera X to prove the correctness of hybrid control systems modeled in Simulink, which we demonstrate with an automotive industrial case study.
Publication Year: 2020
Publication Date: 2020-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 8
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot