2018 Fiscal Year Annual Research Report
Liveness verification in software model checking
| Project/Area Number |
16K00109
|
|---|
| Research Institution | Tsurumi University |
|---|
Principal Investigator |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | モデル検査 / Java / ソフトウェア |
|---|
| Outline of Annual Research Achievements |
平成30年度には，Java PathFinder (JPF) に関して前年度に行った実装をもとに，以下の改良を行った．キャッシュ情報が得られない場合の対処として，前年度に，(1)探索の再実行・(2)復元情報事前保存 の2オプションを融合する実装を行ったことを受けて，本年度は選択基準の設定を行った．部分探索によって取得することによって得られるブランチング数や探索済み状態到達率等の指標に依存して遷移回数間隔を決定するというものである．先行研究でも採用したベンチマークセットを用いた実験によって回数を定めた．
Coq (SSReflect) によるアルゴリズムの形式検証についても，前年度の結果を受けて改良を行った．Petri-netを用いた検証に関しては，被覆可能性の証明に用いられるKarp-Miller Tree の構成の形式化を完成し，この正当性証明を行った．なお，通常の証明では古典演繹が入ってくるところも，それを避けて，Coqが持っている体系内で証明を行うことができた．この成果に関連して，他のグラフ構造における表現可能なデータ数をCoqで形式化する試みも行った．
さらに，JPFで実現されている記号実行手法を応用し，また上記開発で用いたツールを流用して，プログラムの理解を問う問題を自動作成する手法の開発を行った．作成対象となるプログラム (関数) とインバリアントを指定して，インバリアントから自動的に生成される論理式を満たすための入力セットを，動的記号実行によって獲得するという手法であり，生成ツールの作成と生成された問題の評価を行った．
|
Research Products
(4 results)
