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