| 研究課題/領域番号 |
18K11432
|
|---|
| 研究機関 | 名古屋工業大学 |
|---|
研究代表者 |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | プログラム推論 / パターンマイニング / ルール発見 |
|---|
| 研究実績の概要 |
本研究では，リアクティブ・システムなどのソフトウェアを対象に，その正当性を検証する検証システムの構築を目的としている．検証システムで用いる推論系は，先行研究で提案した余論理プログラムに対するプログラム推論手法を基礎とする．本年度は，プログラム検証のために対象システムの仕様式を導出する仕様発見系と，プログラムに誤りがある場合に，プログラム内のバグの位置を特定するバグ発見系の設計を行った．
仕様発見系では，プログラムの実行ログを格納した系列データ集合から再現ルールというパターンを発見するパターン発見アルゴリズムについて引き続き検討を進めた．特に，先行研究において最良の方法に着目し，その計算効率を改善したアルゴリズムを設計し，実験により有効性を確認した．また，再現ルール発見アルゴリズムの並列化についても引き続き検討を進め，ルールを構成するパターンの探索処理を並列化する処理方式を実験した．
バグ発見系では，プログラムの実行ログを格納した系列データ (トレース)とその実行が成功か失敗かを示すラベルの集合を入力として，それからバグの位置を特定する相関ルールを導出する方法について検討した．そのために，形式概念分析(FCA)における関連性の概念を利用して，失敗に関連するプログラムの位置を特徴として選択する方法の予備的実験を行った．また，特徴選択法として自然言語処理で用いられるtf-idf値を利用した方法の有効性についても検討した．さらに，その特徴選択方法を利用してテキスト文書の分類への応用についても検討した．
本年度までの研究結果から，ソフトウェアの正当性の検証問題に対し，プログラムの実行例から仕様式を導出する仕様発見系とバグ発見系を構築する方法論の知見が得られた．これは，プログラム推論とパターン発見技術に基づくシステムの検証方法の構築に利用できる点で意義がある．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究では，システム検証のための計算論理に基づく推論系に，その入力となる仕様式を導出する仕様発見系を融合した検証システムの構築を目的としている．本年度は，プログラムの検証の入力として用いる対象システムの仕様式を導出する仕様発見系と，プログラムに誤りがある場合にそのバグの位置を特定するバグ発見系を中心として，以下の研究課題について研究を行った．
仕様発見系については，プログラムの実行ログを格納した系列データ集合から仕様を表現する再現ルールというパターンを発見する仕様マイニング・アルゴリズムについて，先行研究を改良したアルゴリズムを設計し，その有効性が確認できた．また，再現ルール発見アルゴリズムの並列化についても良好な実験結果が得られた．このように，アルゴリズムと実装の両方の観点からほぼ予定通り順調に進行している．
また，バグ発見系については，プログラムの実行ログ(トレース)を格納した系列データ集合からバグの位置特定のための相関ルールを導出するアルゴリズムについて，形式概念分析における関連性の概念を利用したアルゴリズムを設計し，小規模の例題データについてその有効性が確認できた．また，特徴選択法として自然言語処理で用いられるtf-idf値を利用したアプローチについても検討し同様に有効性を示すことができた．以上から，概ね予定通りに進行している．
システム検証のために検証対象の仕様式を表すルールをマイニングする仕様発見系を備えた検証システムの有効性を確認するために，本年度に行った仕様発見系とバグ発見系については，小規模のテストデータについてはその基礎的な有効性が確認できた． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| 今後の研究の推進方策 |
今年度までに検討してきた方式とその実験結果から得られた知見に基づいて，システム検証のため推論系と検証対象の仕様式を導出する仕様発見系を融合した検証システムの構築に向けて，提案方式の改良と妥当性の検証を引き続き行う．具体的には，以下の項目について研究を進める．
仕様発見系では，仕様を表現する再現ルールのマイニング・アルゴリズムについて，本年度までに提案した複数のアプローチの評価実験を引き続き行い，比較検討する．この過程で，再現ルールマイニングに対して，計算コストの観点から最も良いアルゴリズムと実装方式の確立を目指す．
また，バグ発見系では，プログラム中のバグの位置を特定する方法として，形式概念分析と相関ルール・マイニングにおける手法を中心にして引き続き検討する．バグの位置特定に利用できる相関ルールを導出するために，関連性の概念が有効に使えることがこれまでの検討から分かってきている．それをさらに深化させて効率の良いアルゴリズムの設計につなげ，バグの位置特定法の実現を図る．
検証のため推論系と仕様発見系を有機的に結合した検証システムを構築するために，仕様発見の結果得られる再現ルールを時制論理式に変換する過程，その時制論理式を推論系で検証する過程，さらにプログラムに誤りがある場合にバグ発見系によるバグの位置を特定する過程について，モデル検査などでベンチマークとして使われている例題を中心にして動作確認し本方式の有効性を評価する．バグ発見系ではより大きなテストケースについて実験結果を蓄積して検討を続ける．
|
