Close
Metadata

1. Identity statement
Reference TypeBook Section
Sitemtc-m21b.sid.inpe.br
Holder Codeisadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S
Identifier8JMKD3MGP3W34P/3LG2USB
Repositorysid.inpe.br/mtc-m21b/2016/04.11.17.30   (restricted access)
Last Update2016:12.29.15.07.03 (UTC) administrator
Metadata Repositorysid.inpe.br/mtc-m21b/2016/04.11.17.30.57
Metadata Last Update2018:06.04.02.40.41 (UTC) administrator
Secondary KeyINPE--/
DOI10.1007/978-3-319-29473-5_10
ISBN978-331929472-8
Citation KeySantiagoJúniorTaha:2016:TiPeFo
TitleTime performance formal evaluation of complex systems
Year2016
Access Date2024, Apr. 20
Secondary TypePRE LI
Number of Files1
Size580 KiB
2. Context
Author1 Santiago Júnior, Valdivino Alexandre de
2 Tahar, S.
Resume Identifier1 8JMKD3MGP5W/3C9JJB5
Group1 LAC-CTE-INPE-MCTI-GOV-BR
Affiliation1 Instituto Nacional de Pesquisas Espaciais (INPE)
2 Concordia University
Author e-Mail Address1 valdivino.santiago@inpe.br
2 tahar@ece.concordia.ca
EditorCornélio, Márcio
Roscoe, Bill
Book TitleFormal Methods: Foundations and Applications
PublisherSpringer
Volume9526
Pages162-177
Series TitleLecture Notes in Computer Science
History (UTC)2016-04-11 17:31:25 :: simone -> administrator :: 2016
2018-06-04 02:40:41 :: administrator -> simone :: 2016
3. Content and structure
Is the master or a copy?is the master
Content Stagecompleted
Transferable1
Content TypeExternal Contribution
Version Typepublisher
KeywordsAstrophysics
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
AbstractFormal 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.
AreaCOMP
Arrangementurlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > Time performance formal...
doc Directory Contentaccess
source Directory Contentthere are no files
agreement Directory Content
agreement.html 11/04/2016 14:30 1.9 KiB 
4. Conditions of access and use
Languageen
Target Filevaldivino_time.pdf
User Groupself-uploading-INPE-MCTI-GOV-BR
simone
Visibilityshown
Read Permissiondeny from all and allow from 150.163
Update Permissionnot transferred
5. Allied materials
Mirror Repositoryurlib.net/www/2011/03.29.20.55
Next Higher Units8JMKD3MGPCW/3ESGTTP
DisseminationBNDEPOSITOLEGAL
Host Collectionsid.inpe.br/mtc-m21b/2013/09.26.14.25.20
6. Notes
Empty Fieldsarchivingpolicy 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. Description control
e-Mail (login)simone
update 


Close