研究課題
1.我々の形式仕様・形式検証の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。又、このロジカル・リーズニングの基本として線形論理を用いることが有効であることを示してきた。形式仕様記述には線形論理が用いられ、仕様を満たすプロセスは線形論理証明で表示され、安全性等の自動検証のために必要とされる稠密時間概念の消去手続は線形論理証明の変換手続として実現された。このような線形論理を用いたロジカル・リーズニングが安全性自動検証などの一部の検証に有効であるのみならず、実時間システムの改良や修正等のより広い範囲の分析にも有効であることを示す目的で、実装計画を進めた。2.我々の方法論をダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して応用した。現在までに試作した我々の線形論理自動検証系FATALISをダイナミックシステムの検証に適するように改良を進めた。3.セキュリティプロトコルの安全性検証のためのProtocol Logicsの主要部分が一階述語論理上で実現できることを示した。又、tracesをベースとしたformal semanticsを与え、我々のprotocol logicのsemantic completenessを与えた。又、これを使って我々のprotocol logicの決定問題を肯定的に解いた。さらにこの完全性証明を用いて時間制約を含む具体的なprotocolの安全性証明や反例生成の方法論を開発中である。
すべて 2005 2004
すべて 雑誌論文 (6件) 図書 (1件)
La revue internationale de philosophie No.230
ページ: 449-481
Electronic Notes in Theoretical Computer Science ; Proc.of RULE'05 (Invited Talk) (近刊)
In Image and Reasoning, eds.P.Grialou, G.Longo and M.Okada (近刊)
Proc.of International Workshop Foundations of Computer Security '04
ページ: 97-113
Lecture Note in Computer Science ; Proc.of the International Symposium on Software Security 2003 3233
ページ: 65-86
科学哲学(日本科学哲学会) 36・2
ページ: 79-102
