| 研究課題/領域番号 |
12480071
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
|
|---|
| 研究分担者 |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
伊藤 恵 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30303324)
|
|---|
| キーワード | 形式的オブジェクト指向方法論 / 組み込みシステム / オブジェクト / 並行オブジェクト / スレッド / 定理証明 / 実時間OS |
|---|
| 研究概要 |
オブジェクト指向方法論は、ビジネスシステムに対しては、最も有効な開発方法論であると認められているが、組み込みシステムに対しても、要求分析段階での有用性や発展性における優位性は十分に予想されているが、現実には適用されていない。その最大の理由は、性能上の問題によるものである。すなわち、オブジェクト指向方法論から得られるオブジェクトをそのままの形で並行オブジェクトして実装しても、組み込みシステムに必要な実行性能を得ることが出来ず、また、限られた実時間制約と記憶容量で動作させることが出来ないことである。また、現在のオブジェクト指向方法論はその形式性が低く、高信頼性のための検証などの計算機支援を分析・設計時に十分に行なえないという問題もある。
我々はこの問題を解決するために、(1)形式的オブジェクト指向分析モデルの構築とその上での定理証明技術にもとづく仕様検証、(2)並行オブジェクト構造からスレッド構造への自動的変換、(3)スレッド構造への実時間情報の付与と実時間OSタスク構造の生成、という方法が有効であろうと考え研究を実施、以下に述べる研究成果を得た。
(1)高階関数によるオブジェクト指向分析モデルの形式的記述法
(2)分析モデルの整合性検証法と高階論理HOLによるプロトタイプ実装
(3)並行オブジェクトを並行スレッドに変換するための公理系の提案
(4)並行スレッドのタスクへの基本変換法の提案
(実時間性、資源制約の考察は来年度に行なう。)
|
