BDD-basierte Verifikation von Realzeit-Systemen

Dirk Beyer und Andreas Noack
Lehrstuhl Software-Systemtechnik
BTU Cottbus

Abstract.  Diese Arbeit behandelt die effiziente Erreichbarkeitsanalyse von
Timed Automata.  Wir beschreiben eine Erreichbarkeitseigenschaften erhaltende
Diskretisierung der Zeit.  Diese ermöglicht es, Konfigurationsmengen von Timed
Automata als Binary Decision Diagrams (BDDs) darzustellen.  Die kompakte
BDD-Repräsentation großer Mengen erfordert geeignete Variablenordnungen.  Zur
deren Bestimmung nutzen wir Strukturinformationen aus der Modellierungsnotation
Cottbus Timed Automaton.  Wir belegen die erzielten Effizienzverbesserungen
durch Meßwerte.