Bounded model checking for asynchronous concurrent systems

摘要: Complex hardware systems become more and ubiquitous in mission critical applications such as military, satellite, medical to name but a few. In applications, reliability remains primary concern because failure that occurs during their normal operations might produce important catastrophes like loss of life or money. All these failures are often caused by minuscule bug exists inside the software which controls systems, within itself. addition, most cannot be interrupted while working, even for few seconds year, making it difficult repair bugs found operations. The main purpose this work is build efficient verification techniques asynchronous concurrent systems. Because pivotal roles assume given application, designers must keep development maintenance costs under control meet nonfunctional constraints on design system, cost, power, weight, system architecture But importantly, they assure customer well certification authorities both its implementation correct. Otherwise, may end up shipping unsafe market, consequences action would catastrophic. To achieve goal, need methods tools assist them verifying correctness design. In thesis we focus symbolic model checking technique called bounded (BMC). BMC method targeted mainly at finding system. It answers questions whether there counterexample, shorter than length, violates property. During operation each execution path encoded into Boolean formula, problem reduced satisfiability formula. Therefore, consists constructing formula satisfiable if only counterexample exists. We our with transition (TSs). particular, interested synchronized product TSs. Since formed combination several components communicating between other, TSs well-suited capture behavior The executions commonly modeled using so-called interleaving execution, allows one single event fire step. However, due complexity inteleaving will not require many steps also generate long formulas. work, adopt another approach based breadth-first search (BFS). operation, translation polynomial size model, solving time can exponential research hypothesis improve efficiency generating succinct minimizing number necessary an execution. We introduce aimed improving grouped two parts (i) reachability properties (ii) written linear temporal logic (LTL). propose some bound. We implemented all toolset. At dissertation, discuss experimental results obtained.