Fechar
Metadados

Área de identificação
Tipo de ReferênciaArtigo em Evento (Conference Proceedings)
Sitemtc-m21b.sid.inpe.br
Código do Detentorisadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S
Identificador8JMKD3MGP3W34P/3KA6F98
Repositóriosid.inpe.br/mtc-m21b/2015/09.22.13.04
Última Atualização2015:09.22.13.05.41 administrator
Metadadossid.inpe.br/mtc-m21b/2015/09.22.13.04.52
Última Atualização dos Metadados2018:06.04.02.55.40 administrator
Chave SecundáriaINPE--PRE/
Chave de CitaçãoSantiagoJúniorTaha:2015:TiPeFo
TítuloTime performance formal evaluation of complex systems
Ano2015
Data de Acesso20 abr. 2021
Número de Arquivos1
Tamanho5484 KiB
Área de contextualização
Autor1 Santiago Júnior, Valdivino Alexandre de
2 Tahar, Sofiène
Grupo1 LAC-CTE-INPE-MCTI-GOV-BR
Afiliação1 Instituto Nacional de Pesquisas Espaciais (INPE)
2 Concordia University
Endereço de e-Mail do Autor1 valdivino.santiago@inpe.br
2 tahar@ece.concordia.ca
Nome do EventoCongresso Brasileirod e Software: Teoria e Prática
Localização do EventoBelo Horizonte, MG
Data21-25 set.
Tipo SecundárioPRE CN
Histórico2015-09-22 13:04:52 :: simone -> administrator ::
2018-06-04 02:55:40 :: administrator -> simone :: 2015
Á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
ResumoFormal verification methods, such as Model Checking, have been used for addressing performance/dependability analysis of systems. Such formal methods have several advantages over traditional techniques aiming at performance/dependability analysis such as the use of a single computational technique for evaluation of any measure and all complex numerical computation steps are hidden to the user. This paper reports on the use of Probabilistic Model Checking for time performance evaluation of complex systems. We propose an approach, TPerP, that allows a professional to clearly address time performance analysis based on Continuous-Time Markov Chain (CTMC). Our approach takes into consideration several types of delay analyzes. We applied it to a balloonborne high energy astrophysics scientific experiment where we dealt with CTMCs that had around 30 million reachable states and 75 million transitions, and we concluded that the current definition used in the balloon system is inadequate in terms of performance.
AreaCOMP
ArranjoBDMCI > Fonds > Produção > LABAC > Time performance formal...
Conteúdo da Pasta sourcenão têm arquivos
Conteúdo da Pasta agreement
agreement.html 22/09/2015 10:04 1.0 KiB 
Área de condições de acesso e uso
URL dos dadoshttp://urlib.net/rep/8JMKD3MGP3W34P/3KA6F98
URL dos dados zipadoshttp://urlib.net/zip/8JMKD3MGP3W34P/3KA6F98
Idiomaen
Grupo de Usuáriossimone
Grupo de Leitoresadministrator
simone
Visibilidadeshown
Permissão de Leituraallow from all
Permissão de Atualizaçãonão transferida
Área de fontes relacionadas
Repositório Espelhourlib.net/www/2011/03.29.20.55
Unidades Imediatamente Superiores8JMKD3MGPCW/3ESGTTP
Acervo Hospedeirosid.inpe.br/mtc-m21b/2013/09.26.14.25.20
Área de notas
Campos Vaziosaccessionnumber archivingpolicy archivist booktitle callnumber copyholder copyright creatorhistory descriptionlevel dissemination doi e-mailaddress edition editor format isbn issn keywords label lineage mark nextedition notes numberofvolumes orcid organization pages parameterlist parentrepositories previousedition previouslowerunit progress project publisher publisheraddress resumeid rightsholder secondarydate secondarymark serieseditor session shorttitle sponsor subject targetfile tertiarymark tertiarytype type url versiontype volume
Área de controle da descrição
e-Mail (login)simone
atualizar 

Fechar