@techreport{oai:ipsj.ixsq.nii.ac.jp:00090665,
 author = {張, 漢明 and 野呂, 昌満 and 沢田, 篤史 and 吉田, 敦 and 蜂巣, 吉成 and 横森, 励士 and Han-myung, Chang and Masami, Noro and Atsushi, Sawada and Atsushi, Yoshida and Yoshinari, Hachisu and Reishi, Yokomori},
 issue = {11},
 month = {Mar},
 note = {本研究の目的はソフトウェアアーキテクチャを中心とした実践的な記述法と検証法を確立することである．振舞い仕様と機能仕様及び詳細化関係に着目して，既存のモデル検査とテスティング技術を適切に適用するための検証モデルを提示する．本稿では単純な自動販売機を事例として，アーキテクチャ段階における仕様記述と検証例を示す．本検証モデルは，ソフトウェア開発者がアーキテクチャを記述及び検証するさいの実践的な指針となることを目指す．, We aim to establish practical specification and verification methods for architecture oriented soft-ware development. We pay attention to behavioral specifications, functional specifications and refinement relations, and propose verification models in order to apply existing model checking and testing technologies to the development systematically. In this paper, architectural specifications and verifications of a simple vending machine are presented as a case study. The verification models will be used as practical guidelines for architectural specifications and verifications.},
 title = {アーキテクチャ指向開発における形式手法の適用に関する考察},
 year = {2013}
}