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

2011 年度 研究成果報告書

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

研究概要

本研究では,スケジューリングを伴う並行・並列ソフトウェアと,スケジューリングを提供するリアルタイムオペレーティングシステム(RTOS)を対象とした.成果としては,前者に関しては,実時間を含む振る舞いを検証するためのアルゴリズムおよびツールを提案し,後者に関しては, RTOSの設計と実装を検証する手法およびツールを提案し,実際に使われているRTOSの検証も行った.これにより,現実的なセッティングで,モデル検査に基づいた手法の提案に成功し,実際に,現実問題に適用できることがわかった.

研究成果

• [雑誌論文] A Minimized Assumption Generation Method for Component-Based Software Verification (2010)
  • 著者名/発表者名: Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
  • 雑誌名: IEICE Transactions 巻: 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
  • 査読あり
• [雑誌論文] Evolution of a course on model checking for practical applications (2009)
  • 著者名/発表者名: Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, Shinichi Honiden
  • 雑誌名: ACM SIGCSE Bulletin 巻: Volume 41, Issue 2(June2009) ページ: 38-44
  • 査読あり
• [雑誌論文] 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(June2009) ページ: 45-50
  • 査読あり
• [学会発表] An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification (2012)
  • 著者名/発表者名: Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
  • 学会等名: IEEE-RIVF International Conference on Computing and Communication Technologies
  • 発表場所: ホーチミンシティ,ベトナム
  • 年月日: 2012-02-28
• [学会発表] Conformance Testing for OSEK/VDX Operating System Using Model Checking (2011)
  • 著者名/発表者名: Jiang Chen, Toshiaki Aoki
  • 学会等名: Asia-Pacific Software Engineering Conference
  • 発表場所: ホーチミンシティ,ベトナム
  • 年月日: 2011-11-07
• [学会発表] Pattarasinee Bhattarakosol, Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking (2011)
  • 著者名/発表者名: Warawoot Pacharoen, Toshiaki Aoki, Athasit Surarerks
  • 学会等名: IEEE International Conference on Web Services
  • 発表場所: ワシントンDC,アメリカ
  • 年月日: 2011-07-04
• [学会発表] Automated Adaptor Generation for Services Based on Pushdown Model Checking (2011)
  • 著者名/発表者名: Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
  • 学会等名: IEEE International Conference and Workshops on Engineering of Computer-Based Systems
  • 発表場所: ラスベガス,アメリカ
  • 年月日: 2011-04-18
• [学会発表] Assume-Guarantee Tools for Component-Based Software Verification (2010)
  • 著者名/発表者名: Pham Ngoc Hung, Nguyen Viet Ha, Toshiaki Aoki, Takuya Katayama
  • 学会等名: International Conference on Knowledge and Systems Engineering
  • 発表場所: ハノイ,ベトナム
  • 年月日: 2010-10-08
• [学会発表] Automatic Generation of Model Checking Scripts based on Environment Modeling (2010)
  • 著者名/発表者名: Kenro Yatake, Toshiaki Aoki
  • 学会等名: International SPIN Workshop on Model Checking of Software
  • 発表場所: エンスヘーデ,オランダ
  • 年月日: 2010-09-27
• [学会発表] Modeling of Real-Time System Designs for Parametric Analysis (2010)
  • 著者名/発表者名: Chaiwat Sathawornwichit, Toshiaki Aoki, Takuya Katayama
  • 学会等名: IEEE International Conference on Embedded and Real-Time Computing Systems and Applications
  • 発表場所: タイパ,マカオ
  • 年月日: 2010-08-23
• [学会発表] Alloyを用いた構成変更支援ツールと適用実験 (2010)
  • 著者名/発表者名: 谷崎裕明,青木利晃,片山卓也
  • 学会等名: 情報処理学会第169回ソフトウェア工学研究会
  • 発表場所: 北九州
  • 年月日: 2010-07-22
• [学会発表] RTOS設計検証の経験から (2010)
  • 著者名/発表者名: 青木利晃
  • 学会等名: ソフトウェアシンポジウム
  • 発表場所: 横浜
  • 年月日: 2010-06-10
• [学会発表] Non-Regular Adaptation of Services Using Model Checking (2010)
  • 著者名/発表者名: Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
  • 学会等名: IEEE International Symposium on Object-Oriented/Component/Service-oriented Real-Time Distributed Computing
  • 発表場所: カルモナ,スペイン
  • 年月日: 2010-05-06
• [学会発表] 形式手法教育の取り組みについて (2010)
  • 著者名/発表者名: 青木利晃
  • 学会等名: 先端ソフトウェア工学に関するGrace国際シンポジウム形式手法の産業応用ワークショップ2010
  • 発表場所: 東京
  • 年月日: 2010-03-15
• [学会発表] 環境モデリングによるモデル検査スクリプトの自動生成 (2009)
  • 著者名/発表者名: 矢竹健朗,西端浩和,青木利晃
  • 学会等名: 組込みシステムシンポジウム
  • 発表場所: 東京
  • 年月日: 2009-10-21
• [学会発表] MCBOK2008 :ソフトウェア開発のためのモデル検査知識体系 (2009)
  • 著者名/発表者名: 西原秀明,青木利晃,粂野文洋,篠崎孝一,田口研治,早水公二
  • 学会等名: 組込みシステムシンポジウム
  • 発表場所: 東京
  • 年月日: 2009-10-21
• [学会発表] モデル検査手法の普及活動とその応用 (2009)
  • 著者名/発表者名: 青木利晃
  • 学会等名: SPI Japan 2009
  • 発表場所: 新潟
  • 年月日: 2009-10-06
• [学会発表] An effective framework for assume-guarantee verification of evolving component-based software (2009)
  • 著者名/発表者名: Pham Ngoc Hung, Toshiaki Aoki and Takuya Katayama
  • 学会等名: Proceedings of the joint international and annual ERCIM workshops on Principles of software evolution(IWPSE) and software evolution(Evol) workshops
  • 発表場所: アムステルダム,オランダ
  • 年月日: 2009-09-20
• [学会発表] A Minimized Assumption Generation Method for Component-Based Software Verification (2009)
  • 著者名/発表者名: Pham Ngoc Hung, Toshiaki Aoki and Takuya Katayama
  • 学会等名: In the 6th International Colloquium on Theoretical Aspect of Computing
  • 発表場所: クアランプール,マレーシア
  • 年月日: 2009-08-16
• [学会発表] NGUYEN Tam Thi Minh,モデル検査による設計検証と整合テスト (2009)
  • 著者名/発表者名: 青木利晃
  • 学会等名: 情報処理学会第14回組込みシステム研究会
  • 発表場所: 愛知
  • 年月日: 2009-07-24
• [学会発表] 実用的な形式手法-モデル検査手法とその応用 (2009)
  • 著者名/発表者名: 青木利晃
  • 学会等名: 東芝ソフトウェアフォーラム2009/第九回東芝SEPGカンファレンス
  • 発表場所: 神奈川
  • 年月日: 2009-07-10
• [学会発表] Detecting and Analyzing State Inconsistencies in Multi-task Software (2009)
  • 著者名/発表者名: Toshiaki Aoki, Tadashi Sekiguchi, Masayuki Hirayama, and Tomoji Kishi
  • 学会等名: 12^<th> IEEE International Symposium on Object-Oriented/Component/Service-oriented Real-Time Distributed Computing
  • 発表場所: 東京
  • 年月日: 2009-03-20
• [学会発表] Cプログラムの実行に基づいたモデル検査実験 (2008)
  • 著者名/発表者名: 土肥雅俊,青木利晃
  • 学会等名: ソフトウェア工学の基礎ワークショップ
  • 発表場所: 兵庫
  • 年月日: 2008-11-14
• [学会発表] モデル検査によるリアルタイムオペレーティングシステムの設計検証 (2008)
  • 著者名/発表者名: 青木利晃,山崎真吾
  • 学会等名: 組込みシステムシンポジウム
  • 発表場所: 東京
  • 年月日: 2008-10-31
• [学会発表] Model Checking Multi-task Software on Real-time Operating Systems (2008)
  • 著者名/発表者名: Toshiaki Aoki
  • 学会等名: International Symposium on Object-Oriented Real-Time Distributed Computing 2008
  • 発表場所: フロリダ,アメリカ
  • 年月日: 2008-05-07
• [図書] 組込みソフトウェア開発技術, 9章組込みソフトウェアの静的検証技術 (2011)
  • 著者名/発表者名: 青木利晃
  • 総ページ数: 351
  • 出版者: CQ出版
• [図書] 知識ベース, UML/ステートチャート, 7群1編2章5節 (2009)
  • 著者名/発表者名: 青木利晃
  • 総ページ数: 35-44
  • 出版者: 電子情報通信学会
• [図書] SPINによる設計モデル検証 (2008)
  • 著者名/発表者名: 吉岡信和,青木利晃,田原康之
  • 総ページ数: 226
  • 出版者: 近代科学社