@techreport{oai:ipsj.ixsq.nii.ac.jp:00074106,
 author = {柳, 翔太 and 小飼, 敬 and 上田, 賀一 and 大久保, 訓 and 高橋, 勇喜 and 中野, 利彦 and Shota, Yanagi and Kei, Kogai and Yoshikazu, Ueda and Satoshi, Okubo and Yuki, Takahashi and Toshihiko, Nakano},
 issue = {10},
 month = {Mar},
 note = {ソフトウェアの品質を保証するために，ソフトウェア検証を行う必要性が高まっている．そこで，振舞いを網羅的に検証するモデル検査を開発現場に導入することを考える．現在，情報制御システム記述モデルに対してモデル検査を実行する手法が提案されている．しかし，検証すべき事項の記述方法はまとまっていない．そのため，本研究では検証項目記述の定義を行い，検証項目の設計手法について検討した．また，モデル検査で検証する性質を表すLTL(Linear Temporal Logic)式に検証項目を変換するルールを定義した．モデル検査ツールを用いてこれらの有効性を確認した．, 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.},
 title = {情報制御システム記述モデルの検証項目記述とSPINによる確認},
 year = {2011}
}