Monthly Archive for Juni, 2005

TLDC

Published
by
Niels
on 26. Juni 2005
in Temporale Logik and Tools
. 0 Comments

TLDC berechnet die Aktionen einer TLDA-Spezifikation und konstruiert den Erreichbarkeitsgraphen.

tldc.jpg

Links

Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA)

Published
by
Niels
on 20. Juni 2005
in Studium and Temporale Logik
. 0 Comments

Studienarbeit am Lehrstuhl für Theorie der Programmierung (20. Juni 2005)

Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA)

Die Temporal Logic of Distributed Actions (TLDA) ist eine temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings gibt es noch wenig Erfahrung bei der computergestützten Verifikation halbordnungsbasierter Formalismen. Viele bekannte effiziente Algorithmen des expliziten Modelchecking setzen ein Transitionssystem und somit eine Interleavingsemantik voraus.

In dieser Arbeit wird eine Interleavingsemantik für TLDA vorgeschlagen und ein Prototyp entwickelt, der für eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage für die weitere Arbeit an einem Modelchecker für TLDA sein.

Dateien