Service-oriented Abstraction and Verification of Hybrid Simulink Models with Simulink2dL
Embedded control systems combine discrete and continuous behavior. To cope with the immense complexity of the resulting systems, they are increasingly designed with model-driven development and tools like Matlab Simulink. At the same time, application of embedded systems in safety-critical areas, like in the automotive industry or medical context, require high safety standards. In this project, we investigate a formally well-founded, service-oriented design and verification approach for Simulink. The key ideas of our approach are threefold: First, we propose a service-oriented design approach for Simulink, where we introduce services for Simulink, hybrid contracts to cleanly define these services, and feature models to model their variability. Second, we propose a transformation of Simulink models into the expressive and formally well-defined differential dynamic logic. This enables the formal verification of hybrid systems modeled in Simulink using the powerful interactive theorem prover KeYmaera X. To overcome scalability issues, we enable compositional verification by replacing the inner structure of services by their contracts for system verification.
Contact: Prof. Dr. Paula Herber, Timm Liebrenz, MSc
