Correct System Design

Tim Strazny

On this page:

back to the mainpage.

 

go next top of page

1 Theses (with abstracts)

[TS07]
Tim Strazny. Entwurf und Implementierung von Algorithmen zur Berechnung von Petrinetz-Semantiken für Pi-Kalkül-Prozesse, July 2007.
[ bib | .pdf ]

Häu?g enthalten Computerprogramme Fehler. In kritischen Fällen, bei denen die Abwesenheit von Fehlern im Sinne der Spezi?kation sichergestellt werden muss, werden Programme mühevoll von Hand bewiesen oder Verfahren der automatischen Veri?kation angewendet. Petrinetze, welche die Automatentheorie durch Nebenläu?gkeit verallgemeinern, bieten sich zur automatische Veri?kation an. Für verteilte und dynamisch rekon?gurierbare, d.h. mobile Systeme bietet sich mit dem pi-Kalkül ein formales Modell an, welches mittels neuer Semantiken elegant in P/T-Petrinetze abgebildet werden kann. In der vorliegenden Arbeit werden Algorithmen präsentiert, die bestimmte neue Petrinetz-Semantiken von pi-Kalkül-Prozessen berechnen. Mit diesem automatischen Übersetzen wird das Model-Checking von pi-Kalkül-Prozessen anwendbar.

[TS06]
Tim Strazny. Simulation von Generalized Stochastic Petri Nets, July 2006.
[ bib | .pdf ]

Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bewähren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gefärbte Petrinetze bieten Möglichkeiten komplizierte Sachverhalte strukturiert und kompakt ausdrücken, jedoch ist die Simulation solcher höheren Petrinetze um ein Vielfaches aufwändiger. Mit Geschwindigkeit und Vielfältigkeit als Hauptziel wurden mit P-UMLaut/Sim ein Simulator für solche mehrfach erweiterten Petrinetze entwickelt.

 top of page go back