Refine
Document Type
- Doctoral Thesis (1)
- Report (1)
Language
- German (2)
Has Fulltext
- yes (2)
Keywords
- Automat <Automatentheorie> (1)
- CAN bus (1)
- CAN-Bus (1)
- Kommunikationsprotokoll (1)
- Kommunikationssystem (1)
- Leistungsbewertung (1)
- Medienzugriff (1)
- Model Checking (1)
- UPPAAL (1)
- Unifikationsgrammatik (1)
Institute
Modell-basierte Testverfahren werden im Paradigma der Constraint-Programmierung angesehen. Demnach wird eine Spezifikation (in Form eines Zeitautomaten oder einer Komposition von Zeitautomaten) zunächst als ein Constraint-Programm kodiert. Durch die symbolische Ausführung des Programms werden Testdaten erzeugt, die als Eingaben für Testfälle dienen. Auf dieser Basis kann das Modell dann ggf. korrigiert bzw. weiter verfeinert werden. Um Berechnungen effizient durchführen zu können, werden sog. Konsistenzverfahren eingesetzt, wodurch potentiell weniger Klauseln ausgewählt, der Suchaufwand minimiert und somit die Effizienz gesteigert werden kann. Die im Zusammenhang mit den Konsistenzverfahren zu definierenden Propagierungsmechanismen wurden im Rahmen einer prototypischen Architektur implementiert; zur praktischen Demonstration wurde ein Szenario aus dem Bereich der interaktiven Multimediakommunikation herangezogen.
In dieser Arbeit stellen wir eine durch Zeitautomaten modellierte Spezifikation des Mediumzugriffs im CAN-Protokoll vor sowie ihre Implementierung in UPPAAL. Zeitliche Anforderungen wurden dabei durch entsprechende Uhren-Nebenbedingungen erfasst. Dieses Zeitautomaten-Modell wurde anschließend automatisch verifiziert (Model Checking), wobei mehrere Anforderungen identifiziert wurden, die das CAN Protokoll erfüllen muß (wie Deadlock-Freiheit des Modells, Übertragungsrecht für die höchstpriore Nachricht, exklusives Übertragungsrecht für beliebigen CAN-Adapter nach der gewonnenen Arbitrage etc.). All diese Eigenschaften wurden in einer Variante der temporalen Logik CTL spezifiziert; die automatische Verifikation selbst wurde dabei mit UPPAAL durchgeführt, einem Model Checker für zeitautomaten-basierte Modelle.