講演抄録/キーワード |
講演名 |
2008-03-28 13:00
モデル検査器NuSMVを利用したテストケース自動生成 ○門野雅弥・土屋達弘・菊野 亨(阪大) DC2007-110 CPSY2007-106 |
抄録 |
(和) |
ソフトウェアの信頼性を向上させるための様々なテスト手法が存在する.本研究では,テスト手法の1つである状態遷移テストに着目する.
状態遷移テストは,ソフトウェアシステムの動作を状態図や状態遷移表で表したモデルに基づいて,すべての状態や遷移を網羅するようなテストを行う技術である.この手法を利用して手作業でテストケースを生成できるのは,状態数が非常に少なく遷移条件が単純な場合に限られるため,自動化手法が強く求められている.
そこで本研究では,状態図からすべての状態を網羅するテストセットを,モデル検査器NuSMVを利用して自動生成する手法を提案する.NuSMVの網羅的かつ強力な状態空間探索技術を用いることで,複雑なシステムに対しても漏れなくテストケースを生成することができる. |
(英) |
There are various testing methods of improving the reliability of software.In this study, we consider state transition testing.
State transition testing is one of the testing methods based on specifications described as statecharts or state transition tables.This testing method requires that testcases cover all states or all transitions.Manual testcase generation is feasible only when the number of system states is very small and transition conditions are very simple; thus an automatic method is required.
In this study, we propose a method that automatically generates testcases with the NuSMV model checker to cover all states.Using the exhaustive state space search method of the NuSMV model checker, we can generate testcases for complex systems in reasonable time. |
キーワード |
(和) |
ソフトウェアテスト / 状態遷移テスト / モデル検査 / NuSMV / / / / |
(英) |
Software testing / State transition testing / Model checking / NuSMV / / / / |
文献情報 |
信学技報, vol. 107, no. 559, DC2007-110, pp. 155-160, 2008年3月. |
資料番号 |
DC2007-110 |
発行日 |
2008-03-20 (DC, CPSY) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
DC2007-110 CPSY2007-106 |
研究会情報 |
研究会 |
DC CPSY IPSJ-SLDM IPSJ-EMB |
開催期間 |
2008-03-27 - 2008-03-28 |
開催地(和) |
屋久島 離島総合開発センター |
開催地(英) |
|
テーマ(和) |
組込技術とネットワークに関するワークショップ ETNET2008(コンピュータシステム研究会、情報処理学会システムLSI設計技術研究会、情報処理学会組込みシステム研究会共催) |
テーマ(英) |
|
講演論文情報の詳細 |
申込み研究会 |
DC |
会議コード |
2008-03-DC |
本文の言語 |
日本語 |
タイトル(和) |
モデル検査器NuSMVを利用したテストケース自動生成 |
サブタイトル(和) |
|
タイトル(英) |
Automatically Generating Testcases with the NuSMV Model Checker |
サブタイトル(英) |
|
キーワード(1)(和/英) |
ソフトウェアテスト / Software testing |
キーワード(2)(和/英) |
状態遷移テスト / State transition testing |
キーワード(3)(和/英) |
モデル検査 / Model checking |
キーワード(4)(和/英) |
NuSMV / NuSMV |
キーワード(5)(和/英) |
/ |
キーワード(6)(和/英) |
/ |
キーワード(7)(和/英) |
/ |
キーワード(8)(和/英) |
/ |
第1著者 氏名(和/英/ヨミ) |
門野 雅弥 / Masaya Kadono / カドノ マサヤ |
第1著者 所属(和/英) |
大阪大学 (略称: 阪大)
Osaka University (略称: Osaka Univ.) |
第2著者 氏名(和/英/ヨミ) |
土屋 達弘 / Tatsuhiro Tsuchiya / ツチヤ タツヒロ |
第2著者 所属(和/英) |
大阪大学 (略称: 阪大)
Osaka University (略称: Osaka Univ.) |
第3著者 氏名(和/英/ヨミ) |
菊野 亨 / Tohru Kikuno / キクノ トオル |
第3著者 所属(和/英) |
大阪大学 (略称: 阪大)
Osaka University (略称: Osaka Univ.) |
第4著者 氏名(和/英/ヨミ) |
/ / |
第4著者 所属(和/英) |
(略称: )
(略称: ) |
第5著者 氏名(和/英/ヨミ) |
/ / |
第5著者 所属(和/英) |
(略称: )
(略称: ) |
第6著者 氏名(和/英/ヨミ) |
/ / |
第6著者 所属(和/英) |
(略称: )
(略称: ) |
第7著者 氏名(和/英/ヨミ) |
/ / |
第7著者 所属(和/英) |
(略称: )
(略称: ) |
第8著者 氏名(和/英/ヨミ) |
/ / |
第8著者 所属(和/英) |
(略称: )
(略称: ) |
第9著者 氏名(和/英/ヨミ) |
/ / |
第9著者 所属(和/英) |
(略称: )
(略称: ) |
第10著者 氏名(和/英/ヨミ) |
/ / |
第10著者 所属(和/英) |
(略称: )
(略称: ) |
第11著者 氏名(和/英/ヨミ) |
/ / |
第11著者 所属(和/英) |
(略称: )
(略称: ) |
第12著者 氏名(和/英/ヨミ) |
/ / |
第12著者 所属(和/英) |
(略称: )
(略称: ) |
第13著者 氏名(和/英/ヨミ) |
/ / |
第13著者 所属(和/英) |
(略称: )
(略称: ) |
第14著者 氏名(和/英/ヨミ) |
/ / |
第14著者 所属(和/英) |
(略称: )
(略称: ) |
第15著者 氏名(和/英/ヨミ) |
/ / |
第15著者 所属(和/英) |
(略称: )
(略称: ) |
第16著者 氏名(和/英/ヨミ) |
/ / |
第16著者 所属(和/英) |
(略称: )
(略称: ) |
第17著者 氏名(和/英/ヨミ) |
/ / |
第17著者 所属(和/英) |
(略称: )
(略称: ) |
第18著者 氏名(和/英/ヨミ) |
/ / |
第18著者 所属(和/英) |
(略称: )
(略称: ) |
第19著者 氏名(和/英/ヨミ) |
/ / |
第19著者 所属(和/英) |
(略称: )
(略称: ) |
第20著者 氏名(和/英/ヨミ) |
/ / |
第20著者 所属(和/英) |
(略称: )
(略称: ) |
講演者 |
第1著者 |
発表日時 |
2008-03-28 13:00:00 |
発表時間 |
25分 |
申込先研究会 |
DC |
資料番号 |
DC2007-110, CPSY2007-106 |
巻番号(vol) |
vol.107 |
号番号(no) |
no.559(DC), no.558(CPSY) |
ページ範囲 |
pp.155-160 |
ページ数 |
6 |
発行日 |
2008-03-20 (DC, CPSY) |