2008 Fiscal Year Annual Research Report
| Project/Area Number |
20700004
|
|---|
| Research Institution | Tottori University of Environmental Studies |
|---|
Principal Investigator |
西澤 弘毅 Tottori University of Environmental Studies, 環境情報学部, 講師 (60455433)
|
|---|
| Keywords | 情報基礎 / システム検証 / モデル検査 / 抽象化 / 多値論理 |
|---|
| Research Abstract |
ソフトウェアやハードウェアの誤動作によって起こる社会的な問題は後を絶たない。そこで、これらのシステムを稼働前に検証するモデル検査の技術が広まりつつある。本研究では、モデル検査で不可欠な「抽象化」と呼ばれる効率化情報を再利用または修正するための理論を与える。ある性質の検証には有効であった抽象化も、別の性質の検証にはまったく役に立たない場合があるため、現在のシステム検証の現場では、抽象化のコストが高い。本研究によって抽象化の再利用が進めば、抽象化のコストを下げることができる。本研究では特にさまざまな多値論理の間で抽象化を再利用するための理論を与える。抽象化の正しさは多値論理と模倣の理論に基づいて数学的に保証する。
平成20年度の目標は、さまざまな多値論理やさまざまな抽象化を含む一般的な論理を提案し、その上で模倣の理論に基づいて抽象化の正しさを数学的に保証することであった。研究の結果、4つの多値論理(Frame、 DeMorgan Frame、Bilattice、 MixedTS)を例に含む一般性の高い不動点論理を提案することができた。また、それらにおける模倣の健全性を証明することができた。これによりさまざまな多値論理やさまざまな抽象化を含む一般的な論理を提案したといえる。
平成21年度には、より具体的に以下の1, 2の目標を挙げる。この達成のためには, 平成20年度の成果と1, 2との厳密な比較をすることが必要となる。
1. ACTLのための抽象化がLTLで再利用できるための、真偽値に対する十分条件を与える。
2. 1の十分条件を満たさない真偽値において、再利用できるための抽象化の十分条件を与える。
|
