Automatische Abbildung von MoDeST Spezifikationen auf UPPAAL
Inhalt
'In dieser Arbeit wird eine automatische Abbildung von MoDeST Spezifikationen auf "Timed Automata" (TA) entwickelt und implementiert. MoDeST [ARG01] ist eine Spezifikationssprache für verteilte Systeme. Die Sprache erlaubt insbesondere die Beschreibung von Echtzeiteigenschaften, und kann als Erweiterung von TA angesehen werden. Ziel dieser Arbeit ist, eine konkrete Abbildung von MoDeST in eine bestimmte Variante von TA zu realisieren. Diese Abbildung wird es ermöglichen, den Echtzeit-Modellprüfer UPPAAL im Kontext von MoDeST einzusetzen.