Under certain constraints the test case generation problem can be represented as a model checking problem, thus enabling the use of powerful model checking tools to perform the test case generation automatically. There are, however, several different model checking techniques, and to date there is little evidence and comparison on which of these techniques is best suited for test case generation. This paper presents the results of an evaluation of several different model checkers on a set of realistic formal speci- fications given in the SCR [21] notation. For each specifi- cation test cases are generated for a set of coverage criteria with each of the model checkers using different configurations. The evaluation shows that the best suited model checking technique and optimization very much depend on the specification that is used to generate test cases. However, from the experiments we can draw general conclusions about which optimizations are useful and which model checking technique is best suited for which type of model. Finally, we demonstrate that by combining several model checking techniques it is possible to significantly speed up test case generation and also achieve full test coverage for cases where none of the techniques by itself would succeed.

(2009). An Evaluation of Model Checkers for Specification Based Test Case Generation [conference presentation - intervento a convegno]. Retrieved from http://hdl.handle.net/10446/23387

An Evaluation of Model Checkers for Specification Based Test Case Generation

GARGANTINI, Angelo Michele
2009-01-01

Abstract

Under certain constraints the test case generation problem can be represented as a model checking problem, thus enabling the use of powerful model checking tools to perform the test case generation automatically. There are, however, several different model checking techniques, and to date there is little evidence and comparison on which of these techniques is best suited for test case generation. This paper presents the results of an evaluation of several different model checkers on a set of realistic formal speci- fications given in the SCR [21] notation. For each specifi- cation test cases are generated for a set of coverage criteria with each of the model checkers using different configurations. The evaluation shows that the best suited model checking technique and optimization very much depend on the specification that is used to generate test cases. However, from the experiments we can draw general conclusions about which optimizations are useful and which model checking technique is best suited for which type of model. Finally, we demonstrate that by combining several model checking techniques it is possible to significantly speed up test case generation and also achieve full test coverage for cases where none of the techniques by itself would succeed.
2009
Fraser, Gordon; Gargantini, Angelo Michele
File allegato/i alla scheda:
Non ci sono file allegati a questa scheda.
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/23387
Citazioni
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 12
social impact