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

被引:2
|
作者
Strnadel, Josef [1 ]
机构
[1] Brno Univ Technol, Ctr Excellence IT4Innovat, Fac Informat Technol, Bozetechova 2, Brno 61266, Czech Republic
关键词
Reliability; Model; Analysis; Fault tolerant; Stochastic timed automata; Statistical model checking; UPPAAL SMC; Fault; Hazard; Rate; AVAILABILITY;
D O I
10.1007/978-3-319-47166-2_11
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The paper presents a method for creation and analysis of reliability models by means of stochastic timed automata and statistical model checking approach available in the UPPAAL SMC tool; its application is expected in, but not limited to, the area of electronic systems. The method can be seen as an alternative to classical analytic approaches based on instruments such as fault-tree or Markov reliability models of the above-specified systems. By the means of the method, reliability analysis of systems can be facilitated even for adverse conditions such as inconstant failure (hazard) rate of system components, various fault scenarios or dependencies among components and/or faults. Moreover, the method is applicable to dynamic, evolvable/reconfigurable systems able to add, remove their components and/or change their parameters at run-time; last but not least, it can be utilized to analyze and study reliability in the context of further system parameters such as liveness, safety and/or timing, power and other, application-specific, constraints. A solution to the related problems is far beyond the scope of recent methods.
引用
收藏
页码:166 / 181
页数:16
相关论文
共 50 条
  • [31] Model checking timed automata with one or two clocks
    Laroussinie, F
    Markey, N
    Schnoebelen, P
    CONCUR 2004 - CONCURRENCY THEORY, PROCEEDINGS, 2004, 3170 : 387 - 401
  • [32] Model checking via reachability testing for timed automata
    Aceto, L
    Burgueno, A
    Larsen, KG
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 263 - 280
  • [33] Model Checking Weighted Integer Reset Timed Automata
    Lakshmi Manasa
    Shankara Narayanan Krishna
    Chinmay Jain
    Theory of Computing Systems, 2011, 48 : 648 - 679
  • [34] Durations and parametric model-checking in timed automata
    Bruyere, Veronique
    Dall'olio, Emmanuel
    Raskin, Jean-Francois
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
  • [35] Utility of Statistical Model Checking of Stochastic Hybrid Automata for Patient Controlled Analgesia
    Pranevicius, Henrikas
    Naujokaitis, Darius
    Pilkauskas, Vytautas
    Pranevicius, Osvaldas
    Pranevicius, Mindaugas
    ELEKTRONIKA IR ELEKTROTECHNIKA, 2017, 23 (06) : 10 - 18
  • [36] Model Checking Timed and Stochastic Properties with CSLTA
    Donatelli, Susanna
    Haddad, Serge
    Sproston, Jeremy
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2009, 35 (02) : 224 - 240
  • [37] Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
    Wozna-Szczesniak, Bozena
    Zbrzezny, Andrzej
    FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 553 - 568
  • [38] Checking ACTL* properties of discrete timed automata via bounded model checking
    Wozna, B
    Zbrzezny, A
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2003, 2791 : 18 - 33
  • [39] Deep random search for efficient model checking of timed automata
    Grosu, R.
    Huang, X.
    Smolka, S. A.
    Tan, W.
    Tripakis, S.
    COMPOSITION OF EMBEDDED SYSTEMS: SCIENTIFIC AND INDUSTRIAL ISSUES, 2007, 4888 : 111 - +
  • [40] Parameterized model checking of networks of timed automata with Boolean guards
    Spalazzi, Luca
    Spegni, Francesco
    THEORETICAL COMPUTER SCIENCE, 2020, 813 : 248 - 269