author = "Pontes, Rodrigo Pastl and V{\'e}ras, Paulo Claudino and Ambrosio, 
                         Ana Maria and Villani, Em{\'{\i}}lia",
          affiliation = "{Instituto Tecnol{\'o}gico de Aeron{\'a}utica (ITA)} and 
                         {Instituto Tecnol{\'o}gico de Aeron{\'a}utica (ITA)} and 
                         {Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Tecnol{\'o}gico de Aeron{\'a}utica (ITA)}",
                title = "Contributions of model checking and CoFI methodology to the 
                         development of space embedded software",
              journal = "Empirical Software Engineering",
                 year = "2014",
               volume = "19",
               number = "1",
                pages = "39--68",
                month = "Feb.",
             keywords = "verification, model checking, model based testing, embedded 
                         software, Packet Utilization Standard (PUS), space application.",
             abstract = "The role of embedded software in the last space accidents 
                         highlights the importance of verification and validation 
                         techniques for the development of space embedded software. In this 
                         context, this work analyses the contribution of two verification 
                         techniques applied to the onboard data handling software of space 
                         products. The first technique is model checking. The system is 
                         modeled by a set of timed automata and the verification of safety 
                         and liveness properties is performed using UPPAAL model checker. 
                         The verified model is then used to generate the embedded software. 
                         The second technique analyzed in this work is model based approach 
                         for the generation of test cases. The Conformance and Fault 
                         Injection (CoFI) testing methodology is used to guide the 
                         development of a set of Finite State Machine (FSM) models from the 
                         software specification. The test suite is automatically generated 
                         from the FSM models. The contributions of the two methodologies 
                         are analyzed based on the results provided by an experiment. Two 
                         software products are used as case study, each one implementing 
                         two services of the Packet Utilization Standard (PUS). These 
                         services represent the functionalities offered by a satellite 
                         onboard data handling computer. One of the products is developed 
                         with the aid of model checking, while the other is developed 
                         according to the practices currently used at the Instituto 
                         Nacional de Pesquisas Espaciais (INPE). Both software products are 
                         tested by the CoFI methodology. The experiment highlights the 
                         advantages and vulnerable points of model checking. It also 
                         demonstrates that the main contribution of CoFI testing 
                         methodology is to highlight problems related to situations that 
                         have not been considered in the software specification, such as 
                         the occurrence of inopportune events. This analysis helps to 
                         understand how different techniques can be integrated in the 
                         design of critical embedded software.",
                  doi = "10.1007/s10664-012-9215-y",
                  url = "http://dx.doi.org/10.1007/s10664-012-9215-y",
                 issn = "1382-3256",
             language = "en",
        urlaccessdate = "17 jan. 2021"