Browsing by Subject "Model checking"
Now showing 1 - 3 of 3
- Results Per Page
- Sort Options
Item Applications of lattice theory to model checking(2008-08) Kashyap, Sujatha; Garg, Vijay K. (Vijay Kumar), 1963-Society is increasingly dependent on the correct operation of concurrent and distributed software systems. Examples of such systems include computer networks, operating systems, telephone switches and flight control systems. Model checking is a useful tool for ensuring the correctness of such systems, because it is a fully automatic technique whose use does not require expert knowledge. Additionally, model checking allows for the production of error trails when a violation of a desired property is detected. Error trails are an invaluable debugging aid, because they provide the programmer with the sequence of events that lead to an error. Model checking typically operates by performing an exhaustive exploration of the state space of the program. Exhaustive state space exploration is not practical for industrial use in the verification of concurrent systems because of the well-known phenomenon of state space explosion caused by the exploration of all possible interleavings of concurrent events. However, the exploration of all possible interleavings is not always necessary for verification. In this dissertation, we show that results from lattice theory can be applied to ameliorate state space explosion due to concurrency, and to produce short error trails when an error is detected. We show that many CTL formulae exhibit lattice-theoretic structure that can be exploited to avoid exploring multiple interleavings of a set of concurrent events. We use this structural information to develop efficient model checking techniques for both implicit (partial order) and explicit (interleaving) models of the state space. For formulae that do not exhibit the required structure, we present a technique called predicate filtering, which uses a weaker property with the desired structural characteristics to obtain a reduced state space which can then be exhaustively explored. We also show that lattice theory can be used to obtain a path of shortest length to an error state, thereby producing short error trails that greatly ease the task of debugging. We provide experimental results from a wide range of examples, showing the effectiveness of our techniques at improving the efficiency of verifying and debugging concurrent and distributed systems. Our implementation is based on the popular model checker SPIN, and we compare our performance against the state-of-the-art state space reduction strategies implemented in SPIN.Item Backward and parallel exploration techniques for Java PathFinder(2017-05-08) Mahboob, Muhammad Raza; Khurshid, SarfrazModel checking software programs is an effective approach for finding bugs in program by systematically exploring the entire program's state space. One big issue with model checker is state space explosion. Recent research techniques like Partial Order Reduction and symmetry reductions help in reducing the state explosion but it is still infeasible to model check real world programs. JPF is one such explicit-state model checker designed for Java programs and provides non-deterministic choices and thread scheduling control. JPF uses state backtracking and state comparison to eliminate states that are already executed in the past but still cannot cope with state explosion. We tackle this problem in a different way i.e. by enabling concurrent execution of the state space by different workers. The key insight here is to be able to explore the state space from an arbitrary point and be able to go in any direction i.e. backwards or forwards. We present a new search strategy to explore state space. Using this, we can arbitrarily divide the search space into multiple workers without having to worry about expensive state comparisons or transmitting them on network. However this may result in non-equal division of work between the workers because of the inherent underlying search tree. We further build on this work to develop a near optimal work partitioning strategy by employing Work Sharing and Work Stealing approaches instead of static state partitioning using hash sets. Our techniques help in automated test generation and general state exploration for bug finding. We introduce a novel approach to divide the search space, for concurrent execution, without incurring network communication overhead and build on that to provide a more work optimal solution. We evaluated the technique on standard single and multi-threaded Java programs to show the efficacy of our approach.Item Fast error detection with coverage guarantees for concurrent software(2013-05) Coons, Katherine Elizabeth; McKinley, Kathryn S.Concurrency errors are notoriously difficult to debug because they may occur only under unexpected thread interleavings that are difficult to identify and reproduce. These errors are increasingly important as recent hardware trends compel developers to write more concurrent software and to provide more concurrent abstractions. This thesis presents algorithms that dynamically and systematically explore a program's thread interleavings to manifest concurrency bugs quickly and reproducibly, and to provide precise incremental coverage guarantees. Dynamic concurrency testing tools should provide (1) fast response -- bugs should manifest quickly if they exist, (2) reproducibility -- bugs should be easy to reproduce and (3) coverage -- precise correctness guarantees when no bugs manifest. In practice, most tools provide either fast response or coverage, but not both. These goals conflict because a program's thread interleavings exhibit exponential state- space explosion, which inhibits fast response. Two approaches from prior work alleviate state-space explosion. (1) Partial-order reduction provides full coverage by exploring only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating only interleavings that do not exceed a bound. Bounded search can additionally provide guarantees for cyclic state spaces for which dynamic partial-order reduction provides no guarantees. Without partial-order reduction, however, bounded search wastes most of its time exploring executions that reorder only independent transitions. Fast response with coverage guarantees requires both approaches, but prior work failed to combine them soundly. We combine bounded search with partial-order reduction and extensively analyze the space of dynamic, bounded partial-order reduction strategies. First, we prioritize with a best-first search and show that heuristics that combine these approaches find bugs quickly. Second, we restrict partial-order reduction to combine approaches while maintaining bounded coverage. We specialize this approach for several bound functions, prove that these algorithms guarantee bounded coverage, and leverage dynamic information to further reduce the state space. Finally, we bound the partial order on a program's transitions, rather than the total order on those transitions, to combine these approaches without sacrificing partial-order reduction. This algorithm provides fast response, incremental coverage guarantees, and reproducibility. We manifest bugs an order of magnitude more quickly than previous approaches and guarantee incremental coverage in minutes or hours rather than weeks, helping developers find and reproduce concurrency errors. This thesis makes bounded stateless model checking for concurrent programs substantially more efficient and practical.