Software Engineering Institute Carnegie Mellon

Verification of Evolving Software via Component Substitutability Analysis

Sagar Chaki
Edmund Clarke
Natasha Sharygina
Nishant Sinha

Technical Report
CMU/SEI-2005-TR-008

PDF File

Formal verification by model checking has the potential to produce major enhancements in the reliability and robustness of software. However, a shortcoming in most model checking research is the failure to consider how to make the use of model checking routine throughout various stages of software development. This report presents results of the Independent Research and Development (IRAD) project on verification of evolving software conducted at the Software Engineering Institute in 2005. The research conducted as part of the IRAD project considered ways to reduce the effort of subsequent verifications. In particular, it resulted in the development of techniques that exploit the results of previous verification efforts and focus only on the portions of the system that have changed (components). Thus, these new techniques incorporate model checking into development processes in a much less intrusive or cumbersome manner than previous verification techniques.

The report presents an automated and compositional procedure to solve the component substitutability problem. The solution contributes two techniques for checking the correctness of software upgrades: (1) a technique based on simultaneous use of overapproximations and underapproximations obtained via existential and universal abstractions and (2) a dynamic assume-guarantee reasoning algorithm in which previously generated component assumptions are reused and altered “on the fly” to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, the solution generates constructive feedback that shows developers how to improve the components. The substitutability approach has been implemented and validated in the Component Formal Reasoning Technology (COMFORT) model checking tool set. The experimental evaluation of an industrial benchmark demonstrates encouraging results.