分散オブジェクト環境におけるコンポネント仕様の検証に関する研究

2002 年度 実績報告書

• 研究課題/領域番号: 11480067
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• 研究分担者: 天野 憲樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30313703) ; 森 彰 産業技術総合研究所, 研究員 (30311682)
• キーワード: コンポネント / 代数仕様 / CafeOBJ / PigNose / 形式手法 / 検証 / 導出 / 高品位ソフトウェア

研究概要

将来のソフトウェア産業の基盤技術として必要不可欠である,コンポネントが必要とされている仕様を満たしていることを厳密に検査する基礎技術およびツールの開発を行った.本研究では,仕様のコンポーネント化を支援するための諸機能を有する仕様記述言語CafeOBJを基盤ツールとして用いた.CafeOBJは,研究代表者を中心に開発を続けている代数仕様記述言語で,抽象データ型のみならず抽象機械の記述にも適しており,仕様のコンポネント化を支援する強力なモージュルシステムを有するのも特徴の一つである.具体的な研究成果は以下のとおりである.(1)定理証明器の設計・開発:CafeOBJの項で表現された一階述語論理式に対し導出を行う機能(PigNose)をCafeOBJシステムに組込み,いくつかの例題に適用し有効性を確認した.(2)コンポネントに基づくシステム開発法:コンポネントを組み上げて高品位のソフトウェアを作成するための基礎理論を作り,その理論に基づいてソフトウェアを作成するツールの設計および作成を行った.(3)検証実験:CafeOBJ支援のもとで検証する方法を整理・提案し,鉄道信号システムやセキュリティシステム等に適用することで有効性を確認した.

研究成果

• [文献書誌] Kokichi Futatsugi: "Formal Methods in CafeOBJ"Lecture Notes in Computer Science (LNCS). 2441. 1-20 (2002)
• [文献書誌] R.Diaconescu, K.Futatsugi: "Logical Foundations of CafeOBJ"Theoretical Computer Science. 285. 289-318 (2002)
• [文献書誌] 清野貴博, 緒方和博, 二木厚吉: "項書換えを用いた安全性検証の組織化"FOSE 2002:レクチャーノート/ソフトウェア工学. 28. 107-118 (2002)
• [文献書誌] K.Ogata, K.Futatsugi: "Formal analysis of Suzuki\&Kasami distributed mutual exclusion algorithm"Prof. of the IFIP TC6/WG6.1 Fifth Int'l Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002). 181-195 (2002)
• [文献書誌] K.Ogata, K.Futatsugi: "Formal verification of the Horn-Preneel micropayment"LNCS. 2575. 238-252 (2002)
• [文献書誌] A.Mori, K.Futatsugi: "CafeOBJ as a Tool for Behavioral System Verification"International Symposium on Software Security, LNCS. 2609(To appear). (2003)