Component Verification with Automatically Generated Assumptions |
| |
Authors: | Email author" target="_blank">Dimitra?GiannakopoulouEmail author Corina?S?P?s?reanu Howard?Barringer |
| |
Affiliation: | (1) RIACS/USRA, NASA Ames Research Center, Moffett Field, CA 94035-1000, USA;(2) Kestrel Technology LLC, NASA Ames Research Center, Moffett Field, CA 94035-1000, USA;(3) School of Computer Science, University of Manchester, Oxford Road, Manchester, M13 9PL, UK |
| |
Abstract: | 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.This paper is an expanded version of Giannakopoulou et al. (2002). |
| |
Keywords: | assume-guarantee reasoning model checking component verification |
本文献已被 SpringerLink 等数据库收录! |
|