Statistical Model Checking for Priced Timed Automata

被引:25
|
作者
Bulychev, Peter [1 ]
David, Alexandre [1 ]
Larsen, Kim Guldstrand [1 ]
Legay, Axel [2 ,3 ]
Mikucionis, Marius [1 ]
Poulsen, Danny Bogsted [1 ]
Wang, Zheng [4 ]
机构
[1] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark
[2] INRIA, Rennes, France
[3] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark
[4] East China Normal Univ, Software Engn Inst, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China
来源
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2012年 / 85期
关键词
D O I
10.4204/EPTCS.85.1
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This paper offers a survey of UPPAAL-SMC, a major extension of the real-time verification tool UPPAAL. UPPAAL-SMC allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, UPPAAL-SMC relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. UPPAAL-SMC comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.
引用
收藏
页码:1 / 16
页数:16
相关论文
共 50 条
  • [21] Risk-Averse Model Predictive Control for Priced Timed Automata
    Anbarani, Mostafa Tavakkoli
    Balta, Efe C.
    Meira-Goes, Romulo
    Kovalenko, Ilya
    2023 AMERICAN CONTROL CONFERENCE, ACC, 2023, : 4332 - 4338
  • [22] Concavely-Priced Probabilistic Timed Automata
    Jurdzinski, Marcin
    Kwiatkowska, Marta
    Norman, Gethin
    Trivedi, Ashutosh
    CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, 2009, 5710 : 415 - +
  • [23] Model-checking timed automata with deadlines with Uppaal
    Gomez, Rodolfo
    FORMAL ASPECTS OF COMPUTING, 2013, 25 (02) : 289 - 318
  • [24] Partial order reduction for model checking of timed automata
    Minea, M
    CONCUR '99: CONCURRENCY THEORY, 1999, 1664 : 431 - 446
  • [25] Symbolic model checking of finite precision timed automata
    Yan, RJ
    Li, GY
    Tang, ZS
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2005, 2005, 3722 : 272 - 287
  • [26] Weighted Timed Automata: Model-Checking and Games
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 (01) : 3 - 17
  • [27] 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):
  • [28] 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
  • [29] Model Checking Weighted Integer Reset Timed Automata
    Manasa, Lakshmi
    Krishna, Shankara Narayanan
    Jain, Chinmay
    THEORY OF COMPUTING SYSTEMS, 2011, 48 (03) : 648 - 679
  • [30] 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