Sciweavers

Share
ASE
2005

Component Verification with Automatically Generated Assumptions

11 years 9 months ago
Component Verification with Automatically Generated Assumptions
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 a verification 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...
Dimitra Giannakopoulou, Corina S. Pasareanu, Howar
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where ASE
Authors Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer
Comments (0)
books