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

2000 年度 実績報告書

• 研究課題/領域番号: 10558043
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• 研究分担者: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991) ; 渡部 卓雄 東京工業大学, 情報理工学研究科, 助教授 (20222408)
• キーワード: コンポーネント / 機能的性質 / 非機能的性質 / 代数仕様 / ソフトウェア発展 / 射影型振舞仕様 / 詳細化検証 / 木アーキテクチャ

研究概要

本年度は,以下のことを行った.
・コンポーネントに基づくソフトウェア開発におけるソフトウェア発展:コンポーネントに基づくソフトウェア構築では,コンポーネントを組み上げて作成したシステムの性能の予測が難しい.性能とは,システムの非機能的性質で,システムの応答速度や実行効率,メモリの使用効率等を指す.非機能的な性質は,機能的性質,つまりシステムの論理的で静的な性質が満たされた上で初めて議論可能である.機能的性質と非機能的性質の2つの側面に着目し,その2つの側面がコンポーネントに基づく代数仕様の枠組みを使って、うまく扱えることを示した。
・高信頼コンポーネントソフトウェア開発および支援ツール:コンポーネントを組み合わせてソフトウェアを開発する方法の信頼性を高めるためのコーディネーションモデル(ソフトウェアアーキテクチャ)として「木アーキテクチャ」を提案した.木アーキテクチャの仕様記述には,詳細化検証の自動化が容易である射影型振舞仕様を用い,これにより,詳細化検証の自動化のみならず,コネクタの自動生成も可能となる.さらに,この発方法を支援するツールを設計し,ツールのプロトタイプを作成し,いくつかの例題を用いて開発方法および支援ツールの妥当性を確認した.

研究成果

• [文献書誌] Iida,S.,Futatsugi,K.: "Formal approach for handing software evolution in component-based software developments"Proc.of Int'l Symposium on Principles of Software Evolution 2000. (2000)
• [文献書誌] 飯田周作,二木厚吉: "形式仕様を用いたシステムの非機能的性質記述の試み-コンポーネントに基づくソフトウェア開発への応用-"ソフトウェア・シンポジウム2000. (2000)
• [文献書誌] 飯田周作,二木厚吉: "振舞仕様に基づく仕様コンポーネント化技術の発展可能ソフトウェアへの応用"コンピュータソフトウェア別冊ソフトウェア発展. 30-45 (2001)
• [文献書誌] 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)
• [文献書誌] 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)