|
Published Articles >> Table of Contents >> Abstract
17th IEEE International Conference on Automated Software Engineering (ASE'02)
p. 3
Assumption Generation for Software Component Verification
Dimitra Giannakopoulou, NASA Ames Research Center
Corina S. Pasareanu, NASA Ames Research Center
Howard Barringer, University of Manchester
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2002.1114984
Send link to a friend
| 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 defines a framework that brings a new dimension to model checking of software components. When checking a component against a property, our 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 a NASA application.
|
 Additional Information
|
Citation:
Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer,
"Assumption Generation for Software Component Verification,"
ase,
p. 3,
17th IEEE International Conference on Automated Software Engineering (ASE'02),
2002
|
|
