A Minimized Assumption Generation Method for Component-Based Software Verification

Ngoc Hung PHAM; Viet Ha NGUYEN; Toshiaki AOKI; Takuya KATAYAMA

doi:10.1587/transinf.E93.D.2172

A Minimized Assumption Generation Method for Component-Based Software Verification

Ngoc Hung PHAM, Viet Ha NGUYEN, Toshiaki AOKI, Takuya KATAYAMA

Full Text Views

0

Cite this

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.

Publication: IEICE TRANSACTIONS on Information Vol.E93-D No.8 pp.2172-2181

Publication Date: 2010/08/01

Publicized

Online ISSN: 1745-1361

DOI: 10.1587/transinf.E93.D.2172

Type of Manuscript: PAPER

Category: Software System

Cite this

Copy

Ngoc Hung PHAM, Viet Ha NGUYEN, Toshiaki AOKI, Takuya KATAYAMA, "A Minimized Assumption Generation Method for Component-Based Software Verification" in IEICE TRANSACTIONS on Information, vol. E93-D, no. 8, pp. 2172-2181, August 2010, doi: 10.1587/transinf.E93.D.2172.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E93.D.2172/_p

Copy

@ARTICLE{e93-d_8_2172,
author={Ngoc Hung PHAM, Viet Ha NGUYEN, Toshiaki AOKI, Takuya KATAYAMA, },
journal={IEICE TRANSACTIONS on Information},
title={A Minimized Assumption Generation Method for Component-Based Software Verification},
year={2010},
volume={E93-D},
number={8},
pages={2172-2181},
abstract={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.},
keywords={},
doi={10.1587/transinf.E93.D.2172},
ISSN={1745-1361},
month={August},}

Copy

TY - JOUR
TI - A Minimized Assumption Generation Method for Component-Based Software Verification
T2 - IEICE TRANSACTIONS on Information
SP - 2172
EP - 2181
AU - Ngoc Hung PHAM
AU - Viet Ha NGUYEN
AU - Toshiaki AOKI
AU - Takuya KATAYAMA
PY - 2010
DO - 10.1587/transinf.E93.D.2172
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E93-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2010
AB - 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.
ER -