| 研究課題/領域番号 |
23500041
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2014-03-31
|
| キーワード | モデル検査 / 活性 / 公平性 / Maude |
|---|
| 研究概要 |
活性のモデル検査では，公平性を仮定しなければならないことが多い．このため，モデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる．公平性を表わす論理式の大きさは，状態遷移数に依存するため，検査対象のシステムが複雑になればなるほど大きくなり，モデル検査の効率に大きく影響する．本研究では，"公平性 ⇒ 準公平性"を満たし，公平性より小さな論理式である準公平性を探し，"準公平性 ⇒ 活性"をモデル検査することで効率化を図ることを目指している．本手法を，分散相互排除プロトコルが無排斥性（際どい領域に入りたいプロセスは必ずそこに入ることができること）を満たすことを確認するモデル検査に適用した．実験は，モデル検査機能を有する代数仕様言語Maudeで行った．"公平性 ⇒ 無排斥性"のモデル検査は数時間経過しても終了しなかったのに対し，"公平性 ⇒ 準公平性"ならびに"準公平性 ⇒ 無排斥性"のモデル検査は数分で終了した．この実験により本手法の有効性を確認できた。活性のモデル検査に関する文献調査により，公平性を満たす実行に対してのみモデル検査を行うことのできるモデル検査法が提案されていることがわかった．さらに、そのためのツールの開発も行われていることもわかった．Maude LTLモデル検査器の拡張であるMaude LTLRモデル検査器はそのようなツールの一つである．次年度以降，Maude LTLRモデル検査器を詳細に調査し，本研究での提案方法との比較を行う予定である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究の目的は以下のとおりである：モデル検査の効率は状態機械と(性質を記述した)論理式の大きさに大きく依存する。前者による非効率化(状態爆発問題)は、状態機械の抽象化により解決の兆しが見え始めている。しかし、後者による非効率化はあまり注目されていない。性質を安全性に限れば簡潔な論理式で表現可能であり、安全性は活性より基本的かつ重要と考えられているからである。しかし、活性を考慮すると、後者による非効率化は無視できなくなる。理由は公平性を論理式の一部に埋め込む必要があるからである。本研究課題ではこの問題の解決方法を提案する。提案手法を非自明な例題（分散相互排除プロトコルの無排斥性のモデル検査）に適用することで有効性を確認できた．このことにより本研究課題は順調に進展していること評価できると判断する．一方，活性のモデル検査に関する文献調査により，公平性を満たす実行に対してのみモデル検査を行うことのできるモデル検査法が提案され，そのためのツールが開発されていることもわかった．このようなツールと本研究における提案手法との比較は今後の課題である．次年度以降，このようなツール，特にMaude LTLRモデル検査器を中心に，比較を行い，提案手法の利点・欠点を明らかにする予定である．
|
| 今後の研究の推進方策 |
主に以下のことを行う予定である：(1) 公平性により含意され簡潔な論理式で記述可能な仮定の系統的あるいは自動的な導出法の考案：今年度行った実験（分散相互排除プロトコルの無排斥性のモデル検査）をもとに，"公平性 ⇒ 準公平性"を満たし，公平性より小さな論理式である準公平性を，系統的あるいは自動的に導出する方法を考案する．(2) 公平性を満たす実行に対してのみモデル検査を行うことのできるモデル検査法・モデル検査器の調査：Maude LTLRモデル検査器を中心に調査を行い，本研究の提案手法の利点・欠点を明らかにする．
|
| 次年度の研究費の使用計画 |
調査・研究旅費：モデル検査の最先端の研究動向を調査するには，モデル検査に関する最先端の研究成果について発表される国際会議(CAVやETAPS等)への参加は不可欠である．このような国際会議参加のための外国旅費に使用する予定である．また，意見交換のために国内ならびに外国旅費を使用する予定である．実験用パソコン：パソコンの性能は日進月歩で向上している．モデル検査の実験には高性能のパソコンを必要とする．このため、実験用パソコンの購入費として使用する予定である．消耗品費：実験データ等のバックアップ用のハードディスク，論文作成や発表資料作成のためのパソコンソフトウェアは研究遂行上不可欠である．また，論文誌に論文を掲載する場合，別刷り費が必要となる．このような目的のために使用する予定である．研究員雇用：調査研究により、公平性を満たす実行に対してのみモデル検査を行うことのできるモデル検査法が提案され，そのためのツールが開発されていることが明らかになった。これらは本研究課題と密接な関係があるため、更なる調査を必要とする。この調査のため、研究員の雇用を予定している。当初予定では研究員の雇用は計画しておらず、単年度の予算では雇用することが難しいため、H23年度の予算を翌年度に持ち越すことにした。H23年度の未使用額を研究員雇用に充てる予定である。H23年度の予算に未使用額が生じたのは、実験用パソコンの購入ならびに国際会議参加を見送ったためである。
|
