Uppsala University Department of Information Technology
September 2005
Abstract:The aim of this thesis was to investigate and enlighten the applicability of P-Nets for simulating large and possibly infinite-control systems. P-Nets are generalized coloured Petri nets [Petri62] which retain detailed information in the tokens regarding firing history and the scope of concurrently executing threads. P-Nets are specified with the help of a process calculi called CCSk which is a derivation of Milner's CCS [milner89], and converted to a P-Net representation prior to simulation. A simulation tool named GPSim was implemented using both generic optimization techniques and techniques specific to P-Net structure and semantics. The simulation performance of GPSim was evaluated and compared to two well-known formal verification tools with respectable pedigrees; Bell Labs' Spin and The Concurrency Workbench of the New Century from Stony Brook University.
Note: M.Sc. thesis
Available as PDF (621 kB)
Download BibTeX entry.