Bounded model checking for asynchronous concurrent systems

Open Access

Abstract

Complex hardware systems become more and more ubiquitous in mission critical applications such as military, satellite, and medical to name but a few. In such applications, reliability remains a primary concern because a failure that occurs during their normal operations might produce important catastrophes like loss of life or loss of money. All these failures are often caused by minuscule bug that exists inside the software which controls the systems, or within the hardware itself. In addition, most of these systems cannot be interrupted while working, even for a few seconds a year, making it difficult to repair bugs found during their normal operations. The main purpose of this work is to build efficient verification techniques for asynchronous concurrent systems. Because of the pivotal roles these systems assume in a given application, designers of such systems must keep development and maintenance costs under control and meet nonfunctional constraints on the design of the system, such as cost, power, weight, or the system architecture by itself. But most importantly, they must assure their customer as well as the certification authorities that both the design and its implementation are correct. Otherwise, they may end up shipping unsafe systems to the market, and the consequences of this action would be catastrophic. To achieve this goal, designers need efficient methods and tools to assist them in verifying the correctness of the design. In this thesis we focus on a symbolic model checking technique called bounded model checking (BMC). BMC is a method targeted mainly at finding bugs in a system. It answers the questions whether there exists a counterexample, shorter than a given length, that violates a given property. During a BMC operation each execution path is encoded into Boolean formula, and the problem is reduced to satisfiability checking of the formula. Therefore, the operation consists mainly in constructing a Boolean formula that is satisfiable if and only if such a counterexample exists. We model ...