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
Contents
- 1. Access to our framework (Simulink2dL and SimulinkRL2dL)
- 2. Verification Flow
- 3. Example Models and Proofs
- 3.1. Formal Methods 2021: Proofs and Models with Reinforcement Learning
- 3.2. (A)ISoLA 2022/23: Proofs and Models for Safe and Resilient Hybrid Systems
- 3.3. ATVA 2022: Proofs and Models for Reusable Contracts
- 3.4. Formal Methods 2024: Proofs and Models for Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
- 4. Proof and Model for Safe Battery Use and Grid-Convenience in an Intelligent Energy Control System
