Vortrag beim Workshop “Luhme X” beim Lehrstuhl für Theorie der Programmierung (14. Oktober 2004)
Ein verteilter Algorithmus, der Network Mutex, wird in [Reisig98] als Petrinetz modelliert. Es wird gezeigt, wie diese Modellierung kanonisch in eine TLA-Modellierung überführt werden kann. Außerdem wurde der Network Mutex-Algorithmus erneut — losgelöst von der Petrinetzmodellierung — agentenorientiert in TLA modelliert. Zuletzt wird der TLA-Model Checker TLC beschrieben, mit dem die Äquivalenz der beiden Modellierungen, sowie die Korrektheit gezeigt. Dies war allerdings durch die Zustandsraumexplosion nicht möglich.
Dateien
- Folien (PDF-Dokument, 37 Folien, 488 KB)
letzte Kommentare