Formale Verifikationsmethode für reale Schaltungen und Systeme

Autor: Denguir, Mohamed
Jazyk: němčina
Rok vydání: 2019
Předmět:
Popis: Die Absicherung der funktionalen Sicherheit von Schaltungen und Systemen geschieht kostengünstig mithilfe von Verifikation. Dabei sollen die der realen Struktur zugehörigen Funktionen strukturtreu modelliert werden. Unter strukturtreuer Modellierung verstehen wir die Übereinstimmung der formal hergeleiteten Funktion mit der real erzeugten Funktion. Die Modellierung realer Systeme mithilfe von Funktionen (mithilfe der Beschreibung des Verhaltens), welche die Struktur bewahren, führt auf eine Darstellung als Signalflussgraph (SFG). Diese Arbeit stellt eine strukturtreue Verifikationsmethode, mit dem Namen "Strukturtreue Modellierung anhand von Signalflussgraphen", vor. Diese wird mithilfe einer digitalen Schaltung plausibilisiert. Die vorgestellte Verifikationsmethode "Strukturtreue Modellierung anhand von Signalflussgraphen" führt zur Erzeugung einer Quaternär-Vektorliste (QVL) als Datenbank. Diese Datenbank kodiert die Phasenlisten der gewichteten Kanten eines SFG. Es können Suchfunktionen programmiert werden, welche die Datenbank durchgehen und bestimmte Kriterien, wie z.B. Testabdeckung, Fehlerabdeckung und Prüfschärfe, bestimmen. Die durch eine komplexe Realität erzeugten Listen können jedoch in ihren Dimensionen große Ausmaße annehmen. Um nun geringeren Speicherbedarf und kürzere Rechenzeit zu erhalten, sollte die Datenbank ohne Informationsfluss maximal kompaktiert werden können. In dieser Arbeit wird eine Methode zur verlustlosen Kompaktierung präsentiert und beispielhaft erläutert. Die vorgestellte Verifikationsmethode "Strukturtreue Modellierung anhand von Signalflussgraphen" führt letztendlich zur Erzeugung eines kompaktierten Datenmodells. Mithilfe dieses kompaktierten Datenmodells kann die vorhandene Information zur Testüberdeckung, und damit Informationen über die in einem Baugruppensystem tatsächlich auftretenden Fehler, nun zügig extrahiert und genutzt werden. In dieser Arbeit wird ein optimales, gerichtetes Vorgehen für den Austausch von möglichen fehlerhaften Bauteilen in einem Diagnose-Flow vorgeschlagen. Dafür stellt diese Dissertation das Konzept einer selbstbestätigenden Methode namens "Fehlerbaumanalyse" vor. Wird diese Datenbank nun auch noch mithilfe von Zahlen kodiert, kann die Trennung von Testergebnissen die gewünschte Zielprojektion unterstützen. Doch die Eingabe von Daten mit hohen Dimensionen, in denen nicht wenige Elemente einer Datenmenge irrelevant oder weniger relevant als andere sind, führt meist zu sehr unübersichtlichen und schwierig zu interpretierenden Ergebnissen. Zu Ergebnissen also, in denen die gewünschten Zieldaten nur sehr aufwändig weiterverarbeitet werden können. Also ist es sinnvoll Verfahren heranzuziehen, welche die einzelnen Dimensionen der Datenmengen nach ihrer Relevanz klassifizieren und vorteilhaft reduzieren. In dieser Dissertation wird die Datenanalyse (SEDA) zur Trennung von Daten vorgestellt und anhand eines Anwendungsbeispiels verdeutlicht.
Databáze: OpenAIRE