リアルタイムソフトウェアのコンポジショナルな処理モデルとその構造検証

2010 年度 研究成果報告書

• 研究課題/領域番号: 20500030
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
• 研究分担者: 小野 諭 工学院大学, 情報工学部, 教授 (90407164)
• 研究期間 (年度): 2008 – 2010
• キーワード: 仕様記述 / 仕様検証 / リアルタイムソフトウェア / 非同期処理 / モデル検査

研究概要

本研究では、ソフトリアルタイムソフトウェア構造検証のモデル化の基礎として、プッシュダウンモデル検査の拡張・スケーラビリティ確保・およびそのツール実装を行った(雑誌論文1,学会発表1～3)。さらにアクセス制御の非同期多段処理の実験・ケースタディとして、同期処理による限界を示し、webサーバにおけるセキュリティ制御やセキュリティプロトコルについて各個別なモデル化と検証手法を示した。(学会発表4～8)。

研究成果

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