Verification of embedded software models by combining abstract interpretation, symbolic execution and stability analysis

Dernehl, Christian Michael; Moormann, Dieter; Kowalewski, Stefan

doi:HT020113458

Verification of embedded software models by combining abstract interpretation, symbolic execution and stability analysis

Dernehl, Christian Michael^RWTH*

2019

VerantwortlichkeitsangabeChristian Michael Dernehl, M.Sc.RWTH

ImpressumAachen : RWTH Aachen University, Department of Computer Science 2019

Umfang1 Online-Ressource (xxiii, 156 Seiten) : Illustrationen, Diagramme

ReiheAachener Informatik-Berichte ; 2019-04

Dissertation, RWTH Aachen University, 2019

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor)^RWTH* ; Moormann, Dieter (Thesis advisor)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2019-04-11

Online
DOI: 10.18154/RWTH-2019-05178
URL: https://publications.rwth-aachen.de/record/761850/files/761850.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Lyapunov Stability (frei) ; control theory (frei) ; floating point computation (frei) ; static analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Eingebettete Systeme spielen in vielen Bereichen von immer komplexer werdenden technologischen Anwendungen, z.B. in der Mobilität eine immer größere Rolle. Durch wachsende Anforderungen an die Automatisierung - insbesondere in sicherheitskritischen Anwendungen wie dem autonomen Fliegen oder Fahren - steigt die Quantität und Komplexität in der eingebetteten Software signifikant an. Modellbasierte Softwareentwicklung unterstützt interdisziplinäre Teams um in kurzer Zeit Software mit einer hohen Qualität für eingebettete Systeme zu entwickeln. Ein Anwendungsgebiet für modellbasierte Softwareentwicklung sind regelungstechnische Systeme, welche, im Rahmen einer integrierten Werkzeugkette, simuliert und danach eingesetzt werden können. Jedoch ist das Angebot von Werkzeugen zur automatisierten Verifikation von regelungstechnischen Systemen für den Einsatz in Industrie- oder Forschungsprojekten sehr begrenzt. Insbesondere Seiteneffekte und die automatisierte Diskretisierung machen es schwierig, regelungstechnische Systeme zu validieren. Beispielsweise werden häufig Fließkommazahlen verwendet ohne Beachtung der Randfälle und Rundungsfehler. In der Industrie werden Sicherheitsziele durch die Erfüllung von Standards, wie z.B. der IEC 61508, ISO 26262, DO-178C oder anderen erreicht. Abhängig vom Safety Integrity Level (SIL) müssen verschiedene Beurteilungskriterien herangezogen werden. Zum Beispiel müssen für höhere SIL-Stufen alle Ausführungspfade in den Programmen getestet werden. Kommerzielle Werkzeuge ermöglichen die automatisierte Testfallgenerierung mittels verschiedener Techniken, beispielsweise Zufallstesten. Jedoch gibt es kaum Konzepte, welche auf regelungstechnische Systeme zugeschnitten sind. In Rahmen dieser Arbeit wird ein integriertes Konzept zur automatisierten Validierung von Modellen vorgestellt, welches modellbasierte Softwareentwicklung unterstützt. Fehler können mit der vorgestellten Methodik nicht erst im Quellcode oder auf dem Prüfstand, sondern bereits im Modell behoben werden. Diese Arbeit befasst sich insbesondere mit MathWorks Produkten, mit welchen Blockdiagramme, Zustandsdiagramme und MATLAB-Quellcode modelliert werden kann. Jedoch lassen sich die Konzepte auch auf Modelle anderer Toolhersteller einsetzen. Schließlich werden Forschungsergebnisse aus der Regelungstechnik genutzt, um automatisch Eigenschaften abzuleiten, welche den Berechnungsaufwand der Verifikation reduzieren. Der gezeigte Lösungsweg basiert auf verschiedenen Ansätzen. Aus Modellen werden zunächst regelungstechnische Systeme extrahiert und einer Kategorie zugeordnet. Dabei werden lineare, polynomielle, Reset-, positive und unsichere Systeme betrachtet. Je nach Typ, wird eine vollständige Analyse durchgeführt, welche Ergebnisse zu den Extremwerten der Ausgänge sowie zu internen Stabilität bereitstellt. Diese Lösungen werden schließlich von einer Wertebereichsanalyse und Differenzbereichsanalyse genutzt, welche mit symbolischer Ausführung kombiniert werden. Insbesondere werden der Spitze-zu-Spitze Verstärkungsfaktor sowie Invarianten, basierend auf Ljapunow-Funktionen, eingesetzt. Testfälle werden durch die Kombination von Optimalsteuerung und symbolischen Lösungsverfahren generiert.

Embedded systems play an important role in many technological applications, which become increasingly complex, e.g. mobility. With higher degrees of automation, especially in domains such as automated flying or driving, the quantity and complexity of the embedded software grows significantly. Model-based design supports interdisciplinary teams to develop high quality software for embedded systems rapidly. Control design is one potential application for model-based design, so software controlled systems can be simulated and deployed from an integrated toolchain. Nevertheless, the availability of tools to verify control systems, which are deployed in industrial or research projects, remains limited. In particular, discretization and implicit side effects hardens validation when designing controllers. For example, often floating point numbers are chosen as data type without considering corner cases and rounding errors. Formally, safety in industry is measured by the compliance with a corresponding safety norm, such as IEC 61508, ISO 26262, DO-178C or others. Depending on the safety integrity level, different assessments are required. Components with increased risk must be validated with the necessary diligence. For instance, higher safety integrity levels require all execution paths to be tested. A variety of commercial tools offer automated test case generation, applying different techniques, e.g., random testing. However, concepts to generate test cases for control systems are rarely available. In this thesis, an integrated concept to validate models automatically is introduced, supporting model-based design. Instead of resolving errors at source code level or during hardware in the loop testing, our method aims to detect errors as early as possible. The presented techniques are focused on MathWorks products and include block diagrams, statecharts and MATLAB source code. However, the methods can also be applied to models from other vendors. Key findings from control theory are integrated to derive properties, easing the verification process. Our solution is manifold. First, a fitting control system description is extracted from the model. A distinction between linear, polynomial, reset, positive and uncertain systems is performed. For each type, a thorough analysis is conducted on the output boundaries and internal stability. Results are fed back into a value and slope range analysis combined with symbolic execution. Features include the incorporation of the peak-to-peak gain and invariants, which are based on Lyapunov functions. Test suits, satisfying coverage, are constructed by combining optimal control theory with a symbolic solver.

OpenAccess:
PDF
(zusätzliche Dateien)