Resultado da Pesquisa
A expressão de busca foi <secondaryty pi and firstg DSS-ETE-INPE-MCTI-GOV-BR and y 2014 and dissemination websci>.
1 referência encontrada buscando em 15 dentre 15 sites.
Data e hora local de busca: 26/02/2021 17:21.
Área de identificação
Tipo de ReferênciaJournal Article
Sitemtc-m16d.sid.inpe.br
Código do Detentorisadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S
Identificador8JMKD3MGP7W/3CEUM48
Repositóriosid.inpe.br/mtc-m19/2012/08.15.16.22   (acesso restrito)
Última Atualização2012:08.15.16.25.18 administrator
Metadadossid.inpe.br/mtc-m19/2012/08.15.16.22.47
Última Atualização dos Metadados2021:02.11.21.04.56 administrator
Chave SecundáriaINPE--PRE/
DOI10.1007/s10664-012-9215-y
ISSN1382-3256
Chave de CitaçãoPontesVéraAmbrVill:2014:CoMoCh
TítuloContributions of model checking and CoFI methodology to the development of space embedded software
ProjetoCNPq (306259/2011-7).
Ano2014
MêsFeb.
Data de Acesso26 fev. 2021
Tipo de Trabalhojournal article
Número de Arquivos1
Tamanho593 KiB
Área de contextualização
Autor1 Pontes, Rodrigo Pastl
2 Véras, Paulo Claudino
3 Ambrosio, Ana Maria
4 Villani, Emília
Identificador de Curriculo1
2
3 8JMKD3MGP5W/3C9JGH7
Grupo1
2
3 DSS-ETE-INPE-MCTI-GOV-BR
Afiliação1 Instituto Tecnológico de Aeronáutica (ITA)
2 Instituto Tecnológico de Aeronáutica (ITA)
3 Instituto Nacional de Pesquisas Espaciais (INPE)
4 Instituto Tecnológico de Aeronáutica (ITA)
Endereço de e-Mail do Autor1 rpastl@gmail.com
2 pauloveras@gmail.com
3 ana.ambrosio@inpe.br
4 evillani@ita.br
Endereço de e-Mailmarcelo.pazos@inpe.br
RevistaEmpirical Software Engineering
Volume19
Número1
Páginas39-68
Tipo SecundárioPRE PI
Nota SecundáriaA1_ENGENHARIAS_III A2_CIÊNCIA_DA_COMPUTAÇÃO A2_ENGENHARIAS_IV
Histórico2012-08-15 16:33:22 :: marciana -> administrator :: 2012
2012-11-22 00:33:51 :: administrator -> marciana :: 2012
2012-12-14 12:21:36 :: marciana -> administrator :: 2012
2014-06-02 16:33:06 :: administrator :: 2012 -> 2014
2021-02-11 21:04:56 :: administrator -> marcelo.pazos@inpe.br :: 2014
Área de conteúdo e estrutura
É a matriz ou uma cópia?é a matriz
Estágio do Conteúdoconcluido
Transferível1
Tipo do ConteudoExternal Contribution
Tipo de Versãopublisher
Palavras-Chaveverification, model checking, model based testing, embedded software, Packet Utilization Standard (PUS), space application.
ResumoThe 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.
AreaETES
ArranjoBDMCI > Fonds > Produção > DIDSS > Contributions of model...
Conteúdo da Pasta sourcenão têm arquivos
Conteúdo da Pasta agreement
agreement.html 15/08/2012 13:22 1.0 KiB 
Área de condições de acesso e uso
Idiomaen
Grupo de Usuáriosadministrator
marcelo.pazos@inpe.br
marciana
Grupo de Leitoresadministrator
marcelo.pazos@inpe.br
Visibilidadeshown
Política de Arquivamentodenypublisher denyfinaldraft12
Permissão de Leituradeny from all and allow from 150.163
Permissão de Atualizaçãonão transferida
Área de fontes relacionadas
Repositório Espelhoiconet.com.br/banon/2006/11.26.21.31
Unidades Imediatamente Superiores8JMKD3MGPCW/446B2HE
DivulgaçãoWEBSCI; PORTALCAPES; SCOPUS.
Acervo Hospedeirosid.inpe.br/mtc-m19@80/2009/08.21.17.02
Área de notas
Campos Vaziosalternatejournal archivist callnumber copyholder copyright creatorhistory descriptionlevel format isbn label lineage mark nextedition notes orcid parameterlist parentrepositories previousedition previouslowerunit progress rightsholder secondarydate session shorttitle sponsor subject targetfile tertiarymark tertiarytype url
Área de controle da descrição
e-Mail (login)marcelo.pazos@inpe.br
atualizar