WEKO3
アイテム
コンテキストに注目したゴールモデルのモデル検査に関する研究
https://ipsj.ixsq.nii.ac.jp/records/191085
https://ipsj.ixsq.nii.ac.jp/records/191085e27d0452-8834-48ed-86ad-3052574e526e
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SES2018043.pdf (956.8 kB)
|
Copyright (c) 2018 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2018-08-29 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | コンテキストに注目したゴールモデルのモデル検査に関する研究 | |||||||||||||
| タイトル | ||||||||||||||
| 言語 | en | |||||||||||||
| タイトル | A Study of Model checking for Contextual Goal Models | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | jpn | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||||
| 資源タイプ | conference paper | |||||||||||||
| 著者所属 | ||||||||||||||
| 大阪大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 大阪大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 大阪大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 大阪大学 | ||||||||||||||
| 著者名 |
本田, 大雅
× 本田, 大雅
× 小島, 英春
× 中川, 博之
× 土屋, 達弘
|
|||||||||||||
| 論文抄録 | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | ゴール指向要求モデルは，ソフトウェア開発において顧客の要求を分析して仕様化するのに用いられる．そのゴールモデルに対して矛盾はないか，必要な要求は満たされているかなどを開発の初期段階で検証することで，開発工程の無駄な手戻りを防ぐことが期待できる．本研究では，ゴールモデルからステートマシン図に変換し，それをモデル検査器 SPIN で扱うことのできるモデルに変換することでモデル検査を行う．モデル検査を行うにあたっては，ゴールモデルで表現されたシステムのエージェントやアクタを 1 つのプロセスとして扱う．検査対象のエージェントやアクタが増加すれば，それに伴ってプロセス数も増加するため，状態数は爆発的に増加する．そのような状態爆発を緩和するために，対象とするシステムの周囲の環境を考慮して検証する機能を限定する．モデル検査では全ての状態を網羅し特性を検証するが，ある環境では必要とはされない機能が存在することが考えられ，それに対応する状態については検証する必要はない．そこで，システムの周囲の環境を表現するコンテキストに注目し，それを用いて機能の限定を行う．本研究では，ゴールモデルからモデル検査器用のモデルを作成し，モデル検査器 SPIN を用いてコンテキストを適用した場合としない場合について検証を行う．状態数，実行時間と利用メモリ量を比較し，全ての項目においてコンテキストを適用した場合はしない場合に比べ削減できることが確認できた． | |||||||||||||
| 書誌情報 |
ソフトウェアエンジニアリングシンポジウム2018論文集 巻 2018, p. 229-235, 発行日 2018-08-29 |
|||||||||||||
| 出版者 | ||||||||||||||
| 言語 | ja | |||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||
