Compositional models and its structural verification of real time software

• Project/Area Number: 20500030
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: OGAWA Mizuhito Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (40362024)
• Co-Investigator(Kenkyū-buntansha): ONO Satoshi 工学院大学, 情報工学部, 教授 (90407164)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2010)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2010: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2009: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2008: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
• Keywords: 仕様記述 / 仕様検証 / リアルタイムソフトウェア / 非同期処理 / モデル検査 / 構造検証

Research Abstract

Aiming compositional verification of soft real time software, as foundation of modeling, extensions, algorithms for scalability, and tool implementation of pushdown model checking are shown (Journal 1, Oral presentation 1～3). As an experiment and case studies of asynchronous multi stage processing, their modeling and formal verification methodology on security access control and protocols on a web server are investigated (Oral presentation 4～8).

Research Products

• [Journal Article] Alternate Stacking Technique Revisited : Inclusion Problem of Superdeterministic Pushdown Automata (2008)
  • Author(s): Nguyen Van Tang, Mizuhito Ogawa
  • Journal Title: IPSJ Transactions on Programming Vol.1
  • NAID: 130000022132
  • Peer Reviewed
• [Journal Article] Alternate Stacking Technique Revisited : Inclusion Problem of Superdeterministic Pushdown Automata (2008)
  • Author(s): Nguyen Van Tang, Mizuhito Ogawa
  • Journal Title: IPSJ Transactions on Programming 1(Web公開)
  • NAID: 130000022132
  • Peer Reviewed
• [Presentation] 分散型オンデマンド仮想システム構築法の提案 (2011)
  • Author(s): 濱田惇司、小野諭
  • Organizer: 電子情報通信学会・インターネットアーキテクチャ研究会
  • Place of Presentation: 東京
  • Year and Date: 2011-02-18
• [Presentation] 分散型オンデマンド仮想システム構築法の提案 (2011)
  • Author(s): 濱田惇司、小野諭
  • Organizer: 電子情報通信学会・インターネットアーキテクチャ研究会(IA)
  • Place of Presentation: 機械振興会館(東京)
  • Year and Date: 2011-02-18
• [Presentation] 機能ロールに基づいた動的職責分離の形式的検証手法 (2010)
  • Author(s): 越智通宣、小野諭
  • Organizer: 電子情報通信学会・情報セキュリティ研究会
  • Place of Presentation: 東京
  • Year and Date: 2010-05-21
• [Presentation] 機能ロールに基づいた動的職責分離の形式的検証手法 (2010)
  • Author(s): 越智通宣、小野諭
  • Organizer: 電子情報通信学会・情報セキュリティ研究会(ISEC)
  • Place of Presentation: 機械振興会館(東京)
  • Year and Date: 2010-05-21
• [Presentation] 動的職責分離を記述できるアクセス制御モデルの形式的検証手法 (2010)
  • Author(s): 越智通宣、小野諭
  • Organizer: 電子情報通信学会・情報セキュリティ研究会
  • Place of Presentation: 信州大学
  • Year and Date: 2010-03-04
• [Presentation] Conditional Weighted Pushdown Systems and Applications (2010)
  • Author(s): Xin Li, Mizuhito Ogawa
  • Organizer: ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation(PEPMIO)(pp.141-150)
  • Place of Presentation: マドリッド
  • Year and Date: 2010-01-19
• [Presentation] Conditional Weighted Pushdown Systems and Applications (2010)
  • Author(s): Xin Li, Mizuhito Ogawa
  • Organizer: ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation PEPM10
  • Place of Presentation: マドリッド、スペイン
  • Year and Date: 2010-01-19
• [Presentation] Stacking-based Context-Sensitive Points-to Analysis for Java (2009)
  • Author(s): Xin Li, Mizuhito Ogawa
  • Organizer: Haifa Verification Conference 2009(HVC09)(pp.133-149)(Springer LNCS 6405)
  • Place of Presentation: イスラエル
  • Year and Date: 2009-10-20
• [Presentation] Stacking-based Context-Sensitive Points-to Analysis for Java (2009)
  • Author(s): Xin Li, Mizuhito Ogawa
  • Organizer: Haifa Verification Conference 2009 HVC09
  • Place of Presentation: ハイファ、イスラエル
  • Year and Date: 2009-10-20
• [Presentation] Event-Clock Visibly Pushdown Automata (2009)
  • Author(s): Nguyen Van Tang, Mizuhito Ogawa
  • Organizer: 35th Tnternational Conference on Current Trends in Theory and Practice of Computer Science(SOFSEM09)(pp.558-569)(Springer LNCS5404)
  • Place of Presentation: チェコ
  • Year and Date: 2009-01-27
• [Presentation] Event-Clock Visibly Pushdown Automata (2009)
  • Author(s): Nguyen Van Tang, Mizuhito Ogawa
  • Organizer: 35th International Conference on Current Trends in Theoryand Practice of Computer Science, SOFSEM09
  • Place of Presentation: チェコ
  • Year and Date: 2009-01-27
• [Presentation] スケーラブルなWebサーバ・ソフトウェア構成法の研究 (2008)
  • Author(s): 森春紀、小野諭
  • Organizer: 電子情報通信学会・情報セキュリティ研究会
  • Place of Presentation: 東京
  • Year and Date: 2008-12-17
• [Presentation] スケーラブルなWebサーバ・ソフトウェア構成法の研究 (2008)
  • Author(s): 森春紀, 小野諭
  • Organizer: 電子情報通信学会・情報セキュリティ研究会
  • Place of Presentation: 東京都
  • Year and Date: 2008-12-17
• [Presentation] Authentication Revisited : Flaw or Not, the Recursive Authentication Protocol (2008)
  • Author(s): Guoqiang Li, Mizuhito Ogawa
  • Organizer: 6th International Symposium on Automated Technology for Verification and Analysis(ATVA08)(pp.374-385)(Springer LNCS 5311)
  • Place of Presentation: 韓国
  • Year and Date: 2008-10-21
• [Presentation] Authentication Revisited : Flaw or Not, the Recursive Authenticati on Protocol (2008)
  • Author(s): Guoqiang Li, Mizuhito Ogawa
  • Organizer: 6th International Symposium on Automated Technology for Verification and Analysis, ATVA08
  • Place of Presentation: 韓国
  • Year and Date: 2008-10-21
• [Remarks] ホームページ等