WEKO3
アイテム
情報制御システム記述モデルの検証項目記述とSPINによる確認
https://ipsj.ixsq.nii.ac.jp/records/74106
https://ipsj.ixsq.nii.ac.jp/records/741066a72d2d8-dc22-406a-b6b3-9c29db0102c5
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SE11171010.pdf (376.2 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-03-07 | |||||||
| タイトル | ||||||||
| タイトル | 情報制御システム記述モデルの検証項目記述とSPINによる確認 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Verification Item Description of Information Control System Descriptive Model and Confirmation by SPIN | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 学生セッション：形式手法 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 茨城大学 | ||||||||
| 著者所属 | ||||||||
| 茨城工業高等専門学校 | ||||||||
| 著者所属 | ||||||||
| 茨城大学 | ||||||||
| 著者所属 | ||||||||
| 株式会社日立製作所 | ||||||||
| 著者所属 | ||||||||
| 株式会社日立製作所 | ||||||||
| 著者所属 | ||||||||
| 株式会社日立製作所 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Ibaraki University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Ibaraki National College of Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Ibaraki University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Hitachi Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Hitachi Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Hitachi Ltd. | ||||||||
| 著者名 |
柳, 翔太
小飼, 敬
上田, 賀一
大久保, 訓
高橋, 勇喜
中野, 利彦
× 柳, 翔太 小飼, 敬 上田, 賀一 大久保, 訓 高橋, 勇喜 中野, 利彦
|
|||||||
| 著者名(英) |
Shota, Yanagi
Kei, Kogai
Yoshikazu, Ueda
Satoshi, Okubo
Yuki, Takahashi
Toshihiko, Nakano
× Shota, Yanagi Kei, Kogai Yoshikazu, Ueda Satoshi, Okubo Yuki, Takahashi Toshihiko, Nakano
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | ソフトウェアの品質を保証するために，ソフトウェア検証を行う必要性が高まっている．そこで，振舞いを網羅的に検証するモデル検査を開発現場に導入することを考える．現在，情報制御システム記述モデルに対してモデル検査を実行する手法が提案されている．しかし，検証すべき事項の記述方法はまとまっていない．そのため，本研究では検証項目記述の定義を行い，検証項目の設計手法について検討した．また，モデル検査で検証する性質を表すLTL(Linear Temporal Logic)式に検証項目を変換するルールを定義した．モデル検査ツールを用いてこれらの有効性を確認した． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | The necessity to perform software verification is growing in order to guarantee the quality of software. Therefore we think that we introduce a model checking to verify the behavior cyclopaedically into the development field. A technique to execute a model checking for information control system descriptive model is suggested now. However, the description method of the matters which should be verified is not completed. Therefore we defined the verification item description in this study and examined the design technique of the verification item. In addition, we defined a rule to convert a verification item into LTL(Linear Temporal Logic) formula which expressed a property to verify by model checking. We confirmed these effective by using a model checking tool. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10112981 | |||||||
| 書誌情報 |
研究報告ソフトウェア工学（SE） 巻 2011-SE-171, 号 10, p. 1-8, 発行日 2011-03-07 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
