DFG-Sachbeihilfe-Projekt: EV2
Ziele
Dieses Vorhaben setzt sich zum Ziel, formale Methoden, die bei der Schaltkreissynthese zum Einsatz kommen, auch für die Verifikation nutzbar zu machen.
Dieses Vorhaben setzt sich zum Ziel, formale Methoden, die bei der Schaltkreissynthese zum Einsatz kommen, auch für die Verifikation nutzbar zu machen.
Der Begriff der formalen Methoden beschreibt in der Verifikation den Vorgang, erwünschte oder unerwünschte Schaltkreiseigenschaften mittels mathematischer Ausdrücke zu erfassen und zu beweisen bzw. zu widerlegen. Die entsprechenden Algorithmen können als ausgereift betrachtet werden.
Ebenso können formale Methoden bei der Schaltkreissynthese zum Einsatz kommen. Ein geeigneter Formalismus hierfür sind Operationseigenschaften, mit denen sich zeitliche Abläufe in unterschiedlicher Granularität repräsentieren lassen. Die Synthese von Operationseigenschaften, d. h. die Verwendung eines vollständigen und widerspruchsfreien Eigenschaftssatzes zur automatisierten Generierung einer konkreten Implementierung, wurde für Hardware bereits erforscht.
Teilgegenstand dieses Antrags ist nun die Nutzung eines vollständigen und widerspruchs-freien Satzes von Operationseigenschaften zur Verifikation, sodass die gesamte von den Eigenschaften beschriebene Funktionalität sowie Randfälle der Spezifikation in automatisiert generierte Testfälle einfließt und ein System under Test entsprechend geprüft werden kann. Das erlaubt die Verifikation bestehender, manueller Implementierungen unter Zuhilfenahme einer formalen Systemspezifikation.
Zusätzlich soll eine Zwischensprache entwickelt werden, die die Hardwareabstraktion und plattformübergreifende Anwendung der Methodik erlaubt. Um die Generalität des Ansatzes zu zeigen, wird neben der Schaltkreisverifikation eine weitere Zielplattform betrachtet: Speicherprogrammierbare Steuerungen (SPS). Diese Plattform wurde ausgewählt, da auch bei sicherheitskritischen Systemen die Verifikation in der Praxis kaum eine Rolle spielt. Da sich auf SPS nur eine Teilmenge aller möglichen Eigenschaften abbilden lässt, werden diese plattformabhängigen Einschränkungen formalisiert.
Für diejenigen Eigenschaften, für die automatisiert (plattformabhängig) Testfälle generiert werden können, ist zusätzlich geplant, die Testergebnisse wieder in die ursprüngliche Spezifikation zu annotieren, womit eine Closed Loop im Wasserfallmodell etabliert werden kann. An der Professur existiert das selbstentwickelte Spezifikationswerkzeug SpecScribe, das die Formalisierung von Anforderungen erlaubt. Dieses Tool soll derart erweitert werden, dass die Closed Loop von Spezifikation und Verifikation und somit das gesamte Wasserfallmodell nahtlos abgebildet werden. So können Verifikationsergebnisse auf Spezifikationsebene sichtbar gemacht werden, was die Rückverfolgung von Fehlern bis zur Spezifikation vereinfacht.
Tags
Laufzeit
February 2020
January 2023
