Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-4897
Main Title: A framework for the automatic verification of discrete-time MATLAB simulink models using Boogie
Translated Title: Ein Framework für die automatische Verifikation von zeitdiskreten MATLAB Simulink Modellen mit Boogie
Author(s): Reicherdt, Robert
Advisor(s): Glesner, Sabine
Referee(s): Giese, Holger
Kao, Odej
Glesner, Sabine
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
Language Code: en
Abstract: MATLAB/Simulink ist ein weit verbreitetes Werkzeug für die Entwicklung von eingebetteten Systemen, welches vor allem in der Automobilindustrie zur Entwicklung von Steuerungssystemen benutzt wird. Da solche Systeme häufig in sicherheitskritischen Umgebungen eingesetzt werden, wo eine Fehlfunktion zu schweren Verletzungen und Todesfällen führen kann, werden umfangreiche und vollständige Qualitätssicherungsmaßnahmen benötigt um die Korrektheit der Systeme für alle möglichen Ausführungen sicher zu stellen. Trotzdem werden unvollständige Techniken wie Testen in der Praxis gegenüber den sicheren formalen Methoden bevorzugt. Obwohl es einige formale Verifikationstechniken für MATLAB/Simulink gibt, sind diese entweder kaum automatisiert oder skalieren schlecht. Um dieses Problem zu lösen stellen wir in dieser Arbeit einen Ansatz für eine hochautomatisierte Verifikationsumgebung für MATLAB/Simulink Modelle vor, mit der zeitdiskrete Modelle für Steuerungen formal verifiziert werden können. Die Kernidee in unserem Ansatz ist hierbei eine Kombination aus induktiven Verifikationstechniken und dem automatischen Extrahieren von Verifikationszielen für bestimmte Laufzeitfehler verwenden, um einen automatisierten Verifikationsfluss zu erreichen. Außerdem stellen wir einen Ansatz für das Slicing von MATLAB/Simulink Modellen vor, der als automatisches Verfahren zur Reduzierung der Modellkomplexität verwendet wird. Mit diesem erreichen wir eine bessere Skalierbarkeit, da wir eine komplexe Verifikationsaufgabe in eine Anzahl von weniger komplexen Teilaufgaben aufspalten können. Um die automatische Verifikation von MATLAB/Simulink Modellen zu ermöglichen, stellen wir eine formale Semantik für zeitdiskrete Modelle vor, die auf einer Abbildung der informellen, sequenziellen Simulationssemantik in die formale Verifikationszwischensprache Boogie2 basiert. Zusammen mit automatisch erzeugten und in das formale Modell eingewobenen Invarianten und Verifikationszielen, erlaubt dies die Verifikation der Modelle mit dem Boogie-Framework und induktiven Verifikationstechniken. Um einen hohen Grad der Automatisierung zu erreichen, unterstützen wir auch induktive Verifikationstechniken über mehr als einen Simulationsschritt (k-Induktion), was zwar die Verwendung von schwächeren, automatisch generierten Invarianten erlaubt, aber gleichzeitig die Skalierbarkeit reduziert. Um dem entgegenzuwirken, nutzen wir unser neuartiges Slicing-Verfahren für MATLAB/Simulink Modelle um diese automatisch auf genau die Blöcke zu reduzieren, die für einen (möglichen) Fehler an einem bestimmten Block relevant sind. Darüber hinaus schlagen wir einen Prozess für die effiziente Benutzung unserer Verifikations- und Slicing-Techniken vor. Um die praktische Anwendbarkeit unserer Verifikationsumgebung zu zeigen, haben wir diese in unserem MeMo-Werkzeug implementiert und unseren Prozess auf zwei industrielle Fallbeispiele angewendet. Damit haben wir die Performanz und die Fähigkeit, die Abwesenheit von wichtigen Laufzeitfehlern in einem gegebenen Modell automatisch zu verifizieren, nachgewiesen.
MATLAB/Simulink is a widely used industrial tool for the development of embedded systems, especially for the development of embedded controller software in automotive industries. Since such embedded systems are often deployed in safety critical areas where an error may lead to severe injuries and even to death of persons, comprehensive and complete quality assurance measures are required for ensuring their correctness in all possible cases. Still, incomplete techniques like testing are favored over safe formal techniques in practice. Although there exist some formal verification approaches for MATLAB/Simulink models that can guarantee correctness, they are either poorly automated or suffer from scalability issues. To overcome this problem, we present an approach for a highly automated verification framework for MATLAB/Simulink models that enables the formal verification of discrete-time controller models. Our main idea is to use inductive verification techniques in combination with an automatic extraction of verification goals for a number of important run-time error classes to provide an automatic verification flow. Furthermore, as automatic model reduction technique, we present a slicing approach for MATLAB/Simulink. With that, we increase the scalability by dividing a possibly complex verification task into a number of less complex subtasks. To enable the automatic verification of MATLAB/Simulink models, we present a formal semantics for discrete-time models based on a mapping of the informally defined sequential simulation semantic into the formally well defined intermediate verification language Boogie2. Together with automatically generated invariants and verification goals that are automatically weaved into the formal model, this mapping enables the verification of the models using the Boogie verification framework and inductive verification techniques. To achieve a high degree of automation, we also support inductive verification over more than one simulation step (k-induction), which allows for weaker invariants that can be generated automatically at the price of decreased scalability. To overcome scalability issues for k-induction, we use our novel slicing technique for MATLAB/Simulink models to automatically reduce a model to those blocks that are relevant for a (possible) error at a particular block. Furthermore, we propose a process for the efficient use of our verification and slicing techniques. To show the practical applicability of our framework, we have implemented our approach as the MeMo tool suite and applied our verification process to two industrial case studies. With that, we demonstrate the performance and the capability to automatically verify a given model for the absence of important run-time errors with our verification framework for discrete-time MATLAB/Simulink models.
URI: http://depositonce.tu-berlin.de/handle/11303/5200
http://dx.doi.org/10.14279/depositonce-4897
Exam Date: 10-Jul-2015
Issue Date: 2015
Date Available: 14-Dec-2015
DDC Class: DDC::000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::000 Informatik, Informationswissenschaft, allgemeine Werke
Subject(s): slicing
verification
MATLAB Simulink
Boogie
SMT
Verifikation
Creative Commons License: https://creativecommons.org/licenses/by/4.0/
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
Reicherdt_Robert.pdf4.6 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.