Department of Computer Systems
Conference paperSTRNADEL Josef. On Creation and Analysis of Reliability Models by Means of Stochastic Timed Automata and Statistical Model Checking: Principle. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Cham: Springer International Publishing, 2016, pp. 166181. ISBN 9783319471662. ISSN 03029743. Available from: http://link.springer.com/chapter/10.1007/9783319471662_11  Publication language:  english 

Original title:  On Creation and Analysis of Reliability Models by Means of Stochastic Timed Automata and Statistical Model Checking: Principle 

Title (cs):  Tvorba a analýza spolehlivostních modelů prostředky stochastických časovaných automatů a statistického ověřování modelů: Princip 

Pages:  166181 

Proceedings:  Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques 

Conference:  7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) 

Series:  Lecture Notes in Computer Science, Vol. 9952 

Place:  Cham, CH 

Year:  2016 

URL:  http://link.springer.com/chapter/10.1007/9783319471662_11 

ISBN:  9783319471662 

Journal:  Lecture Notes in Computer Science, No. 10, DE 

ISSN:  03029743 

DOI:  10.1007/9783319471662_11 

Publisher:  Springer International Publishing 

URL:  [PDF] 

Keywords 

reliability, model, analysis, fault tolerant, FT, stochastic timed
automata, STA, statistical model checking, SMC, UPPAAL SMC, probability,
distribution, bathtub, fault, transient, permanent, intermittent, rate,
scenario, tripple modular redundancy, TMR 
Annotation 

The paper presents a method of creation and analysis of reliability models by means of stochastic timed automata (STA) and statistical model checking (SMC) approach available in the UPPAAL SMC tool; a special attention is paid there to reliabilty of electronic systems. The method can be seen as an alternative to classical analytic approaches based on instruments such as faulttree or Markov reliability models. Main goal of the paper is to show that  taking the advantage of the statistical model checking  the reliability analysis of systems can be facilitated even for adverse conditions such as inconstant failure (hazard) rate of inner system components. In the paper, basic terms and principles related to modeling and analysis of dynamic systems by means of the UPPAAL SMC tool are summarized, followed by a short demonstration of its practical applicability and summary of results achieved in the dependability area. 
BibTeX: 

@INPROCEEDINGS{
author = {Josef Strnadel},
title = {On Creation and Analysis of Reliability Models by Means of
Stochastic Timed Automata and Statistical Model Checking:
Principle},
pages = {166181},
booktitle = {Leveraging Applications of Formal Methods, Verification and
Validation: Foundational Techniques},
series = {Lecture Notes in Computer Science, Vol. 9952},
journal = {Lecture Notes in Computer Science},
number = {10},
year = {2016},
location = {Cham, CH},
publisher = {Springer International Publishing},
ISBN = {9783319471662},
ISSN = {03029743},
doi = {10.1007/9783319471662_11},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso88592?id=11168}
} 
