Verification of evolving software via component substitutability analysis |
| |
Authors: | Sagar Chaki Edmund Clarke Natasha Sharygina Nishant Sinha |
| |
Affiliation: | (1) Software Engineering Institute, Pittsburgh, USA;(2) School of Computer Science, Pittsburgh, USA;(3) Universita della Svizzera Italiana, Lugano, Switzerland;(4) Electrical and Computer Engineering Department, Carnegie Mellon University, Pittsburgh, USA |
| |
Abstract: | This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two
techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations
obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning algorithm—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, our solution
generates constructive feedback to developers showing how to improve the components. The substitutability approach has been
implemented and validated in the ComFoRT reasoning framework, and we report encouraging results on an industrial benchmark.
This is an extended version of a paper, Dynamic Component Substitutability Analysis, published in the Proceedings of the Formal Methods 2005 Conference, Lecture Notes in Computer Science, vol. 3582, by the
same authors. This research was sponsored by the National Science Foundation under grant nos. CNS-0411152, CCF-0429120, CCR-0121547,
and CCR-0098072, the Semiconductor Research Corporation under grant no. TJ-1366, the US Army Research Office under grant no.
DAAD19-01-1-0485, the Office of Naval Research under grant no. N00014-01-1-0796, the ICAST project and the Predictable Assembly
from Certifiable Components (PACC) initiative at the Software Engineering Institute, Carnegie Mellon University. The views
and conclusions contained in this document are those of the authors and should not be interpreted as representing the official
policies, either expressed or implied, of any sponsoring institution, the US government or any other entity. |
| |
Keywords: | Compositional verification Assume-guarantee reasoning Automata learning Predicate abstraction Software engineering Model checking |
本文献已被 SpringerLink 等数据库收录! |
|