2015 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)に着目した．述語の否定を計算する双対(dual)プログラムを導出する否定除去技法を利用し，ホーンμ-計算の枠組みで双対プログラムを定式化した．そして，従来の主要なプログラムの意味論である有礎モデル(well-founded model)や解集合(answer set)について，ホーンμ-プログラムとの関係を示した．特に，有礎モデルの双対プログラムの不動点による特徴付けを示した．
また，プログラムの検証では，プログラムが与えられた仕様を満たしているかを調べることが前提であるが，その仕様を与えること自体が難しい課題である．この仕様を自動的に導出するためのパターン発見アルゴリズムについて検討した．その基礎となるパターン発見アルゴリズムの設計と効率的な実現についての見通しを得ることができた．
これまでの結果から，モデル検査などのシステム検証問題に対して余論理プログラムを用いた推論方法によるアプローチが有効で効率的な実装につながることが分かった．これにより，プログラム推論に基づくシステムの検証方法の開発に貢献する点で意義がある．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では計算論理技術に基づくシステム検証の方法論を構築するために，プログラム推論技術の理論的枠組みの構築と，検証システム実現のための余論理プログラミング技術の蓄積，そしてその有効性・妥当性の実証という研究サイクルを遂行するための課題を設定している．その中で，研究計画の1年目は特に以下のようなタスクについて研究を行った．
プログラム推論の理論的基盤については，研究提案者は先行研究で余論理プログラムに対するプログラム変換の枠組みを提案した．この枠組みを拡張しより広い対象を扱うために，ホーンμ-計算に着目し，ホーンμ-計算の枠組みで双対プログラムを定式化した．これにより，より広いクラスの余論理プログラムにも適用可能になった．この点ではほぼ予定通り順調に進行している．
また，検証システムにおいて必要となるプログラムの仕様について，その仕様を自動的に導出するパターン発見アルゴリズムの検討に着手した．その基礎となるパターン発見アルゴリズムの設計と効率的な実現についての見通しを得ることができ，概ね予定通りに進行している．
更に，変換による検証のアプローチの有効性を確認するための実験については，検証システム実現のための余論理プログラミング技術について，時制論理式などいくつかの例題を通してその有効性を確認した． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| Strategy for Future Research Activity |
当初の研究計画に従って，研究計画２年目以降は前年度に設計した方式と実験の検討結果に基づき，引き続き推論方式の拡張と改良に向け，以下のようなタスクを設定して進める．
プログラム推論の理論的基盤については，制約の導入を検討する．これにより検証対象のシステムの記述能力が向上し実応用システムの自然な表現が可能になる．このために，前年度のホーンμ-プログラムの推論規則を拡張して制約を導入した場合の正当性について検討する．また，対象とするリアクティブ・システムのクラスと，その仕様記述の論理式の表現能力の関係について，その妥当性を検討する．
プログラム検証システムに必要となる仕様式については，前年度に行った検討結果から，時制論理式等の仕様マイニングについて見通しがついた．それに基づいて，パターン発見アルゴリズムを利用したシステムの実現方法について検討する．提案方式のシステム実装については，その妥当性を確認後に開始する．その際には，余論理プログラムの処理系のソフトウェア資産を可能な限り再利用する方向で実装を進める方針である．今年度は提案アルゴリズムを実装し、簡便なインタフェースとの連携を確認する．
さらに，提案方法の評価と理論的考察については，引き続きベンチマークとして使われている例題から選択して動作確認する．特に，モデル検査等の検証方式と比較検討して，本方式の有効性を評価する．
以上の過程を通じて，プログラム推論技術を用いたリアクティブ・システム検証の新しい枠組みの確立を目指す．
|
| Causes of Carryover |
平成27年度に、提案アルゴリズムの実装方式の動特性分析を行うとともに，様々な例題による実験結果を学会発表する予定であったが，その分析結果からより一般的な実装方式の可能性が予想されたため、計画を変更し，一般的に適用可能な方式の実装と解析を行うこととしたため、未使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
提案方式の解析と学会発表を次年度に行うこととし、未使用額は成果発表のための経費に充てる計画である。
|
