Component verification with automatically generated assumptions

Dimitra Giannakopoulou, Corina S. Pǎsǎreanu, Howard Barringer

    Research output: Contribution to journalArticlepeer-review


    Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications. © 2005 Springer Science + Business Media, Inc.
    Original languageEnglish
    Pages (from-to)297-320
    Number of pages23
    JournalAutomated Software Engineering
    Issue number3
    Publication statusPublished - Jul 2005


    • Assume-guarantee reasoning
    • Component verification
    • Model checking


    Dive into the research topics of 'Component verification with automatically generated assumptions'. Together they form a unique fingerprint.

    Cite this