述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法

2009 Fiscal Year Annual Research Report

• Project/Area Number: 19500025
• Research Institution: Kanazawa University
• Principal Investigator: 山根 智 Kanazawa University, 電子情報学系, 教授 (70263506)
• Keywords: リアルタイムオブジェクト指向 / 抽象化精錬検証 / 構造とリアルタイム性の抽象化 / 動的リアルタイムCEGAR / モデル検査 / オブジェクトの生成消滅

Research Abstract

本年度は、19年度のステートチャートの構造の抽象化精錬検証方式の開発と実装及び時間ステートチャートの構造と時間の抽象化精錬検証方式の開発と実装、20年度のリアルタイムオブジェクト指向言語の設計とその検証方式の開発を受けて、オブジェクトが生成消滅するシステムの抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。
その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。
これは、リアルタイムシステムの効率的な検証方式の実現可能性を実証したばかりではなく、広くオブジェクト指向システムの効率的な検証方式の実現可能性を実証しており、Javaなどのオブジェクト指向言語で記述されたインターネット上のソフトウェアの効率的な検証方式の実現可能性を示唆しているといった重要な意義のあるものである。
来年度は、本研究の成果を広く適用させるために、広くオブジェクト指向システムの効率的な検証方式の解明に取り掛かる予定である。

Research Products

• [Journal Article] Development Method for Real-Time Software based on Timed Weak Simulation Verification (2010)
  • Author(s): 山根智
  • Journal Title: Embedded Systems : Status and Perspective (In press)
  • Peer Reviewed
• [Journal Article] (2010)
  • Author(s): 山根智(分担)(共著)
  • Journal Title: 電子情報通信学会ハンドブック/知識ベース (オーム社) (電子版公開予定) Pages: 1-6
• [Journal Article] 階層構造の抽象化精錬によるステートチャートの自動検証 (2009)
  • Author(s): 山根智, 山崎真一
  • Journal Title: コンピュータソフトウェア 26(3) Pages: 155-170
  • Peer Reviewed
• [Journal Article] 組込みシステムにおけるハイブリッドオートマトンの形式的手法 (2009)
  • Author(s): 山根智
  • Journal Title: 計測と制御 48(11) Pages: 810-815
• [Presentation] 確率時間CEGAR (2009)
  • Author(s): 森下篤, 駒形龍太, 山根智
  • Organizer: 電子情報通信学会
  • Place of Presentation: 名古屋大学 (愛知県)
  • Year and Date: 2009-11-26