Partial order reduction based analysis of Petri net models

OData support
Vörös András
Department of Measurement and Information Systems

Nowadays, the use of distributed saftey-critical sytems is very wide spread. The correctness of these systems is very critical. We can provide correctness by using formal methods at an early stage of the development. These methods rely on precise mathematical formalism. The aim of this thesis is to develop a tool which can check the correctness of the models of distributed, asynchronous systems. I have implemented a verification module in the PetriDotNet framework, that allows the partial order based examination of Petri-nets. I have chosen one of these approaches, the so-called unfolding algorithm that allows the examination of many models that other simpler algorithms could not assess. My solution contains two main parts: first, my algorithm creates the state space representation of the model. Then it transforms this state space representation into a boolean satisfiability (SAT) problem, which I give to a third party SAT solver. I have developed a simple user interface for the tool, which allows easy use of it.


Please sign in to download the files of this thesis.