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

2001 Fiscal Year Annual Research Report

• Project/Area Number: 11878050
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
• Keywords: コンポーネント / 高信頼 / UML / OCL / CafeOBJ / Java / 分散(実時間)システム / 検証

Research Abstract

本年度は、以下のことを行った。
・高信頼コンポーネントソフトウェア開発:前年度に引き続き、コンポーネントを組み上げることで高信頼のソフトウェアを開発するための開発法に関する研究を行った。コンポーネントにより作成するソフトウェアの仕様をUMLとOCLで記述し、それらを代数仕様言語CafeOBJに変換し、作成しようとするソフトウェアが望ましい性質等を有している事をCafeOBJシステム支援のもとで検証する。さらに、CafeOBJからJavaプログラムに変換することでプロトタイプを容易に得ることが出来る。
・高信頼コンポーネントソフトウェア開発支援ツール:上記開発方法を支援するツールを設計、開発した。いくつかの例題をとおして有効性を確認した。
・分散(実時間)システムの仕様記述と検証:分散(実時間)システムのモデル化および検証方法を整理、提案した。提案手法の有効性を示すため、実時間相互排除在アルゴリズム(Fischerプロトコル)等の実時間システムをモデル化および検証の実験を行った。モデルの記述にはCafeOBJを用い、検証はCafeOBJシステム支援のもとで行った。

Research Products

• [Publications] 松本充広, 二木厚吉: "高信頼コンポーネントソフトウェアの開発ツール"電子情報通信学会論文誌 D-I. J84-D-I・6. 736-744 (2001)
• [Publications] 松本充広, 二木厚吉: "カタリシス法軽量フォーマルメソッド"ソフトウェア工学の基礎VIII(日本ソフトウェア科学会FOSE 01). (2001)
• [Publications] 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)
• [Publications] 清野貴博, 緒方和博, 二木厚吉: "実時間制約を考慮したマルチタスキングのモデル化"ソフトウェア工学の基礎VIII(日本ソフトウェア科学会FOSE 01). 143-146 (2001)