A Service-Oriented Approach for Decomposing and Verifying Hybrid System Models

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 (dL), 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.