AUTOMATISCHE ABBILDUNG VON MODEST SPEZIFIKATIONEN AUF UPPAAL (ABGESCHLOSSEN)

Eine vollständige formale Semantik für die Web Service Beschreibungssprache BPEL 2.0
Verteilte Java Anwendungen: Kann das gut gehen?
Reflexive und transitive Abschluss eines gerichtetes azyklisches Graphes
Implementierung eines Preflow-Algorithmus für Markovketten
Eine Implementierung mit PEPP
Interactive Simulator for MoDeST (abgeschlossen)
Die richtige Ordnung in "Compositional Aggregation" (laufend)
Präzision von MANET-Simulatoren
Diskrete Ereignissimulation (laufend)
Abbildung von StoCharts nach MoDeST (abgeschlossen)
Energieverbrauch in Ad-Hoc und Sensor-Netzwerken (abgeschlossen)
Axiomatisierung von "Branching Bisimulation" mit Divergenz (abgeschlossen)
Value Passing MoDeST (abgeschlossen)
Automatische Abbildung von MoDeST Spezifikationen auf UPPAAL (abgeschlossen)

Titel der Arbeit

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.


Status

Abgeschlossen


Kontakt

Prof. Dr.-Ing Holger Hermanns


Verweise

[ARG01] P. D'Argenio, H. Hermanns, J.-P. Katoen, R. Klaren. MoDeST -- A Modelling and Description Language for Stochastic Timed Systems. PAPM-PROBMIV 2001, LNCS 2165, 2001.