Eigenschaftsbasierte Verifikations- und Validierungsunterstützung - EV2
Zusammenfassung der Projektergebnisse
Vor der Produktion von Schaltkreisen wird erheblicher Aufwand für deren Verifikation betrieben, da sich funktional fehlerbehaftete Hardware nach der Produktion nicht mehr korrigieren lässt. Anders bei industriellen Steuerungen (SPS) – diese lassen sich im Feld beliebig oft neu programmieren, sodass im Programm eventuell vorhandene Fehler problemlos behoben werden können. Das führt im industriellen Umfeld jedoch dazu, dass die Verifikation von SPS im Allgemeinen vernachlässigt wird, was besonders bei sicherheitskritischen Steuerungen fatal sein kann. An dieser Stelle setzt das Projekt EV² an. Aus einer Spezifikation, die als Voraussetzung in formaler Form vorliegen muss, werden automatisiert Testfälle generiert, um ein bestehendes System im Feld hinsichtlich seiner korrekten Funktion testen zu können. Jede formale Eigenschaft beschreibt dabei einen Testaspekt des Gesamtsystems. Mehrere Eigenschaften können verkettet werden, um Sequenzen zu beschreiben, oder sie überlappen sich zeitlich, was Parallelität im implementierten System ausdrückt. Die formalen Eigenschaften werden nun hinsichtlich ihrer Verkettung sowie ihrer möglichen zeitlichen Überlappungen analysiert und daraus ein abstrakter Automat mit Zuständen und Zustandsübergängen aufgebaut. Aus der formalen Spezifikation werden nun für jeden Zustand dieses Automaten mehrere Testfälle generiert, die verschiedene Szenarien der Eingabesignale abdecken. Schließlich wird ein optimaler Weg durch den Automaten gefunden, der alle Testfälle abdeckt. Dabei werden Stimulationsmuster erzeugt, die dafür sorgen, dass sich die zu testende Hardware jederzeit im gewünschten Zustand befindet. Das Stimulationsmuster wird auf die echte, existierende Hardware beaufschlagt, die Ergebnisse werden aufgezeichnet. Außerdem wird ein Golden Model erstellt, das auf jeden Testfall mit den erwarteten Resultaten reagiert. Stimmen die Ergebnisse des Golden Model mit den aufgezeichneten Daten überein, war der Gesamttest erfolgreich. Bei erfolgreichem Test kann die Aussage getroffen werden, dass das getestete System für jede formale Eigenschaft mindestens in einem Testfall ein korrektes Ergebnis geliefert hat. Diese Methodik stellt jedoch keine formale Verifikation dar, sondern nutzt formale Methoden zur Testfallgenerierung im Bereich der Constrained Random Verification.
Projektbezogene Publikationen (Auswahl)
-
A Verification Approach for Programmable Logic Controllers. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) 2020, 19. bis 20. März 2020, Stuttgart.
Elfatih, Braah; Sauppe, Matthias & Heinkel, Ulrich
-
Closed-Loop Approach on Formal Specification for Semiconductor Test, MikroSystemTechnik Congress 2021, 8.-10. Nov. 2021, Stuttgart-Ludwigsburg.
Schott, Christian; Mayer, Franziska; Billich, Enrico; Yazdani, Saeid; Sauppe, Matthias; Wolz, Werner & Heinkel, Ulrich
