高度な並行・並列組込みソフトウェアの検証法に関する研究

2010 年度 自己評価報告書

• 研究課題/領域番号: 20680001
• 研究種目: 若手研究(A)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
• 研究期間 (年度): 2008 – 2011
• キーワード: 形式検証 / モデル検査

研究概要

最近の組込みソフトウェアは,マルチタスクが取り扱い可能なリアルタイムオペレーティングシステムを用いるだけでなく,マルチCPU,マルチOS,マルチコアCPUを用いて高度に並行・並列化されて実装されている.そこで,本研究課題では,このような高度に並行・並列化された組込みソフトウェア,さらには,それらがヘテロに組み合わされた組込みソフトウェアを対象とした検証法を,モデル検査手法を拡張することにより提案する.

研究成果

• [雑誌論文] A Minimized Assumption Generation Method for Component-Based Software Verification (2010)
  • 著者名/発表者名: Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
  • 雑誌名: IEICE Transactions Vol.E93-D, No.8 ページ: 2172-2181
  • 査読あり
• [雑誌論文] Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software (2009)
  • 著者名/発表者名: Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama
  • 雑誌名: IEICE Transactions Vol.E92-A, No.11 ページ: 2772-2780
  • 査読あり
• [雑誌論文] Model checking education for software engineers in Japan (2009)
  • 著者名/発表者名: Hideaki Nishihara, Koichi Shinozaki, Koji Hayamizu, Toshiaki Aoki, Kenji Taguchi, Fumihiro Kumeno
  • 雑誌名: ACM SIGCSE Bulletin Volume 41 , Issue 2 ページ: 45-50
  • 査読あり
• [学会発表] Automatic Generation of Model Checking Scripts based on Environment Modeling (2010)
  • 著者名/発表者名: Kenro Yatake, Toshiaki Aoki
  • 学会等名: The 17th International SPIN Workshop on Model Checking of Software(SPIN 2010), pp.58-75
  • 発表場所: オランダ
  • 年月日: 2010-09-27
• [学会発表] Chaiwat Sathawornwichit Modeling of Real-Time System Designs for Parametric Analysis (2010)
  • 著者名/発表者名: Toshiaki Aoki, Takuya Katayama
  • 学会等名: the 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2010), pp.81-91
  • 発表場所: マカオ
  • 年月日: 2010-08-23
• [学会発表] A Minimized Assumption Generation Method for Component-Based Software Verification (2009)
  • 著者名/発表者名: Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama
  • 学会等名: In the 6th International Colloquium on Theoretical Aspect of Computing, LNCS 5684, pp.277-291
  • 発表場所: マレーシア
  • 年月日: 2009-08-18
• [図書] 組込みソフトウェア開発技術(9章組込みソフトウェアの静的検証技術)ISBN978-4-7898-4548-9 (2011)
  • 著者名/発表者名: 青木利晃
  • 総ページ数: 271-307
  • 出版者: CQ出版
• [図書] SPINによる設計モデル検証 (2008)
  • 著者名/発表者名: 吉岡信和, 青木利晃, 田原康之
  • 総ページ数: 226
  • 出版者: 近代科学社