WEKO3
アイテム
CSPを用いた状態マシン図とシーケンス図の整合性検証
https://ipsj.ixsq.nii.ac.jp/records/97899
https://ipsj.ixsq.nii.ac.jp/records/978990e87bdf3-d9ac-425a-ac30-36cf3b99e203
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WWS2014021.pdf (207.1 kB)
|
Copyright (c) 2014 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2014-01-16 | |||||||
| タイトル | ||||||||
| タイトル | CSPを用いた状態マシン図とシーケンス図の整合性検証 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Consistency veri cation of state machine diagrams and a sequence diagram using CSP | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 形式手法 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 岡山県立大学 | ||||||||
| 著者所属 | ||||||||
| 岡山県立大学 | ||||||||
| 著者所属 | ||||||||
| 川崎医療福祉大学 | ||||||||
| 著者所属 | ||||||||
| 岡山県立大学 | ||||||||
| 著者所属 | ||||||||
| 岡山県立大学 | ||||||||
| 著者所属 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Okayama Prefectural University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Okayama Prefectural University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Kawasaki University of Medical Welfare | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Okayama Prefectural University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Okayama Prefectural University | ||||||||
| 著者名 |
横川, 智教
片山, 巧
宮崎, 仁
佐藤, 洋一郎
有本, 和民
× 横川, 智教 片山, 巧 宮崎, 仁 佐藤, 洋一郎 有本, 和民
|
|||||||
| 著者名(英) |
Tomoyuki, YOKOGAWA
Takumi, KATAYAMA
Hisashi, MIYAZAKI
Yoichiro, SATO
Kazutami, ARIMOTO
× Tomoyuki, YOKOGAWA Takumi, KATAYAMA Hisashi, MIYAZAKI Yoichiro, SATO Kazutami, ARIMOTO
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本稿では，UML の状態マシン図およびシーケンス図をプロセス代数形式のモデル記述言語であるCSP を用いて表現し，検証ツールFDR を用いて整合性検証を行う手法について示す．また，例題への適用実験を通して，整合性違反が存在する場合はそれを正しく検出できることを示している． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | We propose a method to detect consistency errors in UML state machine diagrams and sequence diagrams by representing the diagrams as CSP, which is a process algebra style notation. We use FDR model checker to verify the consistency relation between the diagrams. We show an application example of the method where the correctness of consistencyof example diagrams is checked. | |||||||
| 書誌情報 |
ウィンターワークショップ2014・イン・大洗 論文集 巻 2014, p. 41-42, 発行日 2014-01-16 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
