| 研究課題/領域番号 |
11480067
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| 研究分担者 |
天野 憲樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30313703)
森 彰 産業技術総合研究所, グループリーダ (30311682)
|
|---|
| 研究期間 (年度) |
1999 – 2002
|
| 研究課題ステータス |
完了 (2002年度)
|
| 配分額 *注記 |
14,600千円 (直接経費: 14,600千円)
2002年度: 3,600千円 (直接経費: 3,600千円)
2001年度: 3,500千円 (直接経費: 3,500千円)
2000年度: 3,400千円 (直接経費: 3,400千円)
1999年度: 4,100千円 (直接経費: 4,100千円)
|
|---|
| キーワード | コンポネント / 代数仕様 / CafeOBJ / PigNose / 形式仕様 / 検証 / 導出 / 高品位ソフトウェア / 形式手法 / コンポーネント / 高信頼 / 支援ツール / モジュールシステム / 仕様 / 分散システム / 分散オブジェクト / ソフトウェア・コンポネント / 詳細化検証 / 安全性検査 / 仕様リポジトリ / シグネチャ・マッチング / 振舞詳細化 / モデル検査 |
|---|
| 研究概要 |
将来のソフトウェア産業の基盤技術として必要不可欠である,コンポネントが必要とされている仕様を満たしていることを厳密に検査する基礎技術およびツールの開発を行った.本研究では,仕様のコンポーネント化を支援するための諸機能を有する仕様記述言語CafeOBJを基盤ツールとして用いた.CafeOBJは,研究代表者を中心に開発を続けている代数仕様記述言語で,抽象データ型のみならず抽象機械の記述にも適しており,仕様のコンポネント化を支援する強力なモージュルシステムを有するのも特徴の一つである.具体的な研究成果は以下のとおりである.(1)定理証明器の設計・開発:CafeOBJの項で表現された一階述語論理式に対し導出を行う機能(PigNose)をCafeOBJシステムに組込み,いくつかの例題に適用し有効性を確認した.(2)コンポネントに基づくシステム開発法:コンポネントを組み上げて高品位のソフトウェアを作成するための基礎理論を作り,その理論に基づいてソフトウェアを作成するツールの設計および作成を行った.(3)検証実験:CafeOBJ支援のもとで検証する方法を整理・提案し,鉄道信号システムやセキュリティシステム等に適用することで有効性を確認した.
|
