2020 Fiscal Year Annual Research Report
Specification Mining and Reasoning about Programs for Verifying Systems with Infinite Structures
| Project/Area Number |
18K11432
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 計算論理 / プログラム推論 / パターン発見 |
|---|
| Outline of Annual Research Achievements |
本研究では，リアクティブ・システムなどのソフトウェアを対象に，その正当性を検証する検証システムの構築を目的とする．検証システムのための推論系として，先行研究で提案した余論理プログラムに対するプログラム推論手法を用いる．また，検証対象である仕様式を導出する仕様発見系としては，昨年度に検討した仕様発見アルゴリズムをもとにして，本年度は，その改善・改良を図る．それに加えて，プログラムに誤りがある場合に，そのバグの位置特定のためのバグ発見系の設計とその実装を行った．
バグ発見系は，プログラム中にバグがある場合に，その位置特定を行う．そのために，プログラム実行時の通過行の情報からなるログと，その実行の成功/失敗を示すラベルの組からなるトレース・データを入力とする． 本研究では，形式概念分析の方法を用いて，バグの位置を特定するための相関ルールを導出するアルゴリズムの設計を行った．特に，関連性の概念を利用することによって，相関ルールの探索空間を縮小させるための枝刈り法を導入し，その効果を実験的に検証した．
バグ発見系のもう一つの方法として，ニューラルネットワークを用いた手法についても検討した．ニューラルネットワークを使うバグの位置特定法の先行研究としては，TFIDF-FLなどいくつか提案されている．本研究では，その方法にプログラム中の行について特徴選択法を利用して，バグ発見に重要性が高いと想定される行を抽出することによる精度の向上を図った．また，特徴選択法をテキスト文書の分類に応用可能性について検討し，実験的な検証を行った．
本年度までの研究結果から，ソフトウェアの正当性の検証という課題に向けて，プログラムの実行例から仕様式を導出する仕様発見系とバグ発見系のための方法論の知見が得られた．これは，プログラム推論とパターン発見技術を用いたシステムの検証方法の構築の基盤となる点で意義がある．
|
