Nowadays the verification of software and hardware systems is gaining an even more important role in system design. Applying the mathematically well-founded formal methods in the verification context is a general requirement. Formal verification of complex systems is a hard task. However the available amount of computational resources is increasing, the analysis of complex systems is difficult.
Model checking is a wide-spread method for verification. At first, we have to create the model of the system, in this case using Petri Net formalism, then the algorithm explores the possible state space. After the state space generation we can check the specification requirements defined by temporal logic expressions.
In our former work we have presented the so-called saturation algorithm to discover and store the state space efficiently. However, model checking of complex systems could not be accomplished with these methods so far. These classes of systems have complex or infinite state models.
In my current work I have investigated bounded model checking techniques which can give a solution for these problems.
– I have investigated the saturation based bounded state space generation and model checking algorithms , that enables us to examine many requirements without exploring the full state space, which helps us to analyse complex or even infinite state systems.
– I have investigated the constrained saturation algorithm that prevents the iteration to do unnecessary steps during the model checking.
– I created a new model checking algorithm by combining the bounded state space exploration with the constrained saturation algorithm, which is faster than the former algorithm in many cases.
– I have investigated the completeness of the bounded model checking using three-valued logics that can give more accurate answer for a given criteria.
As part of my work I integrated my solutions into the PetriDotNet framework developed at the Department of Measurement and Information Systems. In addition, I did comparative measurements to prove the efficiency of the new methods.