Summary
|
For Full-Text 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. |
|
A Minimized Assumption Generation Method for Component-Based Software Verification Ngoc Hung PHAM Viet Ha NGUYEN Toshiaki AOKI Takuya KATAYAMA Publication IEICE TRANSACTIONS on Information and Systems Vol.E93-D No.8 pp.2172-2181 Publication Date: 2010/08/01 Online ISSN: 1745-1361 DOI: 10.1587/transinf.E93.D.2172 Print ISSN: 0916-8532 Type of Manuscript: PAPER Category: Software System Keyword: model checking, assume-guarantee reasoning, modular verification, learning algorithm, minimal assumption, Full Text: PDF(319.8KB)>>
Summary: An assume-guarantee verification method has been recognized as a promising approach to verify component-based software by model checking. This method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. The method allows us to decompose a verification target into components so that we can model check each of them separately. In this method, assumptions are seen as the environments needed for the components to satisfy a property and for the rest of the system to be satisfied. The number of states of the assumptions should be minimized because the computational cost of model checking is influenced by that number. Thus, we propose a method for generating minimal assumptions for the assume-guarantee verification of component-based software. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. We have implemented a tool for generating the minimal assumptions. Experimental results are also presented and discussed. | ||||||||||
| ||||||||||
