1. Identity statement | |
Reference Type | Conference Paper (Conference Proceedings) |
Site | mtc-m21b.sid.inpe.br |
Holder Code | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
Identifier | 8JMKD3MGP3W34P/3KA6F98 |
Repository | sid.inpe.br/mtc-m21b/2015/09.22.13.04 |
Last Update | 2015:09.22.13.05.41 (UTC) administrator |
Metadata Repository | sid.inpe.br/mtc-m21b/2015/09.22.13.04.52 |
Metadata Last Update | 2018:06.04.02.55.40 (UTC) administrator |
Secondary Key | INPE--PRE/ |
Citation Key | SantiagoJúniorTaha:2015:TiPeFo |
Title | Time performance formal evaluation of complex systems |
Year | 2015 |
Access Date | 2024, Mar. 28 |
Secondary Type | PRE CN |
Number of Files | 1 |
Size | 5484 KiB |
|
2. Context | |
Author | 1 Santiago Júnior, Valdivino Alexandre de 2 Tahar, Sofične |
Group | 1 LAC-CTE-INPE-MCTI-GOV-BR |
Affiliation | 1 Instituto Nacional de Pesquisas Espaciais (INPE) 2 Concordia University |
Author e-Mail Address | 1 valdivino.santiago@inpe.br 2 tahar@ece.concordia.ca |
Conference Name | Congresso Brasileirod e Software: Teoria e Prática |
Conference Location | Belo Horizonte, MG |
Date | 21-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 Stage | completed |
Transferable | 1 |
Content Type | External Contribution |
Abstract | 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 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. |
Area | COMP |
Arrangement | urlib.net > BDMCI > Fonds > Produçăo anterior ŕ 2021 > LABAC > Time performance formal... |
doc Directory Content | access |
source Directory Content | there are no files |
agreement Directory Content | |
|
4. Conditions of access and use | |
data URL | http://urlib.net/ibi/8JMKD3MGP3W34P/3KA6F98 |
zipped data URL | http://urlib.net/zip/8JMKD3MGP3W34P/3KA6F98 |
Language | en |
User Group | simone |
Reader Group | administrator simone |
Visibility | shown |
Read Permission | allow from all |
Update Permission | not transferred |
|
5. Allied materials | |
Mirror Repository | urlib.net/www/2011/03.29.20.55 |
Next Higher Units | 8JMKD3MGPCW/3ESGTTP |
Host Collection | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 |
|
6. Notes | |
Empty Fields | 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 schedulinginformation secondarydate secondarymark serieseditor session shorttitle sponsor subject targetfile tertiarymark tertiarytype type url versiontype volume |
|
7. Description control | |
e-Mail (login) | simone |
update | |
|