講演名 2013-07-26
UML要求分析モデルへのモデル検査技術適用による実現可能性の検証
青木 善貴, 小形 真平, 松浦 佐江子,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 高品質なソフトウェアを開発するためには,顧客による妥当性が確認された要求仕様を少ない手戻りで実装できるように,要求仕様の実現可能性を早期に検証することが重要である.このためには,要求仕様書が開発の初期段階でその適切さを保証できる検証可能な形式性を持つことが必要であるが,一般には不正確で曖昧な要求を分析している段階において,開発者が検証可能な要求仕様を定義することは困難である.本稿ではUMLを用いた開発において,早期に確認すべき基本的な性質の1つであるシステムの永続化対象データのライフサイクルをモデル検査技術を用いて保証しながら,要求仕様を洗練する手法を提案する.また,UMLの知識をもつ開発者がモデル検査技術の知識を持たなくても手法を利用できる支援ツールを開発した.
抄録(英) A key to success of developing high quality software products is to define valid and feasible requirements specification, so that it can produce high quality source codes with little extra development rework. To provide invariable services to all users at any time, the rules of CRUD on data life cycle are essential properties which persistent data should be met. Thus, such important properties should be verified at the start point of a development. UML2UPPAAL is a support tool of verifying such properties in which requirements specification written in UML is transformed into a finite automaton in UPPAAL A feature of UML2UPPAAL is that developers with knowledge of UML can receive benefit from a model checking technique UPPAAL without extra knowledge. This paper proposes a data life cycle verification method using a model checking technique UPPAAL focusing on CRUD operations at requirements analysis phase.
キーワード(和) UML / 要求仕様の実現可能性 / モデル検査 / 段階的形式化 / CRUD
キーワード(英) UML / Requirements Specification / Model Checking / Stepwise Refinement / CRUD
資料番号 SS2013-29,KBSE2013-29
発行日

研究会情報
研究会 KBSE
開催期間 2013/7/18(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) UML要求分析モデルへのモデル検査技術適用による実現可能性の検証
サブタイトル(和)
タイトル(英) Verification of Feasibility by Model Checking Techniques Applied to UML Requirements Analysis Model
サブタイトル(和)
キーワード(1)(和/英) UML / UML
キーワード(2)(和/英) 要求仕様の実現可能性 / Requirements Specification
キーワード(3)(和/英) モデル検査 / Model Checking
キーワード(4)(和/英) 段階的形式化 / Stepwise Refinement
キーワード(5)(和/英) CRUD / CRUD
第 1 著者 氏名(和/英) 青木 善貴 / Yoshitaka AOKI
第 1 著者 所属(和/英) 日本ユニシス株式会社:芝浦工業大学大学院理工学研究科
Nihon Unisys, Ltd.:Shibaura Institute of Technology
第 2 著者 氏名(和/英) 小形 真平 / Shinpei OGATA
第 2 著者 所属(和/英) 信州大学工学部
Shinshu University
第 3 著者 氏名(和/英) 松浦 佐江子 / Saeko MATSUURA
第 3 著者 所属(和/英) 芝浦工業大学大学院理工学研究科
Shibaura Institute of Technology
発表年月日 2013-07-26
資料番号 SS2013-29,KBSE2013-29
巻番号(vol) vol.113
号番号(no) 160
ページ範囲 pp.-
ページ数 6
発行日