代数仕様を用いた要求モデルの自動検査に関する研究

2010 年度 研究成果報告書

• 研究課題/領域番号: 20500042
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 国立情報学研究所
• 研究代表者: 中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
• 研究期間 (年度): 2008 – 2010
• キーワード: ソフトウェア工学 / ソフトウェア開発効率化・安定化

研究概要

「利用者の誤使用も製造者の責任」、といわれ、どのような機能を提供すべきかを決める作業が大きな課題になっている。この問題に対して、開発の初期段階で作成する要求モデルの検査を行う方法がある。本研究課題では、Event-Bと呼ぶ手法で作成した要求モデルの正しさを自動検証する技術の研究を行った。考案した抽象化に基づく自動検査は、従来の検査方法と補完的な役割を果たす。正しさを検査する基準として新しい視点を導入できたといえる。

研究成果

• [雑誌論文] Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems (2010)
  • 著者名/発表者名: Shin Nakajima, Masaki Ishiguro, Kazuyuki Tanaka
  • 雑誌名: Proceedings of 8^<th> IFIP Workshop on Software Technology for Future Embedded and Ubiquitous Systems ページ: 83-94
  • 査読あり
• [雑誌論文] ソフトウェア品質確保の技術動向 (2010)
  • 著者名/発表者名: 中島震
  • 雑誌名: 自動車研究 Vol.32、No.10 ページ: 561-565
• [雑誌論文] 形式手法の潮流:アーキテクチャへの関心 (2008)
  • 著者名/発表者名: 中島震
  • 雑誌名: システム/制御/情報 Vol.52、No.9 ページ: 310-315
• [学会発表] A Refinement Planning Sheet (2010)
  • 著者名/発表者名: 中島震
  • 学会等名: RODIN User and Developer Workshop 2010
  • 発表場所: デユッセルドルフ
  • 年月日: 2010-09-15
• [学会発表] Event-Bで書かれたシステム要求仕様の妥当性検査 (2010)
  • 著者名/発表者名: 中島震
  • 学会等名: 電子情報通信学会ソフトウェアサイエンス研究会
  • 発表場所: 旭川
  • 年月日: 2010-08-07
• [学会発表] Abstraction Aided Model Checking for Validation of Event-B Descriptions (2009)
  • 著者名/発表者名: Shin Nakajima, Hironobu Kuruma
  • 学会等名: IM_FMT 2009
  • 発表場所: デユッセルドルフ
  • 年月日: 2009-02-16
• [図書] SPIN モデル検査入門 (2010)
  • 著者名/発表者名: M.Ben-Ari(著)、中島震(監訳)、谷津弘一、野中哲、足立太郎(訳)
  • 総ページ数: 241
  • 出版者: オーム社
• [図書] ソフトウェア工学の基礎XVI (2009)
  • 著者名/発表者名: 中島震、鷲崎弘宜(編)
  • 総ページ数: 336
  • 出版者: 近代科学社
• [図書] SPINモデル検査 (2008)
  • 著者名/発表者名: 中島震(著)
  • 総ページ数: 238
  • 出版者: 近代科学社
• [備考] ホームページ等
  • URL: http://research.nii.ac.jp/~nkjm/