A Minimized Assumption Generation Method for Component-Based Software Verification

DOI Web Site 参考文献28件
  • PHAM Ngoc Hung
    College of Technology, Vietnam National University
  • NGUYEN Viet Ha
    College of Technology, Vietnam National University
  • AOKI Toshiaki
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • KATAYAMA Takuya
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)

この論文をさがす

抄録

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.

収録刊行物

参考文献 (28)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ