Title: Assumption generation for software component verification
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.
Publication Year: 2002
Publication Date: 2002-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 182
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot