Automatic verification method for large scale embedded object-oriented design based on predicate abstraction

• Project/Area Number: 19500025
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Kanazawa University
• Principal Investigator: YAMANE Satoshi Kanazawa University, 電子情報学系, 教授 (70263506)
• Project Period (FY): 2007 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000); Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2007: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: 組込みシステム / 述語抽象化検証 / オブジェクト指向 / リアルタイムオブジェクト指向 / 抽象化精錬検証 / 構造とリアルタイム性の抽象化 / 動的リアルタイムCEGAR / モデル検査 / オブジェクトの生成消滅 / 動的再構成組込みシステム / ハイブリッドオートマトン / 仕様記述言語 / 検証 / 述語抽象化洗練

Research Abstract

リアルタイムオブジェクト指向言語を開発して、オブジェクトが生成消滅するシステムに対して、構造と時間の抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。

Research Products

• [Journal Article] Development Method for Real-Time Software based on Timed Weak Simulation Verification (2010)
  • Author(s): S. Yamane
  • Journal Title: mbedded Systems: Status and Perspective, pp. 1-15, American Scientific publishers (in press)
  • Peer Reviewed
• [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: 計測と制御 Vol.48No.11 Pages: 810-815
  • NAID: 10026206099
• [Journal Article] "階層構造の抽象化精錬によるステートチャートの自動検証", コンピュータソフトウェア (2009)
  • Author(s): 山崎真一, 山根智
  • Journal Title: 日本ソフトウェア科学会 Vol.26,No.3 Pages: 155-170
  • Peer Reviewed
• [Journal Article] 確率ゾーングラフを用いた確率時間強模倣関係による検証 (2009)
  • Author(s): 橋爪裕樹, 山根智
  • Journal Title: 電子情報通信学会論文誌 No.1 Pages: 25-38
  • NAID: 110007380048
  • Peer Reviewed
• [Journal Article] 階層構造の抽象化精錬によるステートチャートの自動検証 (2009)
  • Author(s): 山根智, 山崎真一
  • Journal Title: コンピュータソフトウェア 26(3) Pages: 155-170
  • NAID: 130004549140
  • Peer Reviewed
• [Journal Article] 組込みシステムにおけるハイブリッドオートマトンの形式的手法 (2009)
  • Author(s): 山根智
  • Journal Title: 計測と制御 48(11) Pages: 810-815
  • NAID: 10026206099
• [Journal Article] 確率ゾーングラフを用いた確率時間強模倣関係による検証 (2009)
  • Author(s): 橋爪裕樹, 山根智
  • Journal Title: 電子情報通信学会論文誌 J91-D-I, No. 1 Pages: 25-38
  • NAID: 110007380048
  • Peer Reviewed
• [Journal Article] Special Section on Concurrent/Real-time and Hybrid Systems (2008)
  • Author(s): S. Yamane
  • Journal Title: Theory and Applications No.11 Pages: 3206-3206
• [Journal Article] 確率時間オートマトンの確率時間強模倣検証器の開発 (2008)
  • Author(s): 山根智, 小寺広志, 荒井恒夫
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会) Vol.25,No.3 Pages: 148-193
  • NAID: 110004809759
  • Peer Reviewed
• [Journal Article] リアルタイムシステムの形式的検証 (2008)
  • Author(s): 山根智
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会) Vol.25,No.3 Pages: 81-87
  • Peer Reviewed
• [Journal Article] "組込みシステムのフォーマルメソッドにおけるハイブリッドシステムの仕様記述と形式的検証", Fundamentals Review (2008)
  • Author(s): 山根智
  • Journal Title: 電子情報通信学会 Vol.2,No.1 Pages: 22-34
• [Journal Article] 確率時間オートマトンの確率時間強模倣検証器の開発 (2008)
  • Author(s): 山根智, 小寺広志, 荒井恒夫
  • Journal Title: コンピュータソフトウェア Vol. 25, No. 3 Pages: 148-193
  • NAID: 110004809759
  • Peer Reviewed
• [Journal Article] リアルタイムシステムの形式的検証 (2008)
  • Author(s): 山根智
  • Journal Title: コンピュータソフトウェア Vol. 25, No. 3 Pages: 81-87
  • Peer Reviewed
• [Journal Article] UMLと時間オートマトンを用いたソフトリアルタイムシステムの設計解析手法 (2007)
  • Author(s): 坂倉賢昭, 山根智
  • Journal Title: 情報処理学会論文 Vol.48,No9 Pages: 2410-2421
  • NAID: 110006423003
• [Journal Article] The automatic verification system for real-time systems using symbolic model-checking (2007)
  • Author(s): S. Yamane
  • Journal Title: Real-Time Systems: Modeling, Design, and Applications, volume 8 of AMAST Series in Computing Pages: 137-152
  • Peer Reviewed
• [Journal Article] Theory and practice of probabilistic timed game for Embedded Systems (2007)
  • Author(s): S. Yamane
  • Journal Title: Embedded Software and Systems, Lecture Notes in Computer Science 4523 Pages: 109-120
  • Peer Reviewed
• [Journal Article] The automatic verification system for real-time systems using symbolic model-checking (2007)
  • Author(s): 山根 智
  • Journal Title: volume 8 of AMAST Series in Computing 8 Pages: 137-152
  • Peer Reviewed
• [Journal Article] UMLと時間オートマトンを用いたソフトリアルタイムシステムの設計解析手法 (2007)
  • Author(s): 坂倉 賢昭、山根 智
  • Journal Title: 情報処理学会論文誌 Vol.48,No9 Pages: 2410-2421
  • NAID: 110006423003
  • Peer Reviewed
• [Journal Article] Theory and practice of probabilistic timed game for Embedded Systems (2007)
  • Author(s): 山根 智
  • Journal Title: Lecture Notes in Computer Science 4523 Pages: 109-120
  • Peer Reviewed
• [Presentation] 動的再構成可能プロセッサのモデル化, 仕様記述とモデル検査, 6回ディペンダブルシステムシンポジウム( DSS2009) (2009)
  • Author(s): 南翔太、瀧内新悟、瀬古口智、中居佑輝、山根智
  • Organizer: 日本ソフトウェア科学会
  • Place of Presentation: 大阪大学(大阪府)(102-121)
  • Year and Date: 2009-12-15
• [Presentation] 階層時間オートマトン群の並列動作の述語抽象化精錬検証手法, 6回ディペンダブルシステムシンポジウム(DSS2009) (2009)
  • Author(s): 山崎真一、酒井誠、山根智
  • Organizer: 日本ソフトウェア科学会
  • Place of Presentation: 大阪大学(大阪府)(179-197)
  • Year and Date: 2009-12-15
• [Presentation] 確率ゲーム理論による組込みシステムのモデル化とモデル検査 (2009)
  • Author(s): 越田彰太、山根智
  • Organizer: 電子情報通信学会信学技報
  • Place of Presentation: 名古屋大学(愛知県)
  • Year and Date: 2009-11-26
• [Presentation] 確率時間REGARによるPTCTLのサブクラスのモデル検査 (2009)
  • Author(s): 高橋正樹、森下篤、山根智
  • Organizer: 電子情報通信学会信学技報
  • Place of Presentation: 名古屋大学(愛知県)
  • Year and Date: 2009-11-26
• [Presentation] 確率時間CEGAR (2009)
  • Author(s): 森下篤, 駒形龍太, 山根智
  • Organizer: 電子情報通信学会研究報告
  • Place of Presentation: 名古屋大学(愛知県)
  • Year and Date: 2009-11-26
• [Presentation] 確率時間CEGAR (2009)
  • Author(s): 森下篤, 駒形龍太, 山根智
  • Organizer: 電子情報通信学会
  • Place of Presentation: 名古屋大学 (愛知県)
  • Year and Date: 2009-11-26
• [Presentation] 組込みシステムの形式的手法 (2009)
  • Author(s): 山根智
  • Organizer: 第22回回路とシステム軽井沢ワークショップ
  • Place of Presentation: 軽井沢プリンスホテル(長野県)
  • Year and Date: 2009-04-20
• [Presentation] 確率時間ゲーム理論による組込みシステムのモデル化, 仕様記述及び検証 (2009)
  • Author(s): 林将志、山根智
  • Organizer: 数理解析研究所講究録RIMS Kokyuroku
  • Place of Presentation: 京都大学数理解析研究所(京都府)
  • Year and Date: 2009-02-01
• [Presentation] 動的再構成可能組込みシステムのモデル化と仕様記述 (2008)
  • Author(s): 中居佑輝, 山根智
  • Organizer: 2008-EMB-10
  • Place of Presentation: キャンパスプラザ京都(京都府)
  • Year and Date: 2008-11-28
• [Presentation] 並列動作する確率時間システムに対する拡張CEGAR (2008)
  • Author(s): 安井雅俊, 山崎真一, 山根智
  • Organizer: 2008-EMB-10
  • Place of Presentation: キャンパスプラザ京都(京都府)
  • Year and Date: 2008-11-28
• [Presentation] 動的再構成可能組込みシステムのモデル化と仕様記述 (2008)
  • Author(s): 中居佑輝, 山根智
  • Organizer: 情報処理学会組込みシステム研究会
  • Place of Presentation: 京都市
• [Presentation] "ストップウォッチオートマトンによるプリエンプティブスケジューリングシステムの検証"、システム・情報部門学術講演会 (2007)
  • Author(s): 瀧内新吾、山根智
  • Organizer: 計測制御学会
  • Place of Presentation: 国立オリンピック記念青少年総合センター(東京都)
  • Year and Date: 2007-11-27
• [Presentation] チュートリアル"リアルタイムシステムの仕様記述と検証" (2007)
  • Author(s): 山根智
  • Organizer: 組込みシンポジュウム
  • Place of Presentation: 日本科学未来館(東京都)
  • Year and Date: 2007-10-18
• [Presentation] 組み込システムのUML分析設計からタスク設計までの設計検証方法論 (2007)
  • Author(s): 山根智、瀧内新吾
  • Organizer: 情報処理学会研究報告
  • Place of Presentation: キャンパスプラザ京都(京都府)
  • Year and Date: 2007-09-28
• [Presentation] 抽象化洗練によるステートチャートの自動検証 (2007)
  • Author(s): 山崎 真一、山根 智
  • Organizer: 日本ソフトウェア科学会
  • Place of Presentation: 奈良先端大学院大学
  • Year and Date: 2007-09-16
• [Presentation] 制限付きストップウォッチオートマトンと時間オートマトンを用いた, プリエンプティブスケジューリングシステムのUML分析設計からタスク設計までの設計検証方法論 (2007)
  • Author(s): 山根智、瀧内新悟
  • Organizer: 電子情報通信学会ソサエティ大会シンポジュム
  • Place of Presentation: 鳥取大学(鳥取県)
  • Year and Date: 2007-09-13
• [Book] "ハイブリッドオートマトン", 電子情報通信学会ハンドブック/知識ベース (2010)
  • Author(s): 山根智
  • Publisher: オーム社