分散チェックポインティングを用いたネットワークアプリケーションのモデル検査

2013 年度 研究成果報告書

• 研究課題/領域番号: 23300004
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 千葉大学
• 研究代表者: 山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
• 研究分担者: 萩谷 昌己 東京大学, 情報理工学系研究科, 教授 (30156252) ; アルト シリル 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 主任研究員 (30462831) ; 田辺 良則 国立情報学研究所, アーキテクチャ科学系, 特任教授 (60443199)
• 研究協力者: レオンワタナキット ワチャリン 東京大学 ; ヴァイテル フランツ 千葉大学 ; ポッター リチャード 東京大学 ; セビ ナジム 東京大学
• 研究期間 (年度): 2011-04-01 – 2014-03-31
• キーワード: モデル検査 / チェックポインティング

研究概要

我々の先行研究課題の成果であるネットワークアプリケーションのモデル検査手法をさらに発展させ、分散チェックポインティングを利用することで、より複雑かつ実際的な環境の下で動作するネットワークアプリケーションの検証を可能にした。これは分散チェックポインティングにおける通信の復元機能を実現することによって達成された。また、ネットワークAPIをより実際的なネットワークアプリケーションで用いられているものに対応させ、より広い範囲のアプリケーションの検査を可能にした。

研究成果

• [雑誌論文] Modular Software Model Checking for Distributed Systems (2014)
  • 著者名/発表者名: W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto, and K. Takahashi
  • 雑誌名: IEEE Transactions on Software Engineering 巻: Vol.40, No. 5 ページ: 483-501
  • DOI: 10.1109/TSE.2013.49
  • 査読あり
• [雑誌論文] Modbat ; A Model-based API Tester for Event-driven Systems (2013)
  • 著者名/発表者名: C. Artho, A. Biere, M. Hagiya, E. Platon, M. Seidl, Y. Tanabe, and M. Yamamoto
  • 雑誌名: Hardware and Software : Verification and Testing, 9th International Haifa Verification Conference, HVC 2013 巻: 8244 ページ: 112-128
  • DOI: 10.1007/978-3-319-03077-7_8
  • 査読あり
• [雑誌論文] Software Model Checking for Distributed Systems with Selector-Based (2013)
  • 著者名/発表者名: C. Artho, M. Hagiya, R. Potter, Y. Tanabe, F. Weitl, and M. Yamamoto
  • 雑誌名: Non-blocking Communication, 28th IEEE/ACM International Conference on Automated Software Engineering (ASE) ページ: 169-179
  • DOI: 10.1109/ASE.2013.6693077
  • 査読あり
• [雑誌論文] Model Checking Distributed Systems by Combining Caching and Process Checkpointing (2011)
  • 著者名/発表者名: W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, and M. Yamamoto
  • 雑誌名: 26th IEEE/ACM International Conference on Automated Software Engineering (ASE) ページ: 103-112
  • DOI: 10.1109/ASE.2011.6100043
  • 査読あり
• [学会発表] Modbat : A model-based API tester for event-driven systems (2012)
  • 著者名/発表者名: Cyrille Artho
  • 学会等名: 第10回ディペンダブルシステムワークショップ(DSW2012)
  • 発表場所: 独立行政法人理化学研究所計算科学研究機構
  • 年月日: 20121211-12
• [備考]
  • URL: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache