Verification Methods for Highly Parallelized Embedded Software

2010 Fiscal Year Self-evaluation Report

• Project/Area Number: 20680001
• Research Category: Grant-in-Aid for Young Scientists (A)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: AOKI Toshiaki Japan Advanced Institute of Science and Technology, 情報科学研究科, 准教授 (20313702)
• Project Period (FY): 2008 – 2011
• Keywords: 形式検証 / モデル検査

Research Abstract

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

Research Products

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