timemachine

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

Timemachine ist ein Bounded Model Checking Tool für unvollständige Netzwerke von Zeitautomaten, welches die Nicht-Realisierbarkeit einer Invariante beweisen kann. Dieses Tool unterstützt mehrere gängige Kommunikationsmechanismen und erlaubt dem Benutzer mehrere Automaten des Netzwerks als Blackbox zu modellieren. Weiterhin kann für jeden Blackboxausgang festgelegt werden, wie das unbekannte Verhalten modelliert werden soll (Abstraktion basierend auf sicheren Kanten oder basierend auf universeller Quantifizierung). Timemachine verwendet Yices und MathSAT als back-end SMT Solver. Wenn die präzisere Modellierung basierend auf universeller Quantifizierung benötigt wird, können die resultierenden quantifizierten SMT Formeln mit LIRA oder LinAIGs gelöst werden. Als Eingabe akzeptiert Timemachine Netzwerke von Zeitautomaten im standard UPPAAL Format und verwendet hierfür die opensource Parserbibliothek UTAP. Die Kommunikationsmechanismen Synchronisation (Channels), Broadcast Channels, Clocks und Bounded Integer Variables werden als Blackboxausgänge zugelassen.

Fischer Protocol Das Fischer Protokoll garantiert bei mehreren nebenläufigen Prozessen wechselseitigen Ausschluss für einen kritischen Bereich. Im ursprünglichen Design wird eine Integer Variable verwendet, um festzulegen, welcher Prozess auf den kritischen Bereich zugreifen darf. Wir simulieren diese Variable durch einen zusätzlichen Teilautomaten, so dass sämtliche Kommunikation im Netzwerk auf Synchronisation basiert. In jedem Prozess is ein Fehler in einer Guard eingefügt (strikte Ungleichung wird in nicht-strikte Ungleichung verändert). Es wird getestet, ob die ersten n Prozesse gleichzeitig auf den kritischen Bereich zugreifen können, wobei die restlichen Prozesse als Blackboxes modelliert sind.

Processes With Arbiters: Dieses Design ist ein Protokoll für den wechselseitigen Ausschluss, wobei jedem Prozess ein eigener Arbiter zugewiesen ist. Die Prozesse kommunizieren mit ihrem Arbiter über Synchonisation und ein Counter entscheidet über eine Bounded Integer Variable, welcher Prozess als nächstes an der Reihe ist. In unserem ersten Szenario werden mehrere Prozesse als Blackboxes modelliert und geteste, ob die restlichen Prozesse gleichzeitig einen sicheren Zustand erreichen können. Im zweiten Anwendungsfall wird ein Fehler in jeden Arbiter eingefügt, so dass ihr zugehöriger Prozess für jeden Wert der Integer Variable des Counters fortfahren darf. Mit der Abstraktion basierend auf universeller Quantifizierung ist es möglich zu beweisen, dass der oben beschriebene Zustand erreicht werden kann, wenn der Counter als Blackbox modelliert wird.

FlexRay Protocol: Dieses Netzwerk von Zeitautomaten beschreibt eine einfache Version der physikalischen Ebene des FlexRay Protokolls. Die Teilautomaten strobing unit, sending module und voting module, die über Synchronisation, Broadcast Channels, Bounded Integer Variables und Clocks mit den implementierten Automaten kommunizieren, sind als Blackboxes modelliert. Im receiving module ist ein Fehler eingebaut, so dass ein Fehlerzustand erreicht werden kann, der bezeichnet, dass die Übertragung nicht erfolgreich war. Der Fehler hängt von Blackbox Integer Variablen und Clocks ab und kann nur mit der Abstraktion basierend auf universeller Quantifizierung bewiesen werden.

Gear Production Stack: Das Gear Production Stack Benchmark modelliert eine Fertigungsstätte für Getriebe, die aus mehreren aufeinanderfolgenden Stationen besteht. Jede Station teilt ihre Beendigung über Synchronisation und eine Bounded Integer Variable der nächsten Station mit, die dann den Produktionsprozess fortführen kann. Ein Controller initiiert den Ferigungsprozess und überprüft, ob ein Getriebe in einer vorgegebenen Zeit fertiggestellt wurde - wenn nicht, dann befindet sich der Controller in einem Fehlerzustand. In diesem Design sind Einstellungen des Controllers derart fehlerhaft, dass der Fertigungsprozess eines Getriebes immer zu lange dauert und zudem die erste Station, die als Blackbox modelliert wird, übersprungen wird. Es wird die Nicht-Realisierbarkeit der Eigenschaft, dass der Fertigungsprozess rechtzeitig beendet wird, bewiesen.