Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software

Ngoc Hung PHAM  Toshiaki AOKI  Takuya KATAYAMA  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E92-A   No.11   pp.2772-2780
Publication Date: 2009/11/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E92.A.2772
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Theory of Concurrent Systems and its Applications)
Category: 
Keyword: 
model checking,  assume-guarantee reasoning,  modular verification,  component evolution,  conformance testing,  

Full Text: PDF>>
Buy this Article




Summary: 
This paper proposes a framework for modular verification of evolving component-based software. This framework includes two stages: modular conformance testing for updating inaccurate models of the evolved components and modular verification for evolving component-based software. When a component is evolved after adapting some refinements, the proposed framework focuses on this component and its model in order to update the model and recheck the whole evolved system. The framework also reuses the previous verification results and the previous models of the evolved components to reduce the number of steps required in the model update and modular verification processes. An implementation and some experimental results are presented.