
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 Locally Minimum and Strongest Assumption Generation Method for ComponentBased Software Verification
HoangViet TRAN Ngoc Hung PHAM Viet Ha NGUYEN
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E102D
No.8
pp.14491461 Publication Date: 2019/08/01
Online ISSN: 17451361
DOI: 10.1587/transinf.2018FOP0004
Type of Manuscript: Special Section PAPER (Special Section on Formal Approaches) Category: Keyword: assumeguarantee reasoning, model checking, software verification, locally minimum assumption, locally strongest assumption,
Full Text: PDF>>
Summary:
Since software becomes more complex during its life cycle, the verification cost becomes higher, especially for such methods which are using model checking in general and assumeguarantee reasoning in specific. To address the problem of reducing the assumeguarantee verification cost, this paper presents a method to generate locally minimum and strongest assumptions for verification of componentbased software. For this purpose, we integrate a variant of membership queries answering technique to an algorithm which considers candidate assumptions that are smaller and stronger first, larger and weaker later. Because the algorithm stops as soon as it reaches a conclusive result, the generated assumptions are the locally minimum and strongest ones. The correctness proof of the proposed algorithm is also included in the paper. An implemented tool, test data, and experimental results are presented and discussed.

