2016 Fiscal Year Research-status Report
無限構造を扱うプログラム推論を用いたソフトウェア検証方法の確立
| Project/Area Number |
15K00305
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，リアクティブ・システムなどのソフトウェアの正当性を検証する検証システムを構築するための方法論を確立することにある．そのために，計算論理に基づく形式的手法である論理プログラムに対するプログラム推論技術を採用している．
本研究では，リアクティブ・システムの記述に必要な無限構造を自然に扱える余論理(co-logic)プログラムとそのプログラム推論方法を基礎としている． 研究計画1年目では，ホーンμ-計算 (Horn μ-calculus)に着目し，その性質と応用可能性を調べた．余論理プログラムを拡張してその双対プログラムを考えて，その定式化をホーンμ-計算を用いて行った．また，主要なプログラムの意味論である有礎モデルや解集合について，ホーンμ-プログラムとの関係を示した．
研究計画２年目は，これらの結果を拡張し理論的解析を行った．ホーンμ-計算が余論理プログラムの真の拡張であり余論理プログラムに課される構文的制約を必要としない枠組みであることを示した．さらにそのためのプログラム推論の規則や拡張された双対プログラムを示した．
また，プログラム検証に必要になる仕様をログから自動的に導出する仕様発見については，プログラム実行のログを格納した系列データから再現(recurrent)ルールというパターンを発見する方法による仕様発見アルゴリズムについて検討を進めた．また，その基礎となる時間等の量的制約を表現する区間パターン発見アルゴリズムの設計と効率的な実現に基本検討を行った．
これまでの研究結果から，モデル検査などのシステム検証問題に対して余論理プログラムやホーンμ-計算を用いた推論方法が有効であるという知見が得られた．このことは，プログラム推論に基づくシステムの検証方法の開発に貢献する意義がある．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では計算論理技術に基づくシステム検証の方法論を構築するために，プログラム推論技術の理論的枠組みの構築と，検証システム実現のための余論理プログラミング技術の蓄積，そしてその有効性・妥当性の実証という研究サイクルを遂行するための課題を設定して行っている．研究計画２年目は，特に以下のようなタスクについて研究を行った．
プログラム推論の理論的枠組みについては，これまでの枠組みを拡張しより広い対象を扱うためにホーンμ-計算について，その性質と応用可能性を引き続き検討した． ホーンμ-計算にプログラム推論の規則や拡張された双対プログラムを定式化した．これにより，余論理プログラムにもとづく推論方式の適用可能性をより広げることができた．この点ではほぼ予定通り順調に進行している．
また，プログラム検証に必要な仕様をログから自動的に導出する仕様発見については，ログ系列データから再現ルール発見アルゴリズムの検討を続け，その実現に着手した．それを改良して効率的な実現についての見通しを得て，概ね予定通りに進行している．
変換による検証のアプローチの有効性を確認するための実験については，再現ルールから発見される時制論理式を対象にして，それを検証するためのシステム実現に向けて，余論理プログラミング技術に基づく方法の有効性を確認した． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| Strategy for Future Research Activity |
これまでに設計してきた方式と実験の検討結果に基づいて，それを最終的なシステムに統合するとともに，提案方式の拡張と改良を引き続き行う．具体的には，以下のようなタスクについて研究を進める．
プログラム推論の理論的枠組みについては，余論理プログラムやホーンμ-プログラムの表現能力を向上させるため，制約等の導入等を中心にして引き続き検討をすすめる．これにより検証対象のシステムを記述するための表現能力が向上し実応用システムを自然に表現することを目指す．
また，検証するプログラムの性質（仕様）をプログラムの実行からマイニングにより導出する仕様発見については，前年度に行った検討結果から，再現ルールのマイニングについて見通しがついている．それから時制論理式等の導出とその実装方法について検討する．提案方式のシステム実装については，余論理プログラムの処理系のソフトウェア資産やパターン発見のプログラムを可能な限り再利用できる方向で実装を進める．対象とするリアクティブ・システムのクラスと，その仕様記述の論理式の表現能力の関係について，その妥当性を検討する．
プログラム推論技術を用いた検証システムの実現については，時制論理式に対するモデル検査を行う余論理プログラムの証明手続きを利用したシステムについて，ベンチマークとして使われている例題を中心にして動作確認し本方式の有効性を評価する．特に，モデル検査等の検証方式と比較検討して，本方式の有効性を評価する．
以上のプロセスを通じて，プログラム推論技術を用いたリアクティブ・システム検証の新しい枠組みの確立を目指す．
|
| Causes of Carryover |
当該年度に、提案アルゴリズムの実装方式の動特性分析を行うとともに，様々な例題による実験結果などを学会発表する予定であったが，その分析結果からより良いアルゴリズムによる実装方式の可能性が予想されたため，計画を変更し改良された方式の実装と解析を行うこととしたため，未使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
改良された提案方式の解析を引き続き進め，その結果の学会発表を次年度に行うこととし、未使用額は成果発表のための経費に充てる計画である。
|
Research Products
(4 results)
