Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie

摘要

Matlab/Simulink is a widely used industrial tool for the development of embedded systems. Many of these systems are safety critical, especially in automotive industries. At the same time, automatic formal verification techniques for Simulink, in particular on model level, are rare and often suffer from scalability issues. In this paper, we present an automatic transformation of discrete-time Matlab/Simulink models into the intermediate verification language Boogie. This transformation enables us to use the Boogie verification framework and inductive invariant checking for the automatic formal verification of Matlab/Simulink models. Additionally, verification objectives for common error classes are generated automatically. With our approach, we provide an automatic formal verification technique for Matlab/Simulink and the most common error classes which scales better than existing techniques in many cases. To demonstrate the practical applicability, we have applied our approach to a number of case studies from the automotive domain.