Towards Automated Service-Oriented Verification of Embedded Control Software Modeled in Simulink.

The verification of hybrid embedded control systems is a difficult and time intensive task. In previous work, we have presented a compositional, service-oriented verification approach for hybrid systems that are modeled in Simulink using differential dynamic logic and the interactive theorem prover KeYmaera X. In this paper, we discuss the challenges that arise during this verification process with a hybrid system from the medical domain, namely a generic infusion pump (GIP). We discuss the manual effort necessary to verify this (comparatively large) system and propose partial automations that reduce the effort and increase the practical applicability of the verification process.