@Article{PontesVéraAmbrVill:2014:CoMoCh,
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 = "29 mar. 2024"
}