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

• 研究課題/領域番号: 20500042
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 国立情報学研究所
• 研究代表者: 中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
• 研究期間 (年度): 2008 – 2010
• 研究課題ステータス: 完了 (2010年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2010年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2009年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円); 2008年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
• キーワード: ソフトウェア工学 / ソフトウェア開発効率化・安定化 / 仕様記述・仕様検証

研究概要

「利用者の誤使用も製造者の責任」、といわれ、どのような機能を提供すべきかを決める作業が大きな課題になっている。この問題に対して、開発の初期段階で作成する要求モデルの検査を行う方法がある。本研究課題では、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
• [雑誌論文] Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems (2010)
  • 著者名/発表者名: S.Nakajima, M.Ishiguro, K.Tanaka
  • 雑誌名: Proc.8^<th> IFIP SEUS 2010 ページ: 83-94
  • 査読あり
• [雑誌論文] ソフトウェア品質確保の技術動向 (2010)
  • 著者名/発表者名: 中島震
  • 雑誌名: 自動車研究 巻: 32 ページ: 561-565
• [雑誌論文] 形式手法の潮流:アーキテクチャへの関心 (2008)
  • 著者名/発表者名: 中島震
  • 雑誌名: システム/制御/情報 Vol.52、No.9 ページ: 310-315
• [学会発表] A Refinement Planning Sheet (2010)
  • 著者名/発表者名: 中島震
  • 学会等名: RODIN User and Developer Workshop 2010
  • 発表場所: デユッセルドルフ
  • 年月日: 2010-09-15
• [学会発表] A Refinement Planning Sheet (2010)
  • 著者名/発表者名: S.Nakajima
  • 学会等名: RODIN Developer Workshop 2010
  • 発表場所: デユッセルドルフ
  • 年月日: 2010-09-15
• [学会発表] Event-Bで書かれたシステム要求仕様の妥当性検査 (2010)
  • 著者名/発表者名: 中島震
  • 学会等名: 電子情報通信学会ソフトウェアサイエンス研究会
  • 発表場所: 旭川
  • 年月日: 2010-08-07
• [学会発表] 検証モデリングの比較検討-組込みシステムの事例- (2010)
  • 著者名/発表者名: 中島震、谷津、野中、佐原
  • 学会等名: 電子情報通信学会コンカレント工学研究会
  • 発表場所: トヨタ中研(豊田市)
  • 年月日: 2010-01-21
• [学会発表] RODIN Plug-in to Link Event-B with SPIN (2009)
  • 著者名/発表者名: Thomas MULLER, 中島震
  • 学会等名: 電子情報通信学会ソフトウェアサイエンス研究会
  • 発表場所: 北見工大(北見市)
  • 年月日: 2009-08-07
• [学会発表] ソフトウェア工学からみたモデル検査法 (2009)
  • 著者名/発表者名: 中島震
  • 学会等名: 回路とシステム軽井沢ワークショップ
  • 発表場所: プリンスホテル(軽井沢)
  • 年月日: 2009-04-20
• [学会発表] Abstraction Aided Model Checking of Modeling Notations (2009)
  • 著者名/発表者名: Shin Nakajima
  • 学会等名: JAIST 21世紀COE CafeOBJ/Maude Workshop
  • 発表場所: JAIST(能美市)(石川県)
  • 年月日: 2009-02-25
• [学会発表] Abstraction Aided Model Checking for Validation of Event-B Descriptions (2009)
  • 著者名/発表者名: Shin Nakajima, Hironobu Kuruma
  • 学会等名: IM_FMT 2009
  • 発表場所: デユッセルドルフ
  • 年月日: 2009-02-16
• [学会発表] Abstraction Aided Model Checking of Event-B Descriptions (2009)
  • 著者名/発表者名: Shin NAKAJIMA
  • 学会等名: IM_FMT 2009
  • 発表場所: デュッセルドルフ(ドイツ)
  • 年月日: 2009-02-16
• [学会発表] Event-B仕様記述のモデル検査 (2008)
  • 著者名/発表者名: 中島震
  • 学会等名: 日本ソフトウェア科学会第25回大会
  • 発表場所: 東京大学(東京都)
  • 年月日: 2008-09-11
• [学会発表] Event-Bデザインのモデル検査における抽象化 (2008)
  • 著者名/発表者名: 中島震
  • 学会等名: 情報処理学会ソフトウェア工学研究会
  • 発表場所: 情報処理学会(東京都)
  • 年月日: 2008-06-20
• [図書] SPIN モデル検査入門 (2010)
  • 著者名/発表者名: M.Ben-Ari(著)、中島震(監訳)、谷津弘一、野中哲、足立太郎(訳)
  • 総ページ数: 241
  • 出版者: オーム社
• [図書] SPINモデル検査入門(翻訳書) (2010)
  • 著者名/発表者名: 中島震(監訳)、谷津、野中、足立(訳)
  • 総ページ数: 241
  • 出版者: オーム社
• [図書] ソフトウェア工学の基礎XVI (2009)
  • 著者名/発表者名: 中島震、鷲崎弘宜(編)
  • 総ページ数: 336
  • 出版者: 近代科学社
• [図書] SPINモデル検査 (2008)
  • 著者名/発表者名: 中島震(著)
  • 総ページ数: 238
  • 出版者: 近代科学社
• [備考] ホームページ等
  • URL: http://research.nii.ac.jp/~nkjm/
• [備考]
  • URL: http://research.nii.ac.jp/~nkjm/
• [備考]
  • URL: http://researchmap.jp/nkim/