Soweit sich das Verhalten der zu untersuchenden Anwendung durch eine endliche Zustandsmaschine bewältigbaren Umfangs darstellen lässt, ist das entsprechende "Model Checking"-Problem durch geeignete Werkzeuge bekanntlich lösbar. Für komplexe, miteinander interagierende Systeme mag sich allerdings (in Abhängigkeit von der Anzahl der zu modellierenden Prozessvariablen sowie von dem Umfang ihrer Wertebereiche) keine praktikable Reduktion auf eine endliche Zustandsmenge, die sich mit vertretbarem Aufwand analysieren lässt, von vornherein anbieten.

Im Rahmen dieses Projektes wird deshalb untersucht, inwieweit sich die Prüfung der Gültigkeit spezieller (existentieller bzw. universeller) temporallogischer Eigenschaften auch auf Erweiterte Endliche Zustandsmaschinen (EFSM) ingenieurmässig übertragen lässt.

Da Erweiterte Automaten die volle Ausdruckskraft besitzen, lässt sich im Allgemeinen die Erfüllung beliebiger Eigenschaften ihres Verhaltens nicht algorithmisch entscheiden. Daher ist man in solchen Fällen auf den Einsatz heuristischer Verfahren angewiesen, deren Gestaltung und Einsetzbarkeit den Gegenstand der Untersuchungen bilden.

Nachdem die ursprüngliche Erweiterte Zustandsmaschine und die nachzuweisende temporallogische Eigenschaft mittels einer zweiten Erweiterten Zustandsmaschine (der sog. Expandierten Erweiterten Zustandsmaschine EXEFSM) gemeinsam kodiert wurden, wird die Gültigkeit existentieller bzw. die Ungültigkeit universeller temporallogischer Formeln auf die Existenz bestimmter Mengen ausführbarer Pfade der EXEFSM zurückgeführt werden, die durch geeignete Überdeckungskriterien der EXEFSM charakterisiert werden. Zunächst wurde ein Verfahren zur statischen Ermittlung von EXEFSM-Pfadmengen, die das zugrundeliegende Überdeckungskriterium erfüllen, realisiert.

Zur Untersuchung der Ausführbarkeit mindestens einer der identifizierten Pfadmengen wurde ein Verfahren entwickelt und implementiert, das mittels der Metaheuristik Simulated Annealing die Generierung von Testdaten zwecks Ausführung der zuvor statisch ermittelten Pfade anstrebt.

Das Verfahren nutzt dabei Techniken der lokalen Optimierung; hierzu wurde eine mittels Simulated Annealing zu optimierende Bewertungsfunktion für die Testdatengüte definiert, die zu vorgegebenem Pfad den Grad der durch die Testdaten erzielbaren "Ausführbarkeit" evaluiert. Diese Bewertungsfunktion erreicht selbstverständlich ihr Optimum, falls die Testdaten den betrachteten Pfad vollständig ausführen können.

Zur Bewertung der Testdaten wird die Summe aus der sogenannten Annäherungsstufe und der sogenannten lokalen Abstandsfunktion gebildet, wobei
-die Annäherungsstufe die Länge des längsten Pfadsuffixes angibt, das durch die Testdaten nicht zur Ausführung gebracht werden konnte, während
-die lokale Abstandsfunktion den Grad der Verletzung datenspezifischer Prädikate bestimmt, deren Erfüllung für die Pfadausführung notwendig ist.

Das Verfahren konnte anhand eines beispielhaften EFSM-Modells für autonome, kooperierende Roboter erfolgreich evaluiert werden.

Dieses Forschungsprojekt wurde im Berichtszeitraum 2018 schließlich durch die Fertigstellung einer Dissertation mit dem Titel „Strukturelle Testverfahren zur Verifikation existentieller temporallogischer Formeln in erweiterten endlichen Zustandsmaschinen“ und Abschluss der zugehörigen Promotionsprüfung erfolgreich beendet.