@TechReport{SilvaSant:2017:TeSoVi,
               author = "Silva, Felipe Elias Costa da and Santiago J{\'u}nior, Valdivino 
                         Alexandre de",
                title = "Testes de software via model checking para sistemas espaciais 
                         cr{\'{\i}}ticos",
          institution = "Instituto Nacional de Pesquisas Espaciais",
                 year = "2017",
                 type = "RPQ",
              address = "S{\~a}o Jos{\'e} dos Campos",
                 note = "{Bolsa PIBIC/INPE/CNPq}",
             keywords = "software, model checking, sistemas espaciais.",
             abstract = "Testes de software e Model Checking (m{\'e}todo de 
                         Verifica{\c{c}}{\~a}o Formal) s{\~a}o processos/m{\'e}todos 
                         diferentes para assegurar a qualidade de sistemas de software. 
                         Para sistemas cr{\'{\i}}ticos, tais como sat{\'e}lites e 
                         aplica{\c{c}}{\~o}es de bal{\~o}es estratosf{\'e}ricos que o 
                         INPE desenvolve, a quest{\~a}o da qualidade {\'e} ainda mais 
                         relevante, pois um defeito no software pode ocasionar grandes 
                         perdas financeiras. Dado a busca exaustiva no espa{\c{c}}o de 
                         estados que Model Checking realiza, pesquisadores v{\^e}m 
                         propondo gerar casos de testes de software por meio de Model 
                         Checking. Nesse contexto, o racioc{\'{\i}}nio {\'e} interpretar 
                         os contraexemplos gerados pelos Model Checkers (ferramentas de 
                         software que possuem uma realiza{\c{c}}{\~a}o da teoria de Model 
                         Checking) como casos de teste. O principal desafio {\'e} 
                         for{\c{c}}ar o Model Checker a criar, sistematicamente, conjuntos 
                         de tais contraexemplos. Esse projeto de pesquisa possui tr{\^e}s 
                         objetivos espec{\'{\i}}ficos: a.) realizar a gera{\c{c}}{\~a}o 
                         de casos de teste de software a partir de Model Checking; b.) 
                         atualizar a metodologia e a ferramenta SOLIMVA com as 
                         solu{\c{c}}{\~o}es tecnol{\'o}gicas desenvolvidas no projeto; e 
                         c.) aplicar a nova vers{\~a}o da ferramenta e da metodologia 
                         SOLIMVA a software de sistema espacial cr{\'{\i}}tico em 
                         desenvolvimento no INPE. Esse relat{\'o}rio apresenta as 
                         atividades desenvolvidas no per{\'{\i}}odo de 01 de agosto de 
                         2015 a 13 de julho de 2017.",
          affiliation = "{Universidade Salesiana (UNISAL)} and {Instituto Nacional de 
                         Pesquisas Espaciais (INPE)}",
             language = "pt",
                pages = "42",
                  ibi = "8JMKD3MGP3W34R/42L26CL",
                  url = "http://urlib.net/ibi/8JMKD3MGP3W34R/42L26CL",
           targetfile = "silva_testes.pdf",
        urlaccessdate = "25 abr. 2024"
}