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 条
  • [21] Model-checking timed automata with deadlines with Uppaal
    Gomez, Rodolfo
    FORMAL ASPECTS OF COMPUTING, 2013, 25 (02) : 289 - 318
  • [22] Symbolic model checking of finite precision timed automata
    Yan, RJ
    Li, GY
    Tang, ZS
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2005, 2005, 3722 : 272 - 287
  • [23] Counterexample generation for probabilistic timed automata model checking
    Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    Jisuanji Yanjiu yu Fazhan, 2008, 10 (1638-1645):
  • [24] Weighted Timed Automata: Model-Checking and Games
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 (01) : 3 - 17
  • [25] Bounded Model Checking of an MITL Fragment for Timed Automata
    Kindermann, Roland
    Junttila, Tommi
    Niemela, Ilkka
    2013 13TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2013), 2013, : 216 - 225
  • [26] Model Checking Weighted Integer Reset Timed Automata
    Manasa, Lakshmi
    Krishna, Shankara Narayanan
    Jain, Chinmay
    THEORY OF COMPUTING SYSTEMS, 2011, 48 (03) : 648 - 679
  • [27] Model Checking Coordination of CPS Using Timed Automata
    Jiang, Kaiqiang
    Guan, Chunlin
    Wang, Jiahui
    Du, Dehui
    2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, : 258 - 263
  • [28] Model checking probabilistic timed automata in the presence of uncertainties
    Zhang, Junhua
    Huang, Zhiqiu
    Cao, Zining
    Xiao, Fangxiong
    Journal of Computational Information Systems, 2010, 6 (07): : 2231 - 2243
  • [29] On model-checking timed automata with stopwatch observers
    Brihaye, T
    Bruyére, V
    Raskin, JFO
    INFORMATION AND COMPUTATION, 2006, 204 (03) : 408 - 433
  • [30] Efficient encoding for bounded model checking of timed automata
    Chen, Zuxi
    Xu, Zhongwei
    Du, Junwei
    Mei, Meng
    Guo, Jing
    IEEJ TRANSACTIONS ON ELECTRICAL AND ELECTRONIC ENGINEERING, 2017, 12 (05) : 710 - 720