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