@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00102886,
 author = {青木, 善貴 and 松浦, 佐江子 and Yoshitaka, Aoki and Saeko, Matsuura},
 book = {ソフトウェアエンジニアリングシンポジウム2014論文集},
 month = {Aug},
 note = {開発現場では不十分な要件定義や実装時のミス・誤解等により人手では発見困難な不具合が発生する．担当する要員により原因特定にかかる工数が著しく違うことは，開発プロジェクトの進捗の妨げになるため不具合原因を安定的に特定できる手法が必要である．本研究ではモデル検査の網羅的に要求される性質が満たされるかを自動検査する特性を利用して Java ソースコードに対して，仕様とソースコード間の振舞いの不一致の原因の特定を行う．, Software programs often include many defects that are not easy to detect because of the developers' mistakes, misunderstandings caused by the inadequate definition of requirements, and the complexity of the implementation. Due to the different skill levels of the testers, the significant increase in testing person-hours interferes with the progress of development projects. Therefore, it is for any non-specialized developer to identify the cause of the defects. Model checking has been favored as a technique to improve the reliability earlier in the software development process. In this paper, we propose a verification method in which a Java source code control sequence is converted into finite automata in order to detect the cause of defects by using the model-checking, which has an exhaustive checking mechanism.},
 pages = {212--213},
 publisher = {情報処理学会},
 title = {モデル検査を利用した仕様とソースコード間におけるシステムの振舞いの不一致発見},
 volume = {2014},
 year = {2014}
}