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...

• Type: Journal
• Year: 2005
• Where: ASE
• Authors: Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer
• Keywords: ASE 2005, Certain Required Properties, Checking, Software Components