Browsing by Subject "Computer programs--Verification"
Now showing 1 - 10 of 10
- Results Per Page
- Sort Options
Item Efficient and effective symbolic model checking(2006) Iyer, Subramanian Krishnan; Emerson, E. AllenThe main bottleneck in practical symbolic model checking is that it is restricted by the ability to efficiently represent and perform operations on sets of states. Symbolic representations, like Binary Decision Diagrams, grow very large quickly due to their necessity to cover the state space in a breadth first fashion. Satisfiability based techniques result in a proliferation of clauses, one reason being that they have to replicate the transition relation numerous times. We propose techniques to increase the capacity of automatic state-based verification as applied to sequential designs, i.e., symbolic model checking. Firstly, we propose the use of dynamically partitioned ordered Binary Decision Diagrams as a capable data structure. This leads to vast improvements in state space traversal in general and error detection in buggy designs, in particular. Secondly, we propose a partitioned approach to model checking, which splits the problem into multiple partitions handled independently of each other. State space partitioning-based approaches have been proposed in the literature to address the state explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. This algorithm is more suited to parallelization than existing model checking approaches. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude. We address the issue of time scalability in verification, whereby the availability of larger amounts of computation time enables greater exploration of the state space. From a practical standpoint, we observe that extant verification approaches are unable to proceed very deep into the state space. It is our conjecture that partitioning can help in this context and we explore this issue further. Finally, we study the combination of partitioned binary decision diagrams with bounded model checking for more scalable and efficient model checking. We give a technique to scale formal verification to a large grid of processors that demonstrates marked superiority over existing approaches. The contributions of this dissertation are in improving the capacity of symbolic model checking approaches to formal verification, in terms of time and memory requirements, as well as in the development of techniques that are more readily amenable to parallel and distributed model checking.Item Formal verification of computer controlled systems(2007-05) Harutunian, Shant; Hunt, Warren A., 1958-This dissertation discusses the application of formal verification methods to reasoning about the correctness of computer controlled systems. Due to the switching that is introduced by the computer controller, the differential equations associated with such systems may consist of discontinuous vector fields. The physical system may also experience switching due to physical interaction, such as impact. Such system models may exhibit an infinite number of switches in finite time. For example, using rigid body modeling assumptions, a bouncing ball may have infinitely many elastic impacts, but come to rest in finite time. Using nonstandard analysis, we present a model for computer controlled systems which accommodates discontinuous vector fields as well as infinite switches in finite time. This model includes both the semantics of the computer program as well as the ordinary differential equations governing the physical system behavior. We develop a nonstandard definition of a solution for such a model and formally prove that the solution exists. Using this nonstandard definition of solution, we develop proof procedures whereby one may reason about safety and progress properties of the system. The soundness of these proof procedures is formally shown. We conclude with the presentation of a simple example computer controlled system using the presented model, for which safety and progress properties are shown using the respective proof procedures.Item Generalization, lemma generation, and induction in ACL2(2008-05) Erickson, John D., Ph. D.; Moore, J. Strother, 1947-Formal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to find and more costly to fix. Among the formal verification tools available today, theorem provers offer the ability to do the most complete verification of the most complex systems. However, theorem proving requires expert guidance and typically is too costly to be economical for all but the most mission critical systems. Three major challenges to using a theorem prover are: finding generalizations, choosing the right induction scheme, and generating lemmas. In this dissertation we study all three of these in the context of the ACL2 theorem prover.Item Model checking: beyond the finite(2004) Kahlon, Vineet; Emerson, E. AllenItem Observation and verification of software for distributed systems(1995-08) Tomlinson, Alexander Ivor, 1964; Not availableItem Specification and analysis of timing properties in real-time systems(1988) Jahanian, Farnam; Mok, Aloysius Ka-LauThis dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute timing of events. Relative timing concerns the order in which events occur, such as mutual exclusion and precedence constraint properties. Absolute timing concerns the stringent timing restrictions imposed on a system, such as a response time deadline or a minimum elapsed time between occurrences of two events. The approach is based on Real Time Logic (RTL), a logic invented primarily for the specification of both relative and absolute timing of events. The notion of an event occurrence is central to RTL; an event occurrence marks a point in time which is of significance to the behavior of a system. Hence, concurrency is modeled as a partial ordering of the event occurrences in the system. A system specification and a property to be verified can be expressed as arithmetical relations on algebraic expressions involving the event occurrences. To verify the property with respect to the system specification, we prove that the property is a theorem derivable from the specification. Relationship of RTL to Presburger Arithmetic is discussed and a verification technique based on inequality provers is explored. The dissertation also introduces a specification language, Modechart, for real-time systems. The semantics of Modechart is described in terms of RTL formulas. In Modechart, we make use of the concept of modes which can be thought of as partitioning the state space of a system. Intuitively, modes can be viewed as control information that impose structure on the operation of a system. Modes are arranged hierarchically. Furthermore, modes at the same level of hierarchy can be related in one of two ways: in series or in parallel. A transition can be specified between two modes in series, but no transition is allowed between modes in parallel. The language allows sporadic/periodic actions in modes as well as constructs for specifying timing constraints such as delays and deadlines on mode transitions. Verification procedures are introduced for showing a Modechart specification satisfies a property expressed as an RTL formula.Item Symbolic model checking techniques for BDD-based planning in distributed environments(2002-05) Goel, Anuj, 1973-; Barber, Kathleen S.Effective plan specification, solution extraction and plan execution are critical to the ability of single- and multi-agent systems to operate given the dynamism and uncertainties that exist in real-world domains. While much traditional planning research has focused on increasing the tractable search space size for fast and efficient planning, the real-world application of domain-independent planners has suffered due to a lack of corresponding advances with respect to new domain representations, replanning in dynamic and uncertain environments and metric planning. This research implements the Metric Model Checker (MMC) to extend and enhance planning capabilities by applying symbolic model-checking (SMC) techniques for planning in causally specified domains using the causal language, C. SMC is a formal verification technique for propositional satisfiability used to test semantic properties (e.g. Computational Tree Logic) of Boolean domains. C is an action language based on a theory of causal explanation of action effects that supports action preconditions, indirect effects, non-determinism and non-inertial fluents. MMC provides five main capabilities: i) new domain descriptions – MMC translates and compiles C domain descriptions into a format that supports the application of model checking toolkits; ii) extended-goal representations – MMC supports incremental plan generation for multiple, simultaneous temporally-extended goals; iii) replanning – MMC uses BDD representations of generated plan search information to provide intelligent replanning and learning during plan execution in a manner that supports the responsive capabilities of recurrent replanning while providing the goal achievement guarantees gained from precursor methodologies, and iv) metric planning – MMC integrates a linear programming toolkit with its Boolean model-checking algorithms to provide support for plan generation in certain metric (integer-valued) domains while mitigating the state explosion problem; and v) distributed operation – MMC is implemented in a CORBA distributed environment that allows it to be rapidly integrated with existing agent-based systems and supports interaction with external environmental simulators.Item Techniques for formal verification of concurrent and distributed program traces(2004) Sen, Mehmet Alper; Garg, Vijay K. (Vijay Kumar), 1963-Traditional approaches for eliminating errors in concurrent and distributed programs include formal methods and testing. This dissertation presents an approach toward combining formal methods and testing, while avoiding the complexity of model checking or theorem proving and the pitfalls of ad hoc testing. Our technique enables efficient formal verification of specifications on execution traces of actual scalable systems. By allowing an observer to analyze a partial order trace rather than a total order trace, we get the benefit of properly dealing with concurrent events and especially of detecting errors from analyzing successful executions, errors which can occur under a different thread scheduling. Surprisingly, temporal logic model checking even on a finite partial order trace is NP-complete in the size of the trace description. We develop techniques to combat the state explosion problem. Our algorithms have polynomial-time complexity in the size of the trace description as opposed to exponential. We suggest the use of an abstraction technique called slicing. Intuitively, the “slice” of a trace with respect to a predicate (specification) is a sub-trace that contains all the global states of the trace that satisfy the predicate such that it is computed efficiently (without traversing the state space) and represented concisely (without explicit representation of individual states). We present off-line and on-line slicing algorithms with respect to predicates in a subset of temporal logic CTL. We also show that the slicing problem is equivalent to the problem of detecting whether there exists at least one global state of the trace that satisfies the predicate. We develop efficient algorithms to detect several useful classes of predicates. In particular, we show how to use the slicing algorithms to detect predicates in a subset of temporal logic CTL. We also present efficient detection algorithms for predicates that do not allow efficient slicing. We have developed a prototype system Partial Order Trace Analyzer (POTA), which implements our algorithms. We verify several scalable and industrial protocols including CORBA’s GIOP, ISO’s ATMR, cache coherence and mutual exclusion. Our experimental results indicate that slicing can lead to exponential reduction over existing techniques both in time and space.Item Three essays on the interface of computer science, economics and information systems(2007) Hidvégi, Zoltán Tibor, 1970-; Whinston, Andrew B.This thesis looks at three aspects related to the design of E-commerce systems, online auctions and distributed grid computing systems. We show how formal verification techniques from computer science can be applied to ensure correctness of system design and implementation at the code level. Through e-ticket sales example, we demonstrate that model checking can locate subtle but critical flaws that traditional control and auditing methods (e.g., penetration testing, analytical procedure) most likely miss. Auditors should understand formal verification methods, enforce engineering to use them to create designs with less of a chance of failure, and even practice formal verification themselves in order to offer credible control and assistance for critical e-systems. Next, we study why many online auctions offer fixed buy prices to understand why sellers and auctioneers voluntarily limit the surplus they can get from an auction. We show when either the seller of the dibbers are risk-averse, a properly chosen fixed permanent buy-price can increase the social surplus and does not decrease the expected utility of the sellers and bidders, and we characterize the unique equilibrium strategies of uniformly risk-averse buyers in a buy-price auction. In the final chapter we look at the design of a distributed grid-computing system. We show how code-instrumentation can be used to generate a witness of program execution, and show how this witness can be used to audit the work of self-interested grid agents. Using a trusted intermediary between grid providers and customers, the audit allows payment to be contingent on the successful audit results, and it creates a verified reputation history of grid providers. We show that enabling the free trade of reputations provides economic incentives to agents to perform the computations assigned, and it induces increasing effort levels as the agents' reputation increases. We show that in such a reputation market only high-type agents would have incentive to purchase a high reputation, and only low-type agents would use low reputations, thus a market works as a natural signaling mechanism about the agents' type.Item Using theorem proving and algorithmic decision procedures for large-scale system verification(2005) Ray, Sandip; Moore, J Strother, 1947-The goal of formal verification is to use mathematical methods to prove that a computing system meets its specifications. When applicable, it provides a higher assurance than simulation and testing in correct system execution. However, the capacity of the state of the art in formal verification today is still far behind what is necessary for its widespread adoption in practice. In this dissertation, we devise methods to increase the capacity of formal verification. Formal verification techniques can be broadly divided into two categories, namely deductive techniques or theorem proving, and decision procedures such as model checking, equivalence checking, and symbolic trajectory evaluation. Neither deductive nor algorithmic techniques individually scale up to the size of modern industrial systems, albeit for orthogonal reasons. Decision procedures suffer from state explosion. Theorem proving requires manual assistance. Our methods involve a sound, efficient, and scalable integration of deductive and algorithmic techniques. ix There are four main contributions in this dissertation. First, we present several results that connect different deductive proof styles used in the verification of sequential programs. The connection allows us to efficiently combine theorem proving with symbolic simulation to prove the correctness of sequential programs without requiring a verification condition generator or manual construction of a global invariant. Second, we formalize a notion of correctness for reactive concurrent programs that affords effective reasoning about infinite computations. We discuss several reduction techniques that reduce the correctness proofs of concurrent programs to the proof of an invariant. Third, we present a method to substantially automate the process of discovering and proving invariants of reactive systems. The method combines term rewriting with reachability analysis to generate efficient predicate abstractions. Fourth, we present an approach to integrate model checking procedures with deductive reasoning in a sound and efficient manner. We use the ACL2 theorem prover to demonstrate our methods. A consequence of our work is the identification of certain limitations in the logic and implementation of ACL2. We recommend several augmentations of ACL2 to facilitate deductive verification of large systems and integration with decision procedures.