モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

点击翻译按钮获取中文摘要

論理的手法による実時間システム検証の理論を情報学的観点から完成させることを本研究課題の目的としている。又この理論の実装に関して現れる情報学的問題を研究してきた。次のような特徴を持つ論理的検証系の理論を構築してきた。その第1は、実時間システム全体の設計に伴う、体系的で論理的な形式仕様の方法論および、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論の開発である。これまでに得られた我々の論理的検証系に対するPSPACE決定性定理を応用してこの方法論を開発してきた。その第2は、ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性の検討である。エージェントの数が増加したり、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールの方法論の開発を進めた。その第3は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析するツールの方法論の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアップ的に用いると、我々の完全性定理を適用することにより、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なブロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この考え方に基づいて、与えられた実時間システム内での種々のプラニングの問題の論理的な分析ツールの方法論を開発した。