%0 Conference Proceedings
%4 sid.inpe.br/mtc-m21b/2017/
%2 sid.inpe.br/mtc-m21b/2017/
%@isbn 978-145035302-1
%A Santiago Júnior, Valdivino Alexandre de,
%A Silva, Felipe Elias Costa da,
%@affiliation Instituto Nacional de Pesquisas Espaciais (INPE)
%@affiliation Instituto Nacional de Pesquisas Espaciais (INPE)
%@electronicmailaddress valdivino.santiago@inpe.br
%@electronicmailaddress felipe.eliascs@hotmail.com
%T From statecharts into model checking: A hierarchy-based translation and specification patterns properties to generate test cases
%B Brazilian Symposium on Systematic and Automated Software Testing, 2. (SAST)
%D 2017
%S Proceedings
%8 18-19 Sept.
%C Fortaleza, CE
%K Software Testing, Model Checking, Statecharts, Specification Patterns System, Quasiexperiment.
%X Complexity and notation of formal methods are still major impediments for a wider use of these mathematical-based ap- proaches in Software Engineering which include its adoption in software testing. While formal, Statecharts are relatively simple to use and many projects in different domains have been relying on them. In this paper, we present a hierarchy- based translation method, HiMoST, to generate software test cases via Model Checking. Starting with a behavio- ral modeling in Harel's Statecharts, we propose a method to translate from Statecharts into a general structure based on the NuSMV language, and we formalize CTL properties by means of specification patterns and a Combinatorial Interac- tion Testing algorithm. We also present a cost-effectiveness evaluation (quasiexperiment) to compare four different pat- terns/pattern scopes. Results indicate that the Precedence Chain (P precedes S, T) pattern with Global scope presents the best performance. © 2017 Association for Computing Machinery.
%@language en
%3 santiago_from.pdf