Fault Identification in Petri Nets: Theory and Implementation

In this thesis, we address the problem of fault identification in Petri nets: given a known Petri net and an unknown fault introduced to it, in terms of an additional (possibly unobservable) transition, we identify the fault, by only observing the executions of the system. We do this by translating the fault identification into a system of Integer Linear (In)Equations, which enable us to solve the problem using Integer Linear Programming. We prove its soundness, i.e., that the identified Petri net can indeed generate all the observed traces. Additionally, we observe and correct some inaccuracies in the existing literature in fault identification. We propose an approach to exploit the recent developments in the tools for checking satisfiability modulo theories. Through this approach, we empirically examine our research question, whether our fault identification technique is applicable in identifying faults in a number of examples. We have implemented the approach into a program that automatically codes the fault identification method into the input language of the Z3 SMT Solver. An evaluation of the applicability of our tool has been made by using a number of examples.