
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

On Optimization of Minimized Assumption Generation Method for ComponentBased Software Verification
Ngoc Hung PHAM Viet Ha NGUYEN Toshiaki AOKI Takuya KATAYAMA
Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Vol.E95A
No.9
pp.14511460 Publication Date: 2012/09/01
Online ISSN: 17451337
DOI: 10.1587/transfun.E95.A.1451
Print ISSN: 09168508 Type of Manuscript: Special Section PAPER (Special Section on Software Reliability Engineering) Category: Keyword: model checking, assumeguarantee reasoning, modular verification, learning algorithm, minimal assumption,
Full Text: PDF>>
Summary:
The minimized assumption generation has been recognized as an important improvement of the assumeguarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole componentbased software at a lower computational cost. The method is not only fitted to componentbased software but also has a potential to solve the state space explosion problem in model checking. However, the computational cost for generating the minimal assumption is very high so the method is difficult to be applied in practice. This paper presents an optimization as a continuous work of the minimized assumption generation method in order to reduce the complexity of the method. The key idea of this method is to find a smaller assumption in a subtree of the search tree containing the candidate assumptions using the depthlimited search strategy. With this approach, the improved method can generate assumptions with a lower computational cost and consumption memory than the minimized method. The generated assumptions are also effective for rechecking the systems at much lower computational cost in the context of software evolution. An implemented tool supporting the improved method and experimental results are also presented and discussed.

