形式的オブジェクト指向方法論に基づく組み込みソフトウェアの構成法の研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12480071
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
• Co-Investigator(Kenkyū-buntansha): 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702) ; 伊藤 恵 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30303324)
• Keywords: 形式的オブジェクト指向方法論 / 組み込みシステム / オブジェクト / 並行オブジェクト / スレッド / 定理証明 / 実時間OS

Research Abstract

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

Research Products

• [Publications] Takaaki Tateishi: "An Axiomatic System For Verifying The Object-Oriented Analysis Model"SCI2000. 662-667 (2000)
• [Publications] Masumi Toyoshima: "Implementing Fault Tolerant Software In Distributed Environment"Kluwer Academic Publishers, Dependable Network Computing. 5. 341-358 (2000)
• [Publications] 岡崎光隆: "並行動作するオブジェクトからの処理列の抽出法"情報処理学会ソフトウェア工学研究会 研究報告. 2000-SE-129. 65-72 (2000)
• [Publications] 青木利晃: "オブジェクト指向組み込みシステム開発のための設計モデルSESモデル"日本ソフトウェア科学会 ソフトウェア工学の基礎ワークショップFOSE2000. 157-164 (2000)
• [Publications] 伊藤恵: "オブジェクト指向リアルタイムシステムのテスト支援環境"情報処理学会 オブジェクト指向シンポジウム2000. 49-56 (2000)
• [Publications] Takuya Katayama: "Principles and Mechanisms for Evolving Software Systems"6th IEEE International Conference on Engineering of Complex Computer Systems. (2000)