研究課題
1)検証のための新しい論理の構築要求仕様の参照モデルとして有名なJacksonモデルを基にした(要求管理のための)形式手法のためのモデル及び論理を構築し、その成果を国際会議などで発表した。本参照モデルでは、要求とシステム仕様の関係に、ドメイン知識の概念を取り入れ、その三つ組みで要求とシステム仕様の関係を定式化するものである。また、本手法では、形式的議論、及び計算機支援実現のための仕組みとして(形式)論理を用いた。具体的には、要求変更が起きた際の「仕様の最弱条件」という概念を定義し、それを計算機により自動的に導くことにより、要求変更のインパクトを測り、要求変更の管理を支援する技法を開発した。さらに、飛行機の着陸時制御システムの要求管理に本手法を適用し、その有効性を示した。2)一階様相μ計算の理論的性質を明らかにすること2.A)モデル理論:"一般モデルで充足可能な命題様相μ計算の論理式は、標準モデルでも充足可能か?"という問題を解決するために、与えられた一般モデルから、それと論理式の真偽に関して等価な標準モデルを構築する研究を行い、その成果を国内会議にて発表した。現時点では、この主張の完全な証明には至っていないが、有限な一般モデルに対しては、それと等価な標準モデルが構築できることを示した。2.B)表現力:CTL^*の表現力が命題様相μ計算の表現力よりも真に弱いことを示す証明を拡張し、それぞれの一階拡張である、FOCTL^*の表現力が一階様相μ計算の表現力よりも真に弱いことを示し、その成果を国内誌にて発表した。従来のCTL^*及び命題様相μ計算の表現力比較の証明は論理式に関する帰納法を用いている。そこで、一階拡張における証明へ拡張するために、一階拡張に特有の論理式に対応した帰納法による証明を行った。
すべて 2010
すべて 雑誌論文 (4件) (うち査読あり 3件) 学会発表 (3件)
Proceedings of the 16th IEEE Pacific Rim International Symposium on Dependable Computing
巻: (Published electronically)
Proceedings of the IPSJ/SIGSEソフトウェアエンジニアリングシンポジウム
ページ: 149-154
Information and Media Technologies
巻: 5(1) ページ: 40-47
京都大学数理解析研究所講究録
巻: 1708 ページ: 1-14
