モジュールシステムを基盤におくコーディネーションモデルの研究

2000 年度 実績報告書

• 研究課題/領域番号: 11878050
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• 研究分担者: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
• キーワード: コーディネーション / コンポーネント / 射影型振舞仕様 / 詳細化検証 / 高信頼 / 木アーキテクチャ / 開発支援ツール / CafeOBJ

研究概要

本年度は,以下のことを行った.
●高信頼コンポーネントソフトウェア開発:コンポーネントを組み合わせてソフトウェアを開発する方法の信頼性を高めるためのコーディネーションモデル(ソフトウェアアーキテクチャ)として「木アーキテクチャ」を提案した.木アーキテクチャの仕様記述には,詳細化検証の自動化が容易である射影型振舞仕様を用い,これにより,詳細化検証の自動化のみならず,コネクタの自動生成も可能となる.
●高信頼コンポーネントソフトウェア開発支援ツール:上記開発方法を支援するツールを設計し,ツールのプロトタイプを作成し,いくつかの例題を用いて開発方法および支援ツールの妥当性を確認した.
●分散システムの仕様記述と検証:分散システムの例として鉄道信号システムを取り上げ,CafeOBJで仕様を記述し,記述した仕様を基に,鉄道信号システムの安全性(列車同士の衝突は起こらない)を検証した.仕様記述の際に,鉄道信号システムに登場する各主体(列車,信号機,線路)の仕様をを独立に記述し,それらを部品として組み上げることで鉄道信号システム全体の仕様を記述した.

研究成果

• [文献書誌] Matsumoto,M.,Futatsugi,K.: "Higly reliable component-based software development by using algebraic behavioral specification"Proc.of 3rd IEEE Int'l Conference on Formal Engineering Methods (ICFEM'2000). 35-43 (2000)
• [文献書誌] Matsumoto,M.,Futatsugi,K.: "The support tool for highly reliable component-based software development"Proc.of 7th Asia-Pacific Software Engineering Conference (APSEC'2000). 172-179 (2000)
• [文献書誌] 松本充広,二木厚吉: "射影型振舞仕様を用いた高信頼コンポーネントソフトウェアの開発"ソフトウェア工学の基礎VII(FOSE'2000論文誌). 229-236 (2000)
• [文献書誌] 松本充広,二木厚吉: "高信頼コンポーネントソフトウェアの開発支援ツール"電子情報通信学会論文誌D-I. (2001)
• [文献書誌] Seino,T.,Ogata,K.,Futatsugi,K.: "Specification and verification of a single-track railroad signaling in CafeOBJ"Proc.of 2000 Int'l Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000). 268-273 (2000)
• [文献書誌] Nakamura,M.,Ogata,K.: "The evaluation strategy for head normal form with and without on-demand flags"Electronic Motes in Theoretical Computer Science (Proc.of the 3rd Int'l Workshop on Rewriting Logic and its Applications). 36. (2001)