author = "Santiago J{\'u}nior, Valdivino Alexandre de and Silva, Felipe 
                         Elias Costa da",
          affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Nacional de Pesquisas Espaciais (INPE)}",
                title = "From statecharts into model checking: A hierarchy-based 
                         translation and specification patterns properties to generate test 
            booktitle = "Proceedings...",
                 year = "2017",
         organization = "Brazilian Symposium on Systematic and Automated Software Testing, 
                         2. (SAST)",
             keywords = "Software Testing, Model Checking, Statecharts, Specification 
                         Patterns System, Quasiexperiment.",
             abstract = "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 
  conference-location = "Fortaleza, CE",
      conference-year = "18-19 Sept.",
                 isbn = "978-145035302-1",
             language = "en",
           targetfile = "santiago_from.pdf",
        urlaccessdate = "04 dez. 2020"