Contract-based Verification of Hybrid Simulink Models with Differential Dynamic Logic by prof. Paula Herber - Head of the Embedded Systems Group (WWU Münster) and part-time Professor at FMT

Abstract: 
Cyber-physical systems, where digital components interact with a physical environment, are ubiquitous in our everyday lives. Digital devices assist our households, monitor our health, and support our transportation in airplanes, trains, or cars. While the complexity of cyber-physical systems is steadily increasing, a failure in such systems can have serious consequences. Model-driven development provides an approach to cope with the increasing complexity, but has the serious drawback that industrially used modeling languages, such as Matlab/Simulink, have only informally defined semantics. To overcome this problem, we propose to precisely capture the semantics of hybrid Simulink models with an automated transformation into the formally well-defined differential dynamic logic (dL). Our transformation enables us to formally verify crucial safety properties of hybrid Simulink models with the interactive theorem prover KeYmaera X. KeYmaera X enables deductive reasoning and thus has the potential to scale well even for larger systems. However, the interactive verification with KeYmaera X is still expensive in terms of manual effort and required expertise. To reduce the verification effort, we propose to define hybrid contracts, which enable compositional verification, but still have to be defined manually. In this talk, I will summarize our transformation from Simulink to dL, hybrid contracts for compositional verification, and then discuss the idea of using hybrid contract patterns to ease the interactive verification of cyber-physical systems with KeYmaera X.