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 条
  • [1] Statistical Model Checking for Priced Timed Automata
    Bulychev, Peter
    David, Alexandre
    Larsen, Kim Guldstrand
    Legay, Axel
    Mikucionis, Marius
    Poulsen, Danny Bogsted
    Wang, Zheng
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (85): : 1 - 16
  • [2] Statistical Model Checking for Networks of Priced Timed Automata
    David, Alexandre
    Larsen, Kim G.
    Legay, Axel
    Mikucionis, Marius
    Poulsen, Danny Bogsted
    van Vliet, Jonas
    Wang, Zheng
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2011, 6919 : 80 - +
  • [3] Statistical model checking of Timed Rebeca models
    Jafari, Ali
    Khamespanah, Ehsan
    Kristinsson, Haukur
    Sirjani, Marjan
    Magnusson, Brynjar
    COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2016, 45 : 53 - 79
  • [4] TIMED AUTOMATA ROBUSTNESS ANALYSIS VIA MODEL CHECKING
    Bendik, Jaroslav
    Sencan, Ahmet
    Gol, Ebru Aydin
    Cerna, Ivana
    LOGICAL METHODS IN COMPUTER SCIENCE, 2022, 18 (03) : 12:1 - 12:32
  • [5] Model checking for probabilistic timed automata
    Norman, Gethin
    Parker, David
    Sproston, Jeremy
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (02) : 164 - 190
  • [6] Model checking for probabilistic timed automata
    Gethin Norman
    David Parker
    Jeremy Sproston
    Formal Methods in System Design, 2013, 43 : 164 - 190
  • [7] Verified Model Checking of Timed Automata
    Wimmer, Simon
    Lammich, Peter
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT I, 2018, 10805 : 61 - 78
  • [8] Model checking prioritized timed automata
    Lin, SW
    Hsiung, PA
    Huang, CH
    Chen, YR
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 370 - 384
  • [9] Timed Automata Based Model Checking of Timed Security Protocols
    Kurkowski, Miroslaw
    Penczek, Wojciech
    FUNDAMENTA INFORMATICAE, 2009, 93 (1-3) : 245 - 259
  • [10] From Timed Automata to Stochastic Hybrid Games Model Checking, Synthesis, Performance Analysis and Machine Learning
    Larsen, Kim G.
    Fahrenberg, Uli
    Legay, Axel
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2017, 50 : 60 - 103