Automatic Analysis of Requirements Model with Algebraic Specification Techniques

• Project/Area Number: 20500042
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: National Institute of Informatics
• Principal Investigator: NAKAJIMA Shin National Institute of Informatics, アーキテクチャ科学研究系, 教授 (60350211)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2010)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2010: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2009: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2008: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: ソフトウェア工学 / ソフトウェア開発効率化・安定化 / 仕様記述・仕様検証

Research Abstract

Since it is said that even misusage of clients is what developers should be responsible for, the task of specifying what features the system provides becomes a major issue. According to Software Engineering, such a problem is to be resolved by checking of rigorous requirements models constructed at early stages of the development. In this research project, we investigated a new method of automated analysis of requirements models written in Event-B. The proposed method makes use of abstraction techniques, and provides a new correctness criteria complementary to existing methods,

Research Products

• [Journal Article] Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems (2010)
  • Author(s): Shin Nakajima, Masaki Ishiguro, Kazuyuki Tanaka
  • Journal Title: Proceedings of 8^<th> IFIP Workshop on Software Technology for Future Embedded and Ubiquitous Systems Pages: 83-94
  • Peer Reviewed
• [Journal Article] ソフトウェア品質確保の技術動向 (2010)
  • Author(s): 中島震
  • Journal Title: 自動車研究 Vol.32、No.10 Pages: 561-565
• [Journal Article] Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems (2010)
  • Author(s): S.Nakajima, M.Ishiguro, K.Tanaka
  • Journal Title: Proc.8^<th> IFIP SEUS 2010 Pages: 83-94
  • Peer Reviewed
• [Journal Article] ソフトウェア品質確保の技術動向 (2010)
  • Author(s): 中島震
  • Journal Title: 自動車研究 Volume: 32 Pages: 561-565
• [Journal Article] 形式手法の潮流:アーキテクチャへの関心 (2008)
  • Author(s): 中島震
  • Journal Title: システム/制御/情報 Vol.52、No.9 Pages: 310-315
• [Presentation] A Refinement Planning Sheet (2010)
  • Author(s): 中島震
  • Organizer: RODIN User and Developer Workshop 2010
  • Place of Presentation: デユッセルドルフ
  • Year and Date: 2010-09-15
• [Presentation] A Refinement Planning Sheet (2010)
  • Author(s): S.Nakajima
  • Organizer: RODIN Developer Workshop 2010
  • Place of Presentation: デユッセルドルフ
  • Year and Date: 2010-09-15
• [Presentation] Event-Bで書かれたシステム要求仕様の妥当性検査 (2010)
  • Author(s): 中島震
  • Organizer: 電子情報通信学会ソフトウェアサイエンス研究会
  • Place of Presentation: 旭川
  • Year and Date: 2010-08-07
• [Presentation] 検証モデリングの比較検討-組込みシステムの事例- (2010)
  • Author(s): 中島震、谷津、野中、佐原
  • Organizer: 電子情報通信学会コンカレント工学研究会
  • Place of Presentation: トヨタ中研(豊田市)
  • Year and Date: 2010-01-21
• [Presentation] RODIN Plug-in to Link Event-B with SPIN (2009)
  • Author(s): Thomas MULLER, 中島震
  • Organizer: 電子情報通信学会ソフトウェアサイエンス研究会
  • Place of Presentation: 北見工大(北見市)
  • Year and Date: 2009-08-07
• [Presentation] ソフトウェア工学からみたモデル検査法 (2009)
  • Author(s): 中島震
  • Organizer: 回路とシステム軽井沢ワークショップ
  • Place of Presentation: プリンスホテル(軽井沢)
  • Year and Date: 2009-04-20
• [Presentation] Abstraction Aided Model Checking of Modeling Notations (2009)
  • Author(s): Shin Nakajima
  • Organizer: JAIST 21世紀COE CafeOBJ/Maude Workshop
  • Place of Presentation: JAIST(能美市)(石川県)
  • Year and Date: 2009-02-25
• [Presentation] Abstraction Aided Model Checking for Validation of Event-B Descriptions (2009)
  • Author(s): Shin Nakajima, Hironobu Kuruma
  • Organizer: IM_FMT 2009
  • Place of Presentation: デユッセルドルフ
  • Year and Date: 2009-02-16
• [Presentation] Abstraction Aided Model Checking of Event-B Descriptions (2009)
  • Author(s): Shin NAKAJIMA
  • Organizer: IM_FMT 2009
  • Place of Presentation: デュッセルドルフ(ドイツ)
  • Year and Date: 2009-02-16
• [Presentation] Event-B仕様記述のモデル検査 (2008)
  • Author(s): 中島震
  • Organizer: 日本ソフトウェア科学会第25回大会
  • Place of Presentation: 東京大学(東京都)
  • Year and Date: 2008-09-11
• [Presentation] Event-Bデザインのモデル検査における抽象化 (2008)
  • Author(s): 中島震
  • Organizer: 情報処理学会ソフトウェア工学研究会
  • Place of Presentation: 情報処理学会(東京都)
  • Year and Date: 2008-06-20
• [Book] SPIN モデル検査入門 (2010)
  • Author(s): M.Ben-Ari(著)、中島震(監訳)、谷津弘一、野中哲、足立太郎(訳)
  • Total Pages: 241
  • Publisher: オーム社
• [Book] SPINモデル検査入門(翻訳書) (2010)
  • Author(s): 中島震(監訳)、谷津、野中、足立(訳)
  • Total Pages: 241
  • Publisher: オーム社
• [Book] ソフトウェア工学の基礎XVI (2009)
  • Author(s): 中島震、鷲崎弘宜(編)
  • Total Pages: 336
  • Publisher: 近代科学社
• [Book] SPINモデル検査 (2008)
  • Author(s): 中島震(著)
  • Total Pages: 238
  • Publisher: 近代科学社
• [Remarks] ホームページ等
  • URL: http://research.nii.ac.jp/~nkjm/
• [Remarks]
  • URL: http://research.nii.ac.jp/~nkjm/
• [Remarks]
  • URL: http://researchmap.jp/nkim/