2012 Fiscal Year Research-status Report
| Project/Area Number |
23500041
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
|
|---|
| Keywords | モデル検査 / 活性 / 公平性 / 準公平性 / 状態機械 / 反例 / 公平性の理解 / Maude |
|---|
| Research Abstract |
システムの性質は大きく2種類に分類できる。安全性と活性である。安全性は危険な状態が絶対に起こらないこと、活性はそのうち望みのことが必ず起きること、と言い表すことができる。安全性のモデル検査には特別の仮定を必要としないが、活性のモデル検査では公平性と呼ばれる仮定を必要とする場合がある。公平性は、プロセス等の実行主体にプロセッサ資源を公平に割り当てるスケジューリングを抽象化したものとみなすことができる。公平性を仮定しないと、ある特定のプロセスにのみプロセッサが割り当てられることに起因する非現実的な反例を引き起こすこともある。
公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。公平性を表わす論理式の大きさは、システム仕様（状態機械）の大きさ、すなわち状態遷移数に依存する。公平性が大きくなるとモデル検査対象の論理式"公平性 ⇒ 活性"も大きくなり、Buchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。
本研究では、"公平性 ⇒ 準公平性"を満たし，公平性より小さな論理式である準公平性を探し，"準公平性 ⇒ 活性"をモデル検査することで公平性のもとでのモデル検査を可能とする方法を提案した。すなわち、"公平性 ⇒ 活性"の代わりに、"公平性 ⇒ 準公平性"と"準公平性 ⇒ 活性"をモデル検査することになる。
一方アルゴリズムレベルで公平性を効果的に扱う方法が提案されるとともに公平性のもとでの活性のモデル検査を効率良く行うツールが開発されていることがわかった。本研究での提案方法は、モデル検査の処理性能に関しては、これらのツールにかなわないが、活性の検証において何故公平性を必要とするのかをより良く理解するのに役立つことがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
"公平性 ⇒ 活性"の代わりに、"公平性 ⇒ 準公平性"と"準公平性 ⇒ 活性"をモデル検査することにより、前者はモデル検査不可能であるが、後者は可能であることが、Suzuki-Kasami分散相互排除プロトコル（正確にはその改訂版）が無排斥性を満たすことのモデル検査に適用することで明らかになった。
一方、アルゴリズムレベルで公平性を扱う方法が提案されるとともに、それに基づくモデル検査器が開発されていることもわかった。プロセス計算CSPのモデル検査器であるPATモデル検査器と書換仕様のモデル検査器であるMaude LTLRモデル検査器である。Maude LTLRモデル検査器の基になったMaude LTLモデル検査器は本研究で用いているモデル検査器である。モデル検査の処理速度に関しては、本研究での提案方法より、PATモデル検査器やMaude LTLRモデル検査器のほうが優れていることがわかった。
システム検証（システム仕様が性質仕様を満たすことの検証）の目的は、検証を成功させることに留まらない。何故システム仕様が性質仕様を満たすのかを理解することをとおし、対象となるシステムの理解を深めることは検証の成功以上に大切なことである。これにはどのような仮定のもとで検証を行ったのかの理解も含む。すなわち、活性の検証（モデル検査）の場合、何故公平性を仮定する必要があるのかを理解することも重要なことである。本提案方法では、準公平性ならびにそれを導き出す過程をとおし何故公平性を仮定する必要があるのかを理解できることが、Suzuki-Kasami分散相互排除プロトコルへの適用実験によりわかった。本提案方法はこの点においてPATモデル検査器やMaudeLTLRモデル検査器より優れているといえる。
|
| Strategy for Future Research Activity |
１．本提案手法の利点は、既存のLTLモデル検査アルゴリズムを変更する必要がないこと（すなわち既存のLTLモデル検査器を使えること）、公平性のもとでの活性のモデル検査を可能とすること、それに何故公平性を必要とするのかを準公平性およびそれを導く過程をおとしてよりよく理解できるようになることである。このことが評価を受け2013年7月に京都で開催される第37回計算機ソフトウェアと応用に関する国際会議（37th COMPSAC）にフルペーパとして採用された。今後は、準公平性およびそれを導く過程をおとして公平性の必要性を理解することに焦点を当てて研究を進めていく予定である。
２．本研究で用いているMaudeの探索機能を用いて分散スナップショットアルゴリズムが次の性質を満たすことのモデル検査を行った。s1をスナップショットを開始する状態、s*を取得したスナップショット、s2をスナップショットを取得し終えた状態とする。モデル検査した性質は、s*は必ずs1から到達可能であり、s2はs*から必ず到達可能である、というものである。分散スナップしょっとアルゴリズムの満たすべき性質として、スナップショットを開始したら必ず取得し終える、という活性もある。このスナップショットの停止性について、本提案手法を用いてモデル検査することも予定する。
|
| Expenditure Plans for the Next FY Research Funding |
調査・研究旅費：COMPSAC等での成果発表のための国内外の旅費を必要とする。
実験用パソコン：パソコンの性能は日進月歩で向上している．モデル検査の実験には高性能のパソコンを必要とする．このため、実験用パソコンの購入費として使用する予定である．
消耗品費：実験データ等のバックアップ用のハードディスク，論文作成や発表資料作成のためのパソコンソフトウェアは研究遂行上不可欠である．また，論文誌に論文を掲載する場合，別刷り費が必要となる．このような目的のために使用する予定である．
研究員雇用：今後の推進方策で記述したことを遂行するため研究員の雇用を予定する。当初予定では研究員の雇用は計画しておらず、単年度の予算では雇用することが難しいため、H24年度の予算を翌年度に持ち越すことにした。H24年度の未使用額を研究員雇用に充てる予定である。H24年度の予算に未使用額が生じたのは、実験用パソコンの購入を見送ったためである。
|
