Towards Infinite-State Symbolic Model Checking for B and Event-B

Abstract

The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in 1949 or Robert W. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working towards an implementation of a “verifying compiler”. King’s idea has later been stated as a “Grand Challenge for Computing Research” by Tony Hoare in 2005. Idealism however is not the only reason for software verification. According to a study performed in 2002 by the U.S. National Institute of Standards & Technology, the U.S. economy suffers a loss of close to $60 billion per year due to software errors. Furthermore, errors have directly led to deaths or serious injuries, as well as failure or loss of equipment. Within typical software engineering approaches, testing and static analysis tools are used to limit the possibility of software errors. Several holistic approaches to software development have been designed in order to keep bug counts low throughout the whole development cycle. This thesis focuses on a more rigorous approach to the development of software: the usage of formal methods. In particular, it is concerned with improving the ProB model checker by augmenting its original explicit state model checker with a symbolic counterpart. In this way we broaden the scope of problems to which ProB can be applied. As symbolic model checking makes heavy use of constraint solving, one aspect of this thesis is to implement methods to increase the performance of ProB’s constraint solving kernel. This will be achieved by two means. First, by improving the constraint solver itself, mainly by lifting it from finite to infinite-state problems. Second, we developed an integration of ProB with the SMT solvers CVC4 and Z3, combining them into a single procedure. Following, this thesis will present different symbolic model checking algorithms and evaluate them regarding their applicability to B and Event-B. Some suitable algorithms, namely Bounded Model Checking, k-Induction and IC3 were implemented inside ProB. Both the improved constraint solver alone and the symbolic model checking algorithms will be evaluated on different examples ranging from solving B predicates, proving, disproving and SMT solving to model checking of academic and industrial specifications.

Type
Publication
Dissertation submitted to the Heinrich-Heine-University Düsseldorf, Germany
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.