Compositional models and its structural verification of real time software

2010 Fiscal Year Final Research Report

• 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
• 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
  • Peer Reviewed
• [Presentation] 分散型オンデマンド仮想システム構築法の提案 (2011)
  • Author(s): 濱田惇司、小野諭
  • Organizer: 電子情報通信学会・インターネットアーキテクチャ研究会
  • 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: 電子情報通信学会・情報セキュリティ研究会
  • 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] 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] 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] スケーラブルな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
• [Remarks] ホームページ等