| 研究課題/領域番号 |
12480071
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
|
|---|
| 研究分担者 |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
ADEL Cherif (CHERIF Adel) 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10303322)
伊藤 恵 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30303324)
|
|---|
| 研究期間 (年度) |
2000 – 2002
|
| 研究課題ステータス |
完了 (2002年度)
|
| 配分額 *注記 |
7,500千円 (直接経費: 7,500千円)
2002年度: 1,500千円 (直接経費: 1,500千円)
2001年度: 3,200千円 (直接経費: 3,200千円)
2000年度: 2,800千円 (直接経費: 2,800千円)
|
|---|
| キーワード | オブジェクト指向方法論 / 組込みシステム / 分析モデル / 形式的方法論 / 定理証明システム / 並行正規表現 / スレッド / 並行オブジェクト / 組み込みシステム / 定理証明 / 形式的オブジェクト指向方法論 / オブジェクト / 実時間OS |
|---|
| 研究概要 |
オブジェクト指向方法論は、ビジネスシステムに対しては、最も有効な開発方法論であると認められており,組み込みシステムに対しても要求分析段階での有用性や発展性における優位性は十分に予想されているが、実装に関しては困難な問題もあり適用されていないのが現状である。我々は、(1)形式的オブジェクト指向分析モデルの構築とその上での定理証明技術にもとづく仕様検証、(2)並行オブジェクト構造からスレッド構造への自動的変換、(3)スレッド構造への実時間情報の付与と実時間OSタスク構造の生成、という方法により、オブジェクト指向方法論を適用した組み込みソフトウェアの構成法の研究を行った。以下に、得られた主要な成果を述べる。
(1)形式的オブジェクト指向モデルの構築と検証
組み込みシステムのオブジェクト分析モデルを構築し、モデルの正しさや適切さを検証するために、UMLを構築・検証するための理論体系と構築・検証環境のプロトタイプを構成した。環境は、構築したUMLをテスト実行するシステムと。クラスモデルにつけられた不変表明が満たされることをステートチャートモデルに関する帰納法で証明する検証システムからなる。テスト実行システムでは、MLによる動作記述が、また、検証システムでは定理証明システムHOLが用いられた。
(2)並列オブジェクト構造と並列スレッド構造の変換
並行オブジェクトと並行スレッドの振る舞いを表現できる形式的体系として並行正規表現を考え、並行正規表現間の等価性を判定するための公理体系を与えた。これにより、分析モデルとしの並行オブジェクト表現を,設計モデルとしての並行スレッド表現に等価変換するための基礎が確立した。この公理系にもとづいて、実際に等価変換を行うためにシステムを構築し、具体的な問題に適用して、その有効性を確認することが出来た。今後に残された課題は、この公理系に実時間情報や資源情報を加えて、最適な設計モデルの導出に関する研究に展開することである。
|
