Font Size: a A A

Model checking for open systems: A compositional approach to software verification

Posted on:2002-05-06Degree:Ph.DType:Dissertation
University:University of FloridaCandidate:Andrade-Gomez, Hector AdolfoFull Text:PDF
GTID:1468390011994441Subject:Computer Science
Abstract/Summary:
Increasingly, software systems are being constructed from existing components. This has the potential to reduce costs and increase reliability, provided that the components can be specified and verified in such a way that it is possible to reason about the composed system. The goal of this dissertation is to explore the possibility of using a standard logic and its verification tools for open systems: systems that are intended to be used as components in a larger system.;We specify a component with a set of properties expressed in a basic logic---here we use CTL---along with a higher-order property called "guarantees" properties. The guarantees properties of a component say something about the behavior of systems containing the component, provided the systems themselves satisfy certain constraints. The idea is that while the guarantees properties for a component may be fairly expensive to verify, typically requiring some deduction along with model checking, this is tolerable since the verification needs to be done only once for the component. The constraints on the system need to be verified each time the component is used and thus should be easier to verify, usually with model checking only. This asymmetry is not present in compositional approaches with different goals, for example, reducing the state explosion in automatic techniques for verification of temporal properties.;Guarantees properties impose constraints on the entire system in which a component is embedded. In order to facilitate checking these properties, we identify useful subsets of properties expressed in CTL, called universal and existential properties, that are amenable to compositional checking. Universal properties hold in a system if they hold for all components, while existential properties hold in a system if they hold for any component. Constraints expressed using existential and universal properties can be checked separately on each component of the system.;The domain to which this theory can be applied usefully is limited to systems that can be modeled accurately with finite state concurrent systems, and the specification of which consists of a set of temporal properties.
Keywords/Search Tags:Systems, Model checking, Component, Compositional, Verification
Related items