%0 Book Section
%@holdercode {isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S}
%@resumeid 8JMKD3MGP5W/3C9JJB5
%X 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.
%@mirrorrepository urlib.net/www/2011/03.29.20.55
%E Cornélio, Márcio,
%E Roscoe, Bill,
%T Time performance formal evaluation of complex systems
%@isbn 978-331929472-8
%S Lecture Notes in Computer Science
%@electronicmailaddress valdivino.santiago@inpe.br
%@electronicmailaddress tahar@ece.concordia.ca
%@nexthigherunit 8JMKD3MGPCW/3ESGTTP
%@secondarytype PRE LI
%K 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.
%@usergroup self-uploading-INPE-MCTI-GOV-BR
%@usergroup simone
%B Formal Methods: Foundations and Applications
%@group LAC-CTE-INPE-MCTI-GOV-BR
%@secondarykey INPE--/
%2 sid.inpe.br/mtc-m21b/2016/04.11.17.30.57
%@affiliation Instituto Nacional de Pesquisas Espaciais (INPE)
%@affiliation Concordia University
%@versiontype publisher
%I Springer
%P 162-177
%4 sid.inpe.br/mtc-m21b/2016/04.11.17.30
%@documentstage not transferred
%D 2016
%V 9526
%@doi 10.1007/978-3-319-29473-5_10
%A Santiago Júnior, Valdivino Alexandre de,
%A Tahar, S.,
%@dissemination BNDEPOSITOLEGAL
%@area COMP
%3 valdivino_time.pdf