2010 Fiscal Year Annual Research Report
形式手法のための論理の構築と、一階拡張が満たす性質に関する研究
| Project/Area Number |
22500021
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
岡本 圭史 独立行政法人産業技術総合研究所, 関西産学官連携センター, 招聘研究員 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
北村 崇師 独立行政法人産業技術総合研究所, 関西産学官連携センター, 産総研特別研究員 (70530484)
|
|---|
| Keywords | 形式手法 / 論理 / 命題様相μ計算 / 一階様相μ計算 / モデル / (論理の)表現力 |
|---|
| Research Abstract |
1)検証のための新しい論理の構築
要求仕様の参照モデルとして有名なJacksonモデルを基にした(要求管理のための)形式手法のためのモデル及び論理を構築し、その成果を国際会議などで発表した。本参照モデルでは、要求とシステム仕様の関係に、ドメイン知識の概念を取り入れ、その三つ組みで要求とシステム仕様の関係を定式化するものである。また、本手法では、形式的議論、及び計算機支援実現のための仕組みとして(形式)論理を用いた。具体的には、要求変更が起きた際の「仕様の最弱条件」という概念を定義し、それを計算機により自動的に導くことにより、要求変更のインパクトを測り、要求変更の管理を支援する技法を開発した。さらに、飛行機の着陸時制御システムの要求管理に本手法を適用し、その有効性を示した。
2)一階様相μ計算の理論的性質を明らかにすること
2.A)モデル理論:"一般モデルで充足可能な命題様相μ計算の論理式は、標準モデルでも充足可能か?"という問題を解決するために、与えられた一般モデルから、それと論理式の真偽に関して等価な標準モデルを構築する研究を行い、その成果を国内会議にて発表した。現時点では、この主張の完全な証明には至っていないが、有限な一般モデルに対しては、それと等価な標準モデルが構築できることを示した。
2.B)表現力:CTL^*の表現力が命題様相μ計算の表現力よりも真に弱いことを示す証明を拡張し、それぞれの一階拡張である、FOCTL^*の表現力が一階様相μ計算の表現力よりも真に弱いことを示し、その成果を国内誌にて発表した。従来のCTL^*及び命題様相μ計算の表現力比較の証明は論理式に関する帰納法を用いている。そこで、一階拡張における証明へ拡張するために、一階拡張に特有の論理式に対応した帰納法による証明を行った。
|
