Service-oriented decomposition and verification of hybrid system models using feature models and contracts

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 services, and commonly used design languages, like MATLAB/Simulink do not directly allow for the verification of hybrid behavior. Furthermore, services can be reused in new system designs and sometimes require changes in their structure to fit to the new context. By providing hybrid contracts, which formally define the interface behavior of hybrid system services in differential dynamic logic (dL), and providing a decomposition technique, we enable compositional verification of Simulink models with interacting services. This enables us to use the interactive theorem prover KeYmaera X to prove the correctness of hybrid control systems modeled in Simulink. With the inclusion of feature modeling in the design process and the creation of hybrid contracts, we are able to capture a wider range of behavior, while still enabling the use of formal interface description in the verification. We demonstrate the applicability of our approach with a temperature control system and an automotive industrial case study. (C) 2021 Elsevier B.V. All rights reserved.