M.Sc Thesis


M.Sc StudentSade Gal
SubjectOn-the-Fly Model Checking with Guided Abstraction
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg
Full Thesis textFull thesis text - English Version


Abstract


Model checking is an automatic verification method that gets a system model and a specification, and checks whether the model satisfies the specification.


CTL is a branching time temporal logic suitable for specifying behaviors of both software and hardware systems. It enables specifying properties that cannot be expressed in linear time logics, such as LTL. An example of such a property is restartability, which means that in every reachable state, the system may return to its initial state, due to a reset or a recovery.

Further, in many cases, CTL model checking algorithms can be easily extended to handle the alternation-free fragment of the powerful mu-calculus logic.


In this work, we present a novel approach, OMG, that combines on-the-fly verification with abstraction in order to obtain an efficient CTL model checking algorithm.


On-the-fly verification ensures that only parts that are needed for determining the satisfaction of the specification are developed.

The abstraction is used to form inductive invariants, allowing OMG to determine satisfaction of the CTL specification without traversing the entire state-space.


We formalize the correctness of OMG, and present both an explicit version of the algorithm and a symbolic one.


We implemented our algorithm on top of a combination of explicit and symbolic representations, where symbolic representations are handled with SAT/SMT solvers.

Our experiments show that on a few examples, our algorithm outperforms a state-of-the-art SAT-based algorithm for CTL.