This paper presents a completely automated and compositional procedure to solve the substitutability problem in the context of component-based software and safety specifications. Our solution proposes the use of dynamic assume-guarantee reasoning -- previously generated assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. Moreover, our technique supports simultaneous upgrades of multiple components. Finally, our framework provides feedback to developers. We have implemented and validated our approach in the ComFoRT reasoning framework and report encouraging results on an industrial benchmark.
In Proceedings of the Formal Methods 2005 conference,
2005, 16 pages.
PostScript(gz) /
PDF
© 2005 Natasha Sharygina.