Home > Research > Publications & Outputs > Practical Formal Verification for Model Based D...


Text available via DOI:

View graph of relations

Practical Formal Verification for Model Based Development of Cyber-Physical Systems

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Publication date24/08/2016
Host publication2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES)
Number of pages8
<mark>Original language</mark>English


The application of cyber-physical systems (CPSs) in safety-critical applications requires rigorous verification of their functional correctness and safety-relevant properties. We propose a practical verification framework which enables to fill the gaps between model-based development and the formal verification process seamlessly connecting them. The verification framework consists of (a) a model transformation method, which automatically transforms the plant models of CPSs including differential algebraic equations (DAE) to equivalent models without DAE to reduce verification complexity induced by DAE solver execution, and (b) a model simplification method, which automatically simplifies bond-graph models by replacing complex bond-graph components with simpler components for further verification overhead reductions. We successfully applied the proposed verification framework for safety verification of an automotive brake control system. The results of the study demonstrate that the automated model transformations of the CPS models yield significant verification complexity reductions without impairing the ability to detect unsafe behavior of the brake control system in a formal verification based on symbolic execution. © 2016 IEEE.