2012 Fiscal Year Research-status Report
無限項を扱うプログラム変換を用いたソフトウェア検証方法の研究
| Project/Area Number |
24500171
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 計算論理 / プログラム変換 / システム検証 |
|---|
| Research Abstract |
本研究では，リアクティブ・システムの設計やソフトウェアの正当性を形式的に検証可能な検証システムのための方法論を構築することを目的とする．そのために，本研究では計算論理に基づく形式的手法を採用し，特に計算論理に基づく技術として論理プログラムに対するプログラム変換による検証技術を中核に用いるアプローチをとる．
研究提案者は，先行研究で余論理(co-logic)プログラムに対するプログラム変換の枠組みを提案した．余論理プログラムでは，リアクティブ・システムを記述するために無限項を自然に扱える特長を持つことに着目し，確定余プログラムに対するプログラム変換の枠組みを示した．
研究計画1年目は，この枠組みを拡張し，否定を含むプログラムにも適用可能な変換規則を与えた．この方法は，否定除去という従来のプログラム変換技法を利用したものであるが，余論理プログラムではより弱い条件の下で適用可能であることを示した．
また，提案した否定除去を用いた変換規則と，従来の負リテラルに対する展開規則との比較を行った．その結果，提案方法を用いた変換により，従来の枠組みでは扱えないような変換が可能になることを示した． 更に，この拡張したプログラム変換規則により，プログラム変換技術を用いたリアクティブ･システムの検証方法がより広いクラスに対して適用できることを例により示した．この結果，従来方法と比較して，より単純で従って自動化しやすく，しかも直観的に分かりやすい方法で検証が実現できる見通しを得ることができた．
これまでの結果から，プログラム変換を用いたシステム検証方法をより広いクラスに対して適用するための知見を得た．これはプログラム推論に基づくシステムの検証方法の開発に貢献するだけでなく，ソフトウェア検証のためのより強力な方法論の構築に有用な基礎となることが期待される．
|
| 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年目は特に以下のようなタスクについて研究を行った．
プログラム変換の理論的基盤については，研究提案者は先行研究で余論理プログラムに対するプログラム変換の枠組みを提案した．この枠組みを拡張し，否定を含むような余論理プログラムの適用できるように変換規則を定式化する必要があった．このために，否定除去というプログラム変換技法を利用して，余論理プログラムのための適用条件を示した．これにより，否定を含むより広いクラスのプログラムにも適用可能な枠組みを与えた．この点ではほぼ予定通り順調に進行している．
また，リアクティブ・システムの仕様や性質を記述する論理式とその余論理プログラムでの表現方式の検討も研究計画1年目に行う計画であった．システムの性質の記述方法として，時制論理のCTL等についての検討も行った．その結果，オートマトン理論に基づくモデル検査との関連も調べることにより本方式の妥当性を確認できて，概ね予定通りに進行している．
更に，変換による検証のアプローチの有効性を確認するための実験については，リアクティブ・システムの活性(liveness)の検証やω-正規言語の包含問題等のいくつかの例題について，変換による検証アプローチの有効性を確認した． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| Strategy for Future Research Activity |
当初の研究計画に従って，研究計画２年目以降は前年度に設計した方式と実験の検討結果に基づいて，引き続き変換方式の拡張と改良に向け，以下のようなタスクを設定して進める．
プログラム変換の理論的基盤については，制約の導入を検討する．これにより検証対象のシステムの記述能力が向上し実応用システムの自然な表現が可能になる．このために，前年度の否定を含む余論理プログラムの変換規則を拡張して制約を導入した場合の正当性について検討する．また，対象とするリアクティブ・システムのクラスと，その仕様記述の論理式の表現能力の関係について，その妥当性を検討する．
変換に基づくプログラム検証システムの実現については，時制論理のCTL等についての前年度に行った検討結果に基づき，従来のオートマトン理論に基づくモデル検査との関連やその結果の利用について見通しがついた．それに基づいて，余論理プログラムの処理系を利用したシステムの実現方法について検討する．提案方式のシステム実装については，変換戦略の正しさを確認後に開始する．その際には，Guptaらによる余論理プログラムの処理系のソフトウェア資産を可能な限り再利用できる方向で実装を進める方針である．今年度は提案アルゴリズムを実装し、簡便なインタフェースとの連携を確認する．
さらに，提案方法の評価と理論的考察については，引き続きベンチマークとして使われている例題の中で，無限状態システムを対象とするものを使用し動作確認する．特に，モデル検査等の検証方式と比較検討して，本方式の有効性を評価する．
以上の過程を通じて，プログラム変換技術を用いた無限状態リアクティブ・システム検証の新しい枠組みの確立を目指す．
|
| Expenditure Plans for the Next FY Research Funding |
本研究課題で計画している研究費は，システム構築・実験に掛かる経費，プログラム変換方式設計のための資料などの経費，成果発表のための経費に区分けできる．
システム構築と実験に関する経費については，本研究で提案するプログラム変換方式を検証システムとして実装し完成させるため，開発用と検証システム実験用の計算機が必要になる．このうち，実験用計算機1台を2年目に，最終システムの構築用計算機1台を３年目に購入する計画である．また開発・実験用のソフトウェアを購入し，計上した計算機に導入して検証システムの構築と実験に用いる. 実装用のProlog処理系はSICStus社開発のSICStus Prologを用いるのでその購入経費を計上している．加えて，実験を大学院生指導のもとに進めるため，実験の補助として大学院生の研究手伝いを計上して実験を効率的に進める．
プログラム変換方式設計のための経費としては，変換方式及び変換戦略設計の関連研究の調査を含めて進めるため，関連する国際会議等の論文書籍費を各年度１０冊程度分計上した．方式設計の実施等は開発用の計算機を用いるため特に計上していない．
成果発表のための経費としては，各年度の成果をLOPSTRシンポジウムなどの論理プログラムの変換や検証に関連する国際会議に発表するため，旅費を計上している．これらの会議は情報交換の場としても重要である．また国内での成果発表として関連する学会の研究会に各年度２回ほどの出席を予定し，代表者と大学院生の旅費と参加費を計上している．
|
