| Project/Area Number |
11878050
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
|
|---|
| Project Period (FY) |
1999 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2001: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2000: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1999: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | コンポーネント / 高信頼 / UML / OCL / CafeOBJ / Java / 分散(実時間)システム / 検証 / コーディネーション / 射影型振舞仕様 / 詳細化検証 / 木アーキテクチャ / 開発支援ツール / モデル / 言語 / モジュールシステム / Linda / 仕様記述 |
|---|
| Research Abstract |
本年度は、以下のことを行った。
・高信頼コンポーネントソフトウェア開発:前年度に引き続き、コンポーネントを組み上げることで高信頼のソフトウェアを開発するための開発法に関する研究を行った。コンポーネントにより作成するソフトウェアの仕様をUMLとOCLで記述し、それらを代数仕様言語CafeOBJに変換し、作成しようとするソフトウェアが望ましい性質等を有している事をCafeOBJシステム支援のもとで検証する。さらに、CafeOBJからJavaプログラムに変換することでプロトタイプを容易に得ることが出来る。
・高信頼コンポーネントソフトウェア開発支援ツール:上記開発方法を支援するツールを設計、開発した。いくつかの例題をとおして有効性を確認した。
・分散(実時間)システムの仕様記述と検証:分散(実時間)システムのモデル化および検証方法を整理、提案した。提案手法の有効性を示すため、実時間相互排除在アルゴリズム(Fischerプロトコル)等の実時間システムをモデル化および検証の実験を行った。モデルの記述にはCafeOBJを用い、検証はCafeOBJシステム支援のもとで行った。
|
