2013 Fiscal Year Research-status Report
無限項を扱うプログラム変換を用いたソフトウェア検証方法の研究
| Project/Area Number |
24500171
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Keywords | 計算論理 / プログラム変換 / システム検証 |
|---|
| Research Abstract |
本研究では，リアクティブ・システムやソフトウェアの正当性を形式的に検証可能な検証システムのための方法論を構築することを目的とする．そのために，計算論理に基づく形式的手法である論理プログラムに対するプログラム変換技術を中核に用いる検証アプローチを採用した．
研究提案者は，これまでに余論理(co-logic)プログラムに対するプログラム推論の枠組みを提案した．これにより，リアクティブ・システムの記述に必要な無限項を扱える余論理プログラムの特長を利用して，プログラム変換を用いた検証が可能であることを示した．
研究計画２年目は，余論理プログラムをモデル検査問題に適用するための方法を検討した．CTLという時間論理式に対する分岐時間モデル検査を扱うために，余論理プログラムが持つ「層状化制限」制約を緩和して「局所層状化制限」という条件を与え，その意味論について考察した．その結果，CTL式を扱う弱交替オートマタを余論理プログラムで自然に表現でき，Kupfermanらのオートマタ理論に基づく最も効率のよい方法と同等な計算を行うことを示した．
更に，層状化制限を満たさない余論理プログラムを扱うために，Charatonikらのホーンμ-計算が利用できることに注目して，余論理プログラムの推論方法を拡張することによりホーンμ-計算のための証明法が得られることを示した．
これまでの研究から，余論理プログラムを用いた推論方法がモデル検査などのシステム検証に対して適用できて，その結果，従来のオートマタ理論によるモデル検査方法を自然に表現可能で，それに対して計算論理に基づく推論技術を適用することにより効率的な実装につながる見通しを得ることができた．この結果は，プログラム推論に基づくシステムの検証方法の開発につながると同時に，システム検証のための方法論を構築する基盤技術となることが期待される．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的である計算論理技術に基づくシステム検証の方法論を構築するために，研究計画では，基盤となるプログラム変換の理論的枠組みを構築すること，システム検証に利用するための余論理プログラムによる表現方法と推論技術を確立すること，そしてその有効性・妥当性をシステム検証において確認するという課題を設定した．研究計画２年目は，特に以下のようなタスクについて研究を行った．
プログラム変換の理論的枠組みについては，余論理プログラムに対するプログラム変換規則やその性質に関する知見をこれまでに蓄積してきている．システムの仕様に対するモデル検査問題を扱うためには，余論理プログラムを用いた推論方法を確立する必要があった．このために，否定を含む余論理プログラムのクラスを拡張して，CTL式を扱う弱交替オートマタを表現できるような定式化を与えた．この結果，余論理プログラムの推論により，オートマタ理論に基づく最良の方法と同等な検証を実現することを示した．この点ではほぼ予定通り順調に進行している．
また，リアクティブ・システムの仕様や性質を記述する論理式とその余論理プログラムでの表現方式の検討も研究計画２年目に行う計画であった．システムの性質を記述する方法として，他の時制論理式(LTLなど)についての検討も行った．その結果，オートマタ理論に基づくモデル検査との関係が明確になり本方式の妥当性を確認できて，概ね予定通りに進行している．
更に，計算論理技術に基づくシステム検証アプローチの有効性を確認するための実験については，リアクティブ・システムの安全性や活性(liveness)について，従来ベンチマークで用いられている例題を用いて提案方式の有効性の確認を続けている． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| Strategy for Future Research Activity |
当初の研究計画に従って，研究計画３年目はこれまでに設計してきた方式と実験の検討結果に基づいて，提案方式の拡張と改良を引き続き行うとともに，得られた結果を最終的なシステムへ統合する． 具体的には，以下のようなタスクについて研究を進める．
プログラム変換の理論的基盤については，余論理プログラムの表現能力を向上させるため，制約の導入を中心にして引き続き検討をすすめる． 同時に，制約付き余論理プログラムに対するプログラム推論方式について定式化する．また，制約付き余論理プログラムを用いた場合，検証の対象とするリアクティブ・システムやその仕様記述の論理式のクラスとの関係について，妥当性を検討する．
プログラム推論技術を用いた検証システムの実現については，時制論理のCTL等についての前年度までに行った検討から，従来のオートマタ理論に基づくモデル検査の研究結果との関係について知見を蓄積した．それに基づいて，余論理プログラムの証明手続きを利用したシステムの実現方法を検討する．その際には，Guptaらによる余論理プログラムの処理系(co-SLD)のソフトウェアを利用できる見通しが立ったので，それを活用して実装を進める．これまでの検討結果をアルゴリズムに取り入れて実装し、インタフェースと連携させて動作を確認する．
さらに，提案方法の評価と理論的考察のために，引き続きベンチマークとして使われている例題を中心にして動作確認し評価を行う．特に，モデル検査等の検証方式と比較検討して，本方式の有効性を評価する．以上のプロセスを通じて，計算論理に基づくプログラム推論技術を用いたリアクティブ・システム検証の新しい枠組みの確立を目指す．
|
| Expenditure Plans for the Next FY Research Funding |
実験用ソフトウェア（言語処理系）の購入等を予定していたが，オープンソースのソフトウェアを利用して開発できる見通しがついたので，購入を見送ったため．
研究費は，システム構築・実験に掛かる経費，方式設計のための資料などの経費，成果発表のための経費に区分けできる．システム構築と実験に関する経費では，提案方式を検証システムとして実装し完成させるため，開発用と検証システム実験用の計算機が必要になる．実験用計算機1台と最終システムの構築用計算機1台を購入する計画である．
方式設計のための経費では，関連研究の調査等のため国際会議等の論文書籍費を１０冊程度分計上した．方式設計の実施は開発用計算機を用いるため特に計上していない．成果発表のための経費としては，成果をLOPSTRシンポジウムなどの論理プログラムの変換や検証に関連する国際会議に発表するため，旅費を計上している．これらの会議は情報交換の場としても重要である．また国内での成果発表として関連する学会の研究会に２回ほどの出席を予定し，代表者と大学院生の旅費と参加費を計上している．
|
Research Products
(3 results)
