From Statecharts into Model Checking: A Hierarchy-based Translation and Specification Patterns Properties to Generate Test Cases

• Valdivino Alexandre de Santiago Júnior INPE
• Felipe Elias Costa da Silva INPE

Resumo

Complexity and notation of formal methods are still major impediments for a wider use of these mathematical-based approaches 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 behavioral 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 Interaction Testing algorithm. We also present a cost-effectiveness evaluation (quasiexperiment) to compare four different patterns/pattern scopes. Results indicate that the Precedence Chain (P precedes S, T) pattern with Global scope presents the best performance.

Palavras-chave: Statecharts, Specification Patterns System, Software Testing, Quasiexperiment, Model Checking