Research on Design Verification Process Using Model Checking

• Project/Area Number: 19500035
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: The University of Electro-Communications (2008); National Institute of Informatics (2007)
• Principal Investigator: TAHARA Yasuyuki The University of Electro-Communications, 大学院・情報システム学研究科, 准教授 (30390602)
• Co-Investigator(Kenkyū-buntansha): 本位田 真一 国立情報学研究所, アーキテクチャ科学研究系, 教授 (70332153)
• Project Period (FY): 2007 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2008: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000); Fiscal Year 2007: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
• Keywords: 計算機システム / 情報システム / ソフトウェア開発効率化・安定化 / ソフトウェア学 / ソフトウェア検証

Research Abstract

近年、ソフトウェアは大規模化、複雑化が進んでいることから、高信頼でかつ安全なソフトウェア設計を実施するために、モデル検査技術が有望視されている。本研究では、開発者に分かりやすい設計と、モデル検査に必要な抽象的数学理論のギャップを縮めるために、既存技術であるTemplate Semantics をベースとした、形式モデルの意味論を参照・変更可能な設計モデル検証プロセスを考案し、そのプロセスに基づく開発支援ツールのプロトタイプを開発した。

Research Products

• [Presentation] Education Course of Practical Model Checking (2008)
  • Author(s): Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, Shinichi Honiden
  • Organizer: First International Workshop on Formal Methods Education and Training
  • Place of Presentation: 北九州市(日本)
  • Year and Date: 2008-10-28
• [Presentation] 開発プロセスにおけるセキュリティ関心事の分離に向けて (2008)
  • Author(s): 田原康之, 吉岡信和, 田口研治, 海谷治彦, 本位田真一
  • Organizer: ウインターワークショップ2008・イン・道後
  • Place of Presentation: 松山市(日本)
  • Year and Date: 2008-01-24
• [Presentation] 開発プロセスにおけるセキュリティ関心事の分離に向けて (2008)
  • Author(s): 田原 康之、吉岡 信和、田口 研治、本位田 真一
  • Organizer: ウインターワークショップ2008・イン・道後
  • Place of Presentation: 愛媛大学
  • Year and Date: 2008-01-24
• [Book] SPINによる設計モデル検証 (2008)
  • Author(s): 吉岡信和、青木利晃、田原康之(著)、萩谷昌己(監修)、本位田真一(シリーズ監修)
  • Publisher: 近代科学社
• [Book] ソフトウェア科学基礎 (2008)
  • Author(s): 磯部祥尚、粂野文洋、櫻庭健年、田口研治、田原康之(著)、田中譲(監修)、本位田真一(シリーズ監修)
  • Publisher: 近代科学社
• [Book] SPINによる設計モデル検証 (2008)
  • Author(s): 吉岡 信和
  • Publisher: 近代科学社
• [Book] ソフトウェア科学基礎 (2008)
  • Author(s): 磯部 祥尚
  • Publisher: 近代科学社