| 1. Identificação | ||||
| Tipo de Referência | Capítulo de Livro (Book Section) | |||
| Site | mtc-m21b.sid.inpe.br | |||
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S | |||
| Identificador | 8JMKD3MGP3W34P/3LG2USB | |||
| Repositório | sid.inpe.br/mtc-m21b/2016/04.11.17.30 (acesso restrito) | |||
| Última Atualização | 2016:12.29.15.07.03 (UTC) administrator | |||
| Repositório de Metadados | sid.inpe.br/mtc-m21b/2016/04.11.17.30.57 | |||
| Última Atualização dos Metadados | 2018:06.04.02.40.41 (UTC) administrator | |||
| Chave Secundária | INPE--/ | |||
| DOI | 10.1007/978-3-319-29473-5_10 | |||
| ISBN | 978-331929472-8 | |||
| Chave de Citação | SantiagoJúniorTaha:2016:TiPeFo | |||
| Título | Time performance formal evaluation of complex systems  | |||
| Ano | 2016 | |||
| Data de Acesso | 19 abr. 2024 | |||
| Tipo Secundário | PRE LI | |||
| Número de Arquivos | 1 | |||
| Tamanho | 580 KiB | |||
| 2. Contextualização | ||||
| Autor | 1 Santiago Júnior, Valdivino Alexandre de 2 Tahar, S. | |||
| Identificador de Curriculo | 1 8JMKD3MGP5W/3C9JJB5 | |||
| Grupo | 1 LAC-CTE-INPE-MCTI-GOV-BR | |||
| Afiliação | 1 Instituto Nacional de Pesquisas Espaciais (INPE) 2 Concordia University | |||
| Endereço de e-Mail do Autor | 1 valdivino.santiago@inpe.br 2 tahar@ece.concordia.ca | |||
| Editor | Cornélio, Márcio Roscoe, Bill | |||
| Título do Livro | Formal Methods: Foundations and Applications | |||
| Editora (Publisher) | Springer | |||
| Volume | 9526 | |||
| Páginas | 162-177 | |||
| Título da Série | Lecture Notes in Computer Science | |||
| Histórico (UTC) | 2016-04-11 17:31:25 :: simone -> administrator :: 2016 2018-06-04 02:40:41 :: administrator -> simone :: 2016 | |||
| 3. Conteúdo e estrutura | ||||
| É a matriz ou uma cópia? | é a matriz | |||
| Estágio do Conteúdo | concluido | |||
| Transferível | 1 | |||
| Tipo do Conteúdo | External Contribution | |||
| Tipo de Versão | publisher | |||
| Palavras-Chave | Astrophysics Balloons Continuous time systems Markov processes Model checking Numerical methods Computational technique Continuous time Markov chain Formal verification methods Numerical computations Performance analysis Probabilistic model checking Scientific experiments Traditional techniques | |||
| Resumo | Formal 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 balloon-borne 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. | |||
| Área | COMP | |||
| Arranjo | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > Time performance formal... | |||
| Conteúdo da Pasta doc | acessar | |||
| Conteúdo da Pasta source | não têm arquivos | |||
| Conteúdo da Pasta agreement |
| |||
| 4. Condições de acesso e uso | ||||
| Idioma | en | |||
| Arquivo Alvo | valdivino_time.pdf | |||
| Grupo de Usuários | self-uploading-INPE-MCTI-GOV-BR simone | |||
| Visibilidade | shown | |||
| Permissão de Leitura | deny from all and allow from 150.163 | |||
| Permissão de Atualização | não transferida | |||
| 5. Fontes relacionadas | ||||
| Repositório Espelho | urlib.net/www/2011/03.29.20.55 | |||
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/3ESGTTP | |||
| Divulgação | BNDEPOSITOLEGAL | |||
| Acervo Hospedeiro | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 | |||
| 6. Notas | ||||
| Campos Vazios | archivingpolicy archivist callnumber city copyholder copyright creatorhistory descriptionlevel e-mailaddress edition format issn label lineage mark nextedition notes numberofvolumes orcid parameterlist parentrepositories previousedition previouslowerunit progress project readergroup rightsholder schedulinginformation secondarydate secondarymark serieseditor session shorttitle sponsor subject tertiarymark tertiarytype translator url | |||
| 7. Controle da descrição | ||||
| e-Mail (login) | simone | |||
| atualizar | ||||