On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification
Summary :
The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based 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 sub-tree of the search tree containing the candidate assumptions using the depth-limited 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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E95-A No.9 pp.1451-1460
- Publication Date
- 2012/09/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1587/transfun.E95.A.1451
- Type of Manuscript
- Special Section PAPER (Special Section on Software Reliability Engineering)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
Copy
Ngoc Hung PHAM, Viet Ha NGUYEN, Toshiaki AOKI, Takuya KATAYAMA, "On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification" in IEICE TRANSACTIONS on Fundamentals,
vol. E95-A, no. 9, pp. 1451-1460, September 2012, doi: 10.1587/transfun.E95.A.1451.
Abstract: The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based 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 sub-tree of the search tree containing the candidate assumptions using the depth-limited 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E95.A.1451/_p
Copy
@ARTICLE{e95-a_9_1451,
author={Ngoc Hung PHAM, Viet Ha NGUYEN, Toshiaki AOKI, Takuya KATAYAMA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification},
year={2012},
volume={E95-A},
number={9},
pages={1451-1460},
abstract={The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based 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 sub-tree of the search tree containing the candidate assumptions using the depth-limited 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.},
keywords={},
doi={10.1587/transfun.E95.A.1451},
ISSN={1745-1337},
month={September},}
Copy
TY - JOUR
TI - On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1451
EP - 1460
AU - Ngoc Hung PHAM
AU - Viet Ha NGUYEN
AU - Toshiaki AOKI
AU - Takuya KATAYAMA
PY - 2012
DO - 10.1587/transfun.E95.A.1451
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E95-A
IS - 9
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - September 2012
AB - The minimized assumption generation has been recognized as an important improvement of the assume-guarantee verification method in order to generate minimal assumptions. The generated minimal assumptions can be used to recheck the whole component-based software at a lower computational cost. The method is not only fitted to component-based 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 sub-tree of the search tree containing the candidate assumptions using the depth-limited 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.
ER -
English
