形式手法の統合によるシームレスなソフトウェア開発手法の提案

• 研究課題/領域番号: 24500035
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
• 研究期間 (年度): 2012-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円); 2014年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2013年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2012年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
• キーワード: 形式手法 / モデル検査 / 形式仕様記述 / テスト / 車載ソフトウェア / 形式仕様

研究成果の概要

本研究では，複数の形式手法を統合し，システム開発の上流工程から下流工程までをシームレスに接続する手法を提案した．また，実際の車載オペレーティングシステムの事例に適用し，提案手法の有効性を示すことができた．車載オペレーティングシステムなどの組込みシステムでは，開発工程の一部に形式手法を適用し，検証を行うことが主流であった．一方で，我々は，仕様記述から実装のテストまで，シームレスに接続し，全行程をカバーすることができた．これにより，産業界における形式手法の採用が加速され，ソフトウェアの信頼性，安全性が向上することを期待している．

研究成果

• [雑誌論文] A Framework for Verifying the Conformance of Design to Its Formal Specifications (2015)
  • 著者名/発表者名: Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
  • 雑誌名: IEICE Transactions 巻: Vo.E-98-D, No.6
  • NAID: 130005072395
  • 査読あり / 謝辞記載あり
• [雑誌論文] Active Learning of Nondeterministic Finite State Machines (2013)
  • 著者名/発表者名: Warawoot Pacharoen, Toshiaki Aoki, Pattarasinee Bhattarakosol, and Athasit Surarerks
  • 雑誌名: Mathematical Problems in Engineering 巻: vol. 2013 ページ: 1-11
  • DOI: 10.1155/2013/373265
  • 査読あり
• [雑誌論文] Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking (2012)
  • 著者名/発表者名: Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E95.D 号: 7 ページ: 1882-1893
  • DOI: 10.1587/transinf.E95.D.1882
  • NAID: 10031024282
  • ISSN: 0916-8532, 1745-1361
  • 査読あり
• [雑誌論文] UMLに基づくRTOS設計検証のための環境自動生成法 (2012)
  • 著者名/発表者名: 矢竹健朗, 青木利晃
  • 雑誌名: 日本ソフトウェア科学会 学会誌 コンピュータソフトウェア 巻: Vo.29, No.3, ページ: 121-142
  • NAID: 130004549272
  • 査読あり
• [雑誌論文] On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification (2012)
  • 著者名/発表者名: Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
  • 雑誌名: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences 巻: E95.A 号: 9 ページ: 1451-1460
  • DOI: 10.1587/transfun.E95.A.1451
  • NAID: 10031142529
  • ISSN: 0916-8508, 1745-1337
  • 査読あり
• [学会発表] Large scale testing using computer clusters (2015)
  • 著者名/発表者名: Toshiaki Aoki
  • 学会等名: Static Analysis meets Runtime Verification, Shonan Meeting
  • 発表場所: 湘南国際村センター(神奈川県・葉山町)
  • 年月日: 2015-03-16 – 2015-03-19
  • 招待講演
• [学会発表] 車載オペレーティングシステムを対象としたモデル検査とテストによる正しさの確信手法 (2014)
  • 著者名/発表者名: 青木 利晃, 佐藤 信, 谷 充弘 , 矢竹 健朗, 岸 知二
  • 学会等名: 第21回ソフトウェア工学の基礎ワークショップ(ポスター発表)
  • 発表場所: 霧島国際ホテル(鹿児島県・霧島市)
  • 年月日: 2014-12-11 – 2014-12-13
• [学会発表] ISO26262における安全仕様のゴール木を用いた浅い形式化 (2014)
  • 著者名/発表者名: 青木 利晃，千葉 勇輝，松原 正裕，西 昌能，成沢 文雄
  • 学会等名: 第21回ソフトウェア工学の基礎ワークショップ(ポスター発表)
  • 発表場所: 鹿児島県霧島国際ホテル(鹿児島県・霧島市)
  • 年月日: 2014-12-11 – 2014-12-13
• [学会発表] Creating Confidence in the Correctness with formal methods and testing (2014)
  • 著者名/発表者名: Toshiaki Aoki
  • 学会等名: Integration of Formal Method and Testing for Model-Based Systems Engineering, Shonan Meeting
  • 発表場所: 湘南国際村センター(神奈川県・葉山町)
  • 年月日: 2014-12-01 – 2014-12-03
  • 招待講演
• [学会発表] Checking the Conformance of a Promela Design to Its Formal Specification in Event-B (2014)
  • 著者名/発表者名: Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
  • 学会等名: Third International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS)
  • 発表場所: Luxembourg
  • 年月日: 2014-11-06 – 2014-11-07
• [学会発表] A Spin-based Approach for Checking OSEK/VDX Applications (2014)
  • 著者名/発表者名: Haitao Zhang, Toshiaki Aoki, Yuki Chiba
  • 学会等名: Third International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS)
  • 発表場所: Luxembourg
  • 年月日: 2014-11-06
• [学会発表] Practical Application of Formal Methods to Automotive Systems (2014)
  • 著者名/発表者名: Toshiaki Aoki
  • 学会等名: Science and Practice of Engineering Trustworthy Cyber-Physical Systems, Shonan Meeting
  • 発表場所: 湘南国際村センター(神奈川県・葉山町)
  • 年月日: 2014-10-26 – 2014-10-30
  • 招待講演
• [学会発表] SMT-based Bounded Model Checking for OSEK/VDX Applications (2013)
  • 著者名/発表者名: Haitao Zhang, Toshiaki Aoki, Hsin-Hung Lin, Min Zhang, Yuki Chiba and Kenro Yatake
  • 学会等名: 20th Asia-Pacific Software Engineering Conference(APSEC)
  • 発表場所: バンコク，タイ
• [学会発表] Preserving correctness of requirements evolution through refinement in Event-B (2013)
  • 著者名/発表者名: Kriangkrai Traichaiyaporn and Toshiaki Aoki
  • 学会等名: 20th Asia-Pacific Software Engineering Conference(APSEC)
  • 発表場所: バンコク，タイ
• [学会発表] A Practical Study of Debugging using Model Checking (2013)
  • 著者名/発表者名: Hideto Ogawa, Makoto Ichii, Fumihiko Kumeno and Toshiaki Aoki
  • 学会等名: 20th Asia-Pacific Software Engineering Conference(APSEC)
  • 発表場所: バンコク，タイ
• [学会発表] An approach for checking OSEK/VDX applications (2013)
  • 著者名/発表者名: Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang and Hsin-Hung Lin
  • 学会等名: The 13th International Conference on Quality Software(QSIC)
  • 発表場所: 南京，中国
• [学会発表] Building A Body of Knowledge on Model Checking for Software Development (2013)
  • 著者名/発表者名: Kenji Taguchi, Hideaki Nishihara, Toshiaki Aoki, Fumihiro Kumeno, Koji Hayamizu, and Koichi Sinozaki
  • 学会等名: Annual International Computers, Software & Applications Conference (COMPSAC)
  • 発表場所: 京都
• [学会発表] Refinement Tree and Its Patterns: a Graphical Approach for Event-B (2013)
  • 著者名/発表者名: Kriangkrai Traichaiyaporn and Toshiaki Aoki
  • 学会等名: Second International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS)
  • 発表場所: クイーンズタウン，ニュージーランド
• [学会発表] An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol (2013)
  • 著者名/発表者名: Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake and Toshiaki Aoki
  • 学会等名: Second International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS)
  • 発表場所: クイーンズタウン，ニュージーランド
• [学会発表] POM/MCを用いた仮説ベースモデル検査デバッグ手法 (2013)
  • 著者名/発表者名: 小川秀人, 市井誠, 粂野文洋, 青木利晃
  • 学会等名: ソフトウェア工学の基礎ワークショップ
  • 発表場所: 石川
• [学会発表] Evaluation of Operational Vulnerability in Cloud Service Management using Model Checking (2013)
  • 著者名/発表者名: Shinji Kikuchi, Toshiaki Aoki
  • 学会等名: IEEE Seventh International Symposium on Service-Oriented System Engineering(SOSE)
  • 発表場所: Redwood City, USA
• [学会発表] A Variability Management Method for Software Configuration Files (2012)
  • 著者名/発表者名: Hiroaki Tanizaki, Toshiaki Aoki, Takuya Katayama
  • 学会等名: The 24th International Conference on Software Engineering and Knowledge Engineering(SEKE)
  • 発表場所: Redwood City, USA
• [学会発表] SMT-based Enumeration of Object Graphs from UML class diagrams (2012)
  • 著者名/発表者名: Kenro Yatake, Toshiaki Aoki
  • 学会等名: 5th International workshop UML and Formal Methods
  • 発表場所: Paris, France
• [学会発表] Faithfully Formalizing OSEK/VDX Operating System Specification (2012)
  • 著者名/発表者名: Dieu-Huong Vu, Toshiaki Aoki
  • 学会等名: third International Symposium on Information and Communication Technology(SoICT)
  • 発表場所: Ha Long Bay, Vietnam
• [学会発表] モデル検査とテストによる車載オペレーティングシステムのシームレスな検証 (2012)
  • 著者名/発表者名: 青木利晃, 佐藤信, 谷充弘, 矢竹健朗
  • 学会等名: 組込みシステムシンポジウム
  • 発表場所: 東京
• [学会発表] モデル検査ツールにより出力された反例に基づく誤り特定手法 (2012)
  • 著者名/発表者名: 陳適, 青木利晃
  • 学会等名: ソフトウェア工学の基礎ワークショップ
  • 発表場所: 大分
• [学会発表] モデル検査器により出力された反例に基づく誤り特定に関する研究 (2012)
  • 著者名/発表者名: 陳適, 青木利晃
  • 学会等名: 情報処理学会 第177回ソフトウェア工学研究会
  • 発表場所: 大阪
• [図書] Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods (2012)
  • 著者名/発表者名: Toshiaki Aoki, Kenji Taguchi
  • 総ページ数: 528
  • 出版者: Springer