Correct System Design

Tim Strazny

On this page:

back to the mainpage.

 

go next top of page

1 Theses (BibTeX Source)


@MISC{ts07,
  TITLE = {{E}ntwurf {u}nd {I}mplementierung {v}on {A}lgorithmen {z}ur {B}erechnung {v}on {P}etrinetz-{S}emantiken {f}\"{u}r {P}i-{K}alk\"{u}l-{P}rozesse},
  AUTHOR = {{T}im {S}trazny},
  SCHOOL = {University of Oldenburg},
  MONTH = {July},
  YEAR = {2007},
  URL = {http://csd.informatik.uni-oldenburg.de/~skript/pub/diplom/strazny07.pdf},
  ABSTRACT = {H\"{a}u?g enthalten Computerprogramme Fehler. In kritischen F\"{a}llen, bei denen die Abwesenheit von Fehlern im Sinne der Spezi?kation sichergestellt werden muss, werden Programme m\"{u}hevoll von Hand bewiesen oder Verfahren der automatischen Veri?kation angewendet. Petrinetze, welche die Automatentheorie durch Nebenl\"{a}u?gkeit verallgemeinern, bieten sich zur automatische Veri?kation an. F\"{u}r verteilte und dynamisch rekon?gurierbare, d.h. mobile Systeme bietet sich mit dem $\pi$-Kalk\"{u}l ein formales Modell an, welches mittels neuer Semantiken elegant in P/T-Petrinetze abgebildet werden kann. In der vorliegenden Arbeit werden Algorithmen pr\"{a}sentiert, die bestimmte neue Petrinetz-Semantiken von $\pi$-Kalk\"{u}l-Prozessen berechnen. Mit diesem automatischen \"{U}bersetzen wird das Model-Checking von $\pi$-Kalk\"{u}l-Prozessen anwendbar.}
}


@MISC{ts06,
  TITLE = {{S}imulation {v}on {G}eneralized {S}tochastic {P}etri {N}ets},
  AUTHOR = {{T}im {S}trazny},
  SCHOOL = {University of Oldenburg},
  YEAR = {2006},
  MONTH = {July},
  URL = {http://csd.informatik.uni-oldenburg.de/~skript/pub/ip/strazny06.pdf},
  ABSTRACT = {Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bew\"{a}hren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gef\"{a}rbte Petrinetze bieten M\"{o}glichkeiten komplizierte Sachverhalte strukturiert und kompakt ausdr\"{u}cken, jedoch ist die Simulation solcher h\"{o}heren Petrinetze um ein Vielfaches aufw\"{a}ndiger. Mit Geschwindigkeit und Vielf\"{a}ltigkeit als Hauptziel wurden mit P-UMLaut/Sim ein Simulator f\"{u}r solche mehrfach erweiterten Petrinetze entwickelt.}
}

 top of page go back