Search T-Space Advanced Search
Home

Browse
Communities
& Collections

Issue Date
Author
Title
Subject

Sign on to:
Receive email
updates

My Account
authorized users

Edit Profile

Help
About T-Space
 Please use this identifier to cite or link to this item: http://hdl.handle.net/1807/17453

 Title: Approximation and Refinement Techniques for Hard Model-checking Problems Authors: Bobaru, Mihaela Advisor: Chechik, Marsha Department: Computer Science Keywords: formal methodsmodel checkingsoftware verificationhardware verification Issue Date: 15-Jul-2009 Abstract: Formal verification by model checking verifies whether a system satisfies some given correctness properties, and is intractable in general. We focus on several problems originating from the usage of model checking and from the inherent complexity of model checking itself. We propose approximation and iterative refinement techniques and demonstrate that they help in making these problems tractable on practical cases. Vacuity detection is one of the problems, relating to the trivial satisfaction of properties. A similar problem is query solving, useful in model exploration, when properties of a system are not fully known and are to be discovered rather than checked. Both of these problems have solution spaces structured as lattices and can be solved by model checking using those lattices. The lattices, in the most general formulation of these problems, are too complex to be implemented efficiently. We introduce a general approximation framework for model checking with lattices and instantiate this framework for the two problems, leading to algorithms and implementations that can obtain efficiently partial answers to the problems. We also introduce refinement techniques that consider incrementally larger lattices and compute even the partial answers gradually, to further abate the size explosion of the problems. Another problem we consider is the state-space explosion of model checking. The size of system models is exponential in the number of state variables and that renders model checking intractable. We consider systems composed of several components running concurrently. For such systems, compositional verification checks components individually to avoid composing an entire system. Model checking an individual component uses assumptions about the other components. Smaller assumptions lead to smaller verification problems. We introduce iterative refinement techniques that improve the assumptions generated by previous automated approaches. One technique incrementally refines the interfaces between components in order to obtain smaller assumptions that are sufficient to prove a given property. The smaller assumptions are approximations of the assumption that would be obtained without our interface refinement. Another technique computes assumptions as abstractions of components, as an alternative to current approaches that learn assumptions from counterexamples. Our abstraction refinement has the potential to compute smaller nondeterministic assumptions, in contrast to the deterministic assumptions learned by current approaches. We confirm experimentally the benefits of our new approximation and refinement techniques. URI: http://hdl.handle.net/1807/17453 Appears in Collections: DoctoralDepartment of Computer Science - Doctoral theses

Files in This Item:

File Description SizeFormat
Bobaru_Mihaela_200903_PhD_Thesis.pdf838.22 kBAdobe PDF
View/Open

This item is licensed under a Creative Commons License

Items in T-Space are protected by copyright, with all rights reserved, unless otherwise indicated.