Algorithms and Data Structures for Parametric Analysis of Real-Time Systems

Abstract

Dieses Dokument ist ein Beitrag auf dem Gebiet der Validierung und Verifizierung der Kommunikation in Echtzeit-Systemen, mit Schwerpunkt auf parametrische Erreichbarkeit Analyse der Systeme modelliert mit Timed Automata.Erreichbarkeit Analyse ist ein entscheidender Aspekt für die Validierung und Verifikation von Software-und Hardware-Systeme. Die Erreichbarkeit für die Echtzeit-Analyse-Systemen ist, dass die Fläche ist die von vielen Forschern in der Wissenschaft und der Industrie. Jedoch nicht viel getan worden, für Systeme, in denen die Zeit Zwänge sind anhand von Parametern. Das ist eine ernste Missverhältnis mit der realen Welt, wo die Daten der meisten der Kommunikations-Protokolle oder Embedded-Software-und Hardware-Systeme sind in der Tat parametrisierten.Diese Arbeit präsentiert eine komplette Rahmen für die vorwärts und rückwärts parametrischen Erreichbarkeit Analyse. Die hier vorgestellte Lösung kann verwendet werden, als Basis von Algorithmen für die Validierung und Verifikation von Software-und Hardware-Echtzeit-Systeme, modelliert als Timed Automata mit Parametern. Die Ergebnisse der Dissertation kann leicht auf Model-Checking oder Test Generation Werkzeuge und Algorithmen.Die zentrale Idee der Diplomarbeit ist ein Konzept der erweiterten Differenz Bound Matrix (EDBM). Dies ist eine Datenstruktur, die Beziehungen zwischen allen Geschäften Systems Uhren und Parameter. Im Gegensatz zu Parametric DBM, das ist die state-of-the-art-Daten für die parametrische Analyse, EDBM ist es nicht erforderlich, die Speicherung Beschränkungen für Uhren und Zwänge von Parametern getrennt. Dies führt zu erheblichen Vorteilen in Bezug auf Speicher und Zeit erforderlich sind, um grundlegende Vorgänge für symbolische Analyse.Die Laufzeit der Lösung wurde durch die Umsetzung eines Proof-of-Concept-Tool und Experimente mit modernen Kommunikations-Protokoll. Die Ergebnisse zeigen, dass auch komplexe Systeme können effizient durch den Rahmen.