Close

1. Identity statement
Reference TypeConference Paper (Conference Proceedings)
Sitemtc-m21b.sid.inpe.br
Holder Codeisadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S
Identifier8JMKD3MGP3W34P/3KA6F98
Repositorysid.inpe.br/mtc-m21b/2015/09.22.13.04
Last Update2015:09.22.13.05.41 (UTC) administrator
Metadata Repositorysid.inpe.br/mtc-m21b/2015/09.22.13.04.52
Metadata Last Update2018:06.04.02.55.40 (UTC) administrator
Secondary KeyINPE--PRE/
Citation KeySantiagoJúniorTaha:2015:TiPeFo
TitleTime performance formal evaluation of complex systems
Year2015
Access Date2024, Mar. 28
Secondary TypePRE CN
Number of Files1
Size5484 KiB
2. Context
Author1 Santiago Júnior, Valdivino Alexandre de
2 Tahar, Sofične
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
Conference NameCongresso Brasileirod e Software: Teoria e Prática
Conference LocationBelo Horizonte, MG
Date21-25 set.
History (UTC)2015-09-22 13:04:52 :: simone -> administrator ::
2018-06-04 02:55:40 :: administrator -> simone :: 2015
3. Content and structure
Is the master or a copy?is the master
Content Stagecompleted
Transferable1
Content TypeExternal Contribution
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 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
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 22/09/2015 10:04 1.0 KiB 
4. Conditions of access and use
data URLhttp://urlib.net/ibi/8JMKD3MGP3W34P/3KA6F98
zipped data URLhttp://urlib.net/zip/8JMKD3MGP3W34P/3KA6F98
Languageen
User Groupsimone
Reader Groupadministrator
simone
Visibilityshown
Read Permissionallow from all
Update Permissionnot transferred
5. Allied materials
Mirror Repositoryurlib.net/www/2011/03.29.20.55
Next Higher Units8JMKD3MGPCW/3ESGTTP
Host Collectionsid.inpe.br/mtc-m21b/2013/09.26.14.25.20
6. Notes
Empty Fieldsarchivingpolicy 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 schedulinginformation secondarydate secondarymark serieseditor session shorttitle sponsor subject targetfile tertiarymark tertiarytype type url versiontype volume
7. Description control
e-Mail (login)simone
update 


Close