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

2001 Fiscal Year Annual Research Report

• Project/Area Number: 11480067
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Kenkyū-buntansha): 森 彰 経済産業省産業技術総合研究所, 研究者 (30311682)
• Keywords: コンポーネント / 高信頼 / 支援ツール / CafeOBJ / モジュールシステム / 仕様 / 分散システム / 検証

Research Abstract

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

Research Products

• [Publications] 松本充広, 二木厚吉: "高信頼コンポーネントソフトウェアの開発ツール"電子情報通信学会論文誌 D-I. J84-D-I・6. 736-744 (2001)
• [Publications] 松本充広, 二木厚吉: "カタルシス法軽量フォーマルメソッド"ソフトウェア工学の基礎VIII(日本ソフトウェア科学会FOSE 01). (2001)
• [Publications] 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)
• [Publications] 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)