機能に基づく仕様のコンポーネント化を可能とする形式仕様言語の開発

2001 年度 実績報告書

• 研究課題/領域番号: 10558043
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• 研究分担者: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991) ; 渡部 卓雄 東京工業大学, 情報理工学研究科, 助教授 (20222408)
• キーワード: コンポーネント / 高信頼 / 支援ツール / CafeOBJ / モジュールシステム / 仕様 / 分散(実時間)システム / 検証

研究概要

本研究では、仕様のコンポーネント化を支援するための諸機能を有する仕様記述言語CafeOBJを基盤ツールとして用いた。CafeOBJは、研究代表者を中心に開発を続けている代数仕様言語で、抽象データ型のみならず、オブジェクト指向におけるオブジェクトや抽象機械の記述にも適しており、仕様のコンポーネント化を支援する強力なモジュールシステムを有するのも特徴の一つである。
具体的には以下のことを行った。
・検証実験:鉄道の信号システム、航空管制システム、病院における患者監視システム等、人命に多大な影響を及ぼし得るシステムは、並列分散(実時間)システムであることが多い。これらシステムをCafeOBJ支援のことで検証する方法を整理、提案し、いくつかの事例研究をとおして提案手法の有効性を確認した。
・ツールの設計および作成:コンポーネントを組み上げて高品位のソフトウェアを作成するための基礎理論を作り、その理論に基づいてソフトウェアを作成するツールの設計および作成を行った。

研究成果

• [文献書誌] 松本充広, 二木厚吉: "高信頼コンポーネントソフトウェアの開発ツール"電子情報通信学会論文誌 D-1. J84-D-I・6. 736-744 (2001)
• [文献書誌] T.Seino, K.Ogata, K.Futatsugi: "Specification and verification of a single-track railroad signaling in CafeOBJ"IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science. E84-A・6. 1471-1478 (2001)
• [文献書誌] K.Futatsugi, K.Ogata: "Rewriting can verify distributed real-time systems"Proc. of the Int 1 Workshop on Rewriting in Proof and Computation (RPC 01). 60-79 (2001)
• [文献書誌] K.Ogata, K.Futatsugi: "Modeling and verification of distributed real-time systems based on CafeOBJ"Proc. of the 16^<th> IEEE Int 1 Conference on Automated Software Engineering (ASE 01). 185-192 (2001)
• [文献書誌] K.Ogata, K.Futatsugi: "Formally modeling and verifying Ricart & Agrawala distributed mutual exclusion algorithm"Proc. of the Second Asia-Pacific Conference on Quality Software (APAQS '01). 357-366 (2001)
• [文献書誌] K.Ogata, K.Futatsugi: "Formal analysis of Suzuki & Kasami distributed mutual exclusion algorithm"Proc. of the IFIP TC6/WG6.1 Fifth Int' 1 Conference on Formal Methods for Open Object-Based Distributed Systems. (2002)