WEKO3
アイテム
モデル検査を利用した仕様とソースコード間におけるシステムの振舞いの不一致発見
https://ipsj.ixsq.nii.ac.jp/records/102886
https://ipsj.ixsq.nii.ac.jp/records/102886cb0b967c-e87d-4291-a154-4406c6cbfe43
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 2014 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Symposium(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 2014-08-25 | |||||||
タイトル | ||||||||
タイトル | モデル検査を利用した仕様とソースコード間におけるシステムの振舞いの不一致発見 | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | Behavioral Inconsistency Detection between Source Code and Specification using Model Checking | |||||||
言語 | ||||||||
言語 | jpn | |||||||
キーワード | ||||||||
主題Scheme | Other | |||||||
主題 | ポスター論文 | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
資源タイプ | conference paper | |||||||
著者所属 | ||||||||
日本ユニシス株式会社/芝浦工業大学 | ||||||||
著者所属 | ||||||||
芝浦工業大学 | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Nihon Unisys ,Ltd. / Shibaura Institute of Technology | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Shibaura Institute of Technology | ||||||||
著者名 |
青木, 善貴
× 青木, 善貴
|
|||||||
著者名(英) |
Yoshitaka, Aoki
× Yoshitaka, Aoki
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 開発現場では不十分な要件定義や実装時のミス・誤解等により人手では発見困難な不具合が発生する.担当する要員により原因特定にかかる工数が著しく違うことは,開発プロジェクトの進捗の妨げになるため不具合原因を安定的に特定できる手法が必要である.本研究ではモデル検査の網羅的に要求される性質が満たされるかを自動検査する特性を利用して Java ソースコードに対して,仕様とソースコード間の振舞いの不一致の原因の特定を行う. | |||||||
論文抄録(英) | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 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. | |||||||
書誌情報 |
ソフトウェアエンジニアリングシンポジウム2014論文集 巻 2014, p. 212-213, 発行日 2014-08-25 |
|||||||
出版者 | ||||||||
言語 | ja | |||||||
出版者 | 情報処理学会 |