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