author = "Pinheiro, Arineiza C. and Sim{\~a}o, Adenilso and Ambrosio, Ana 
          affiliation = "Instituto de Ci{\^e}ncias Matem{\'a}ticas e de 
                         Computa{\c{c}}{\~a}o, USPS{\~a}o Carlos, SP, Brazil and 
                         Instituto de Ci{\^e}ncias Matem{\'a}ticas e de 
                         Computa{\c{c}}{\~a}o, USPS{\~a}o Carlos, SP, Brazil and 
                         {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                title = "FSM-based test case generation methods applied to test the 
                         communication software on board the ITASAT university satellite: A 
                         case study",
              journal = "Journal of Aerospace Technology and Management",
                 year = "2014",
               volume = "6",
               number = "4",
                pages = "447--461",
             keywords = "Application programs, Finite automata, Logic circuits, Model 
                         checking, Modular construction, Satellites, Testing, Communication 
                         modules, Communication software, Critical software, Model based 
                         testing, Satellite applications, Software behavior, Test case 
                         generation, Testing methodology, Software testing.",
             abstract = "The software in satellite applications has become increasingly 
                         larger, more complex and more integrated, so its verification and 
                         validation require exploration of new approaches. In this paper we 
                         present a Model-Based Testing (MBT) approach applied to the 
                         Communication Module of the ITASAT-1 university satellite. The 
                         models are Finite State Machines (FSM) representing the software 
                         behavior. In order to manage the difficulties to model the 
                         software behavior the approach employs the Conformance and Fault 
                         Injection (CoFI) testing methodology associated with the 
                         JPlavisFSM tool in the real context of a satellite's critical 
                         software. The former advises the modularization of the modelling 
                         into different types of behavior into different FSMs, while the 
                         latter integrates several FSM-based methods to derive test cases, 
                         provides facilities to design and to check properties of the 
                         models and computes metrics. The main result of this case study 
                         was the evaluation of the drawbacks on the design of the testing 
                         models supported by CoFI and JPlavisFSM. The models, test sets, 
                         metrics with the application of our approach applied to the 
                         Communication Module are presented. The paper discusses the 
                         benefits as well as the points requiring new researches.",
                  doi = "10.5028/jatm.v6i4.369",
                  url = "http://dx.doi.org/10.5028/jatm.v6i4.369",
                 issn = "1984-9648",
                label = "scopus 2015-01 PinheiroSim{\~A}Ambr:2014:CaSt",
             language = "en",
           targetfile = "369-2213-1-PB.pdf",
        urlaccessdate = "30 nov. 2020"