• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2001 年度 実績報告書

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

研究課題

研究課題/領域番号 12480071
研究機関北陸先端科学技術大学院大学

研究代表者

片山 卓也  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)

研究分担者 青木 利晃  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
CHERIF Adel  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10303322)
キーワードオブジェクト指向方法論 / 組み込みシステム / 分析モデル / 定理証明 / 並行オブジェクト / スレッド
研究概要

本研究課題では、オブジェクト指向方法論による組み込みシステムの科学的構成法の確立を目指して研究をおこなってきたが、平成13年度は下記研究課題1および研究課題2の研究を行なった。
1.組み込みシステムに特化した形式的オブジェクト指向分析法の展開、定理証明技術およびプロトタイプ実行に基づくモデル検証
2.並行オブジェクト構造からスレッド構造への変換
即ち、形式的オブジェクト指向方法論を用いて組み込みシステムの形式的分析モデルを構成し、その適切さを定理証明系やプロトタイプ実行を通して確立する方法論の研究、および並行オブジェクトで与えられる統合分析モデルを現実の計算機アーキテクチャに適合させ、効率良く実行させるための研究を行なった。
前者に関しては、(1)組み込みシステムのモデル化に必要な分析モデルの形式化と、それらの間の整合性検証法の確立、(2)分析モデルの高階論理シズテムHOLでの公理化、分析モデル間の整合性検証法のための証明システムに関して有効な成果を得た。また、HOLでの証明では、対象ドメインの公理化が必須であることから、どのドメインにも有効なオブジェクトドメインの公理化を行った。
後者に関しては、並行オブジェクトの動作を並行スレッドに変換するための変換規則を得た。これは並行オブジェクトを表現する並行正規表現をスレッド正規表現に変換するもので、変換規則の健全性を証明した。

  • 研究成果

    (4件)

すべて その他

すべて 文献書誌 (4件)

  • [文献書誌] 青木利晃, 立石孝彰, 片山卓也: "定理証明技術のオブジェクト指向分析への適用"コンピュータソフトウェア. 18巻4号. 18-48 (2001)

  • [文献書誌] Toshiaki Aoki, Takaaki Tateishi, Takuya Katayama: "An Axiomatic Formalization of UML Models"Proc. Workshop on Practical UML-based Rigorous Development Methods. 13-28 (2001)

  • [文献書誌] Toshiaki Aoki, Takuya Katayama: "Prototype Execution of Independently Constructed Analysis Models"Automating the Object-Oriented Software Development Methods, ECOOP2001 Workshop. (2001)

  • [文献書誌] Takuya Katayama: "Putting Formalities into Object-Oriented Methodologies"PDCAT(Invited Talk). (2001)

URL: 

公開日: 2003-04-03   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi