実時間システムに対する論理的仕様・検証言語の国際共同実装計画

2002 Fiscal Year Annual Research Report

• Project/Area Number: 13558031
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Co-Investigator(Kenkyū-buntansha): 中川 中 (株)エスアールエー, ソフトウェア工学研究所, 部長(研究職) ; 田村 直之 神戸大学, 工学部, 助教授 (60207248) ; 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Keywords: 線形論理 / 形式仕様 / 形式検証 / 実時間システム

Research Abstract

線形論理に基づいた稠密実時問システムの仕様・検証系についての我々の理論的成果や萌芽的アィデアを用いて、これを応用することに焦点をあてて本研究を行ってきた。我々の線形論理的方法論に対する実装を行い、理論と実践の橋渡しをすることを目標としている。この目標のために、国際共同研究の形で論理的検証ツール実装のための設計及び実装試作を進めてきた。我々の用いる線形論理の部分体系および書き換え論理は実時間システムの安全性や種々のスケジューリング問題に対してPSPACE決定可能であることが日米共同研究(岡田グループとScedrovグループ)の理論的成果として確立されてきたが(このPSPACE-決定性はこの種の自動検証問題に対して最適な成果であることも知られている)、この理論に従って、我々の自動決定手続きを改良した。また、自動検証が不可能なより高度な検証問題は、決定可能な線形論理の部分体系を超えた、通常の線形論理の体系の証明システムを使用する必要がある。その典型は種々のパラメータを含む検証問題である。このような半自動的な検証を演繹的手法で行うことを実現するには、証明支援系(Proof-Assistance System)をわれわれの線形論理言語上で整備する必要がある。フランス側共同研究グループが開発したCoq System上でのProof-Assistance機構の実装のノウハウを利用しながら、岡田グループとCoqグループとの共同でこの証明支援系の設計を進めた。自動検証に用いる線形論理の部分体系の中核部分は本質的に書き換え論理と同型である。われわれは、この項書き換え系を基本とし、これに量化記号などの線形論理的表現力を強化する形でわれわれの仕様検証言語を整備した。

Research Products

• [Publications] Mitsuhiro Okada: "A Uniform Proof for Higher Order Cut-Elimination and Normalization theorem"Theoretical Computer Science. 281. 471-498 (2002)
• [Publications] M.Kanovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)
• [Publications] K.Hasebe-M.Okada: "A Logical Veritication Method for Security Protocols Based on Linear Logic and Ban Logic"Hot-topic series. 2609号. 422-445 (2003)
• [Publications] 岡田光弘, 長谷部浩二: "線形論理によるセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究会報告集. 102. 49-54 (2002)
• [Publications] 岡田光弘: "オントロジー工学の論理的基礎III「現代のフォーマルオントロジーの動向とオントロジー工学」"人工知能. 17巻4号. 434-442 (2002)
• [Publications] 岡田光弘: "オントロジー工学の論理的基礎IV「オントロジー応用のための方法論の考察と展望」"人工知能. 17巻5号. 604-613 (2002)
• [Publications] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)