Saturation based model checking of linear time properties

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

Nowadays, embedded controllers are becoming more and more widespread. Since the failure of a safety-critical system may have disastrous effects, the verification of these embedded systems is an important task. We can check the correct behaviour of a system with the help of formal methods in a mathematically sound way in the early phases of development. Model checking is a widely used technique to answer complex verification questions, providing a great deal of information. During the execution of model checking, we examine the validity of requirements expressed with temporal logics. There exist several temporal logics; the most widespread are linear temporal logic (LTL) and computation tree logic (CTL). Their expressiveness cannot be compared, nevertheless using LTL is often more convenient, due to its compactness and simplicity. This does not come for free though – the complexity of LTL model checking is in the PSPACE class, thus it is vital to use efficient algorithms.

Saturation is a symbolic iteration algorithm that is capable of effective state-space exploration and CTL model checking. Its efficiency is due to its iteration strategy and the symbolic, thus compact coding of states. There are saturation-based solutions for CTL model checking, but they cannot be used for LTL model checking because of their different characteristics. There were attempts to use symbolic algorithms for LTL model checking lately – however no one has ever successfully applied saturation to this problem domain yet.

In my work I examine how the saturation algorithm could be applied to LTL model checking. The result is an automata-theoretic approach that I developed based on saturation, thus creating a new, efficient model checking algorithm.

In this work, I will present the theoretical background of the saturation-based linear temporal logic model checking and the new model checking algorithm that I introduced.

Downloads

Please sign in to download the files of this thesis.