@techreport{oai:ipsj.ixsq.nii.ac.jp:00158002,
 author = {須藤, 一輝 and 小野, 康一 and 深澤, 良彰 and Kazuki, Sudo and Kouichi, Ono and Yoshiaki, Fukazawa},
 issue = {20},
 month = {Mar},
 note = {UML による Web アプリケーションモデルをモデル検査系で形式検証する一手法を提案する．このような目的の既存手法では，モデル変換により時間オートマトンなどの形式表現を得てそれを検証するものがあるが，実際のソフトウェアモデルは規模と複雑さが大きいため，単純な変換では状態爆発により検証が現実的には不可能である．そこで，アプリケーションドメイン固有の機能や役割の情報をモデルに記述しておき，それを手がかりとして簡略化された時間オートマトンに変換することで状態数を削減する方法を提案する．その代償としてドメイン固有の性質のみが検証対象となるが，そのような性質はドメイン内のアプリケーション全般において共通に存在するので有用と考える．本稿では手法と適用事例について述べる．},
 title = {モデル変換によるドメイン固有性質の形式検証に関する研究},
 year = {2016}
}