The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Um método de verificação de suposição de garantia foi reconhecido como uma abordagem promissora para verificar software baseado em componentes por meio de verificação de modelo. Este método não é apenas adequado para software baseado em componentes, mas também tem potencial para resolver o problema da explosão do espaço de estados na verificação de modelos. O método nos permite decompor um alvo de verificação em componentes para que possamos modelar a verificação de cada um deles separadamente. Neste método, as suposições são vistas como os ambientes necessários para que os componentes satisfaçam uma propriedade e para que o resto do sistema seja satisfeito. O número de estados das suposições deve ser minimizado porque o custo computacional da verificação do modelo é influenciado por esse número. Assim, propomos um método para gerar suposições mínimas para a verificação de suposição-garantia de software baseado em componentes. A ideia chave deste método é encontrar as suposições mínimas nos espaços de busca das suposições candidatas. As suposições mínimas geradas pelo método proposto podem ser usadas para verificar novamente todo o sistema com um custo computacional muito menor. Implementamos uma ferramenta para gerar as suposições mínimas. Resultados experimentais também são apresentados e discutidos.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copiar
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
Copiar
@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},}
Copiar
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 -