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

Aachen / RWTH Aachen University, Department of Computer Science (2019) [Buch, Doktorarbeit, Bericht]

Seite(n): 1 Online-Ressource (xxiii, 156 Seiten) : Illustrationen, DiagrammeReport-Nummer: AIB-2019-04

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.

Autorinnen und Autoren

Autorinnen und Autoren

Dernehl, Christian Michael

Gutachterinnen und Gutachter

Kowalewski, Stefan
Moormann, Dieter

Identifikationsnummern

  • REPORT NUMBER: RWTH-2019-05178

Downloads