Bounded model checking for GSMP models of stochastic real-time systems

被引:0
|
作者
Alur, Rajeev [1 ]
Bernadsky, Mikhail [1 ]
机构
[1] Univ Penn, Dept Informat & Comp Sci, Philadelphia, PA 19104 USA
关键词
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Model checking is a popular algorithmic verification technique for checking temporal requirements of mathematical models of systems. In this paper, we consider the problem of verifying bounded reachability properties of stochastic real-time systems modeled as generalized semi-Markov processes (GSMP). While GSMPs is a rich model for stochastic systems widely used in performance evaluation, existing model checking algorithms are applicable only to subclasses such as discrete-time or continuous-time Markov chains. The main contribution of the paper is an algorithm to compute the probability that a given GSMP satisfies a property of the form "can the system reach a target before time T within k discrete events, while staying within a set of safe states". For this, we show that the probability density function for the remaining firing times of different events in a GSMP after k discrete events can be effectively partitioned into finitely many regions and represented by exponentials and polynomials. We report on illustrative examples and their analysis using our techniques.
引用
收藏
页码:19 / 33
页数:15
相关论文
共 50 条
  • [31] Approximate Model Checking of Real-time Systems for Linear Duration Invariants
    Choe, Changil
    Han, Song
    Dang Van Hung
    2012 INTERNATIONAL CONFERENCE ON APPLIED INFORMATICS AND COMMUNICATION (ICAIC 2012), 2013, : 16 - 21
  • [32] Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems
    Courcoubetis, C
    Tripakis, S
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 183 - 219
  • [33] Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    PRIMA 2016: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2016, 9862 : 149 - 167
  • [34] Spatio-temporal model checking for mobile real-time systems
    Quesel, Jan-David
    Schaefer, Andreas
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2006, 2006, 4281 : 347 - 361
  • [35] Combined formal refinement and model checking for real-time systems verification
    Krupp, A
    Mueller, W
    Oliver, I
    LANGUAGES FOR SYSTEM SPECIFICATION: SELECTED CONTRIBUTIONS ON UML, SYSTEMC, SYSTEM VERILOG, MIXED-SIGNAL SYSTEMS, AND PROPERTY SPECIFICATION FROM FDL'03, 2004, : 301 - 314
  • [36] PRTS: An Approach for Model Checking Probabilistic Real-Time Hierarchical Systems
    Sun, Jun
    Liu, Yang
    Song, Songzheng
    Dong, Jin Song
    Li, Xiaohong
    FORMAL METHODS AND SOFTWARE ENGINEERING, 2011, 6991 : 147 - +
  • [37] Scheduling analysis based on model checking for multiprocessor real-time systems
    Karamti, Walid
    Mahfoudhi, Adel
    JOURNAL OF SUPERCOMPUTING, 2014, 68 (03): : 1604 - 1629
  • [38] Scheduling analysis based on model checking for multiprocessor real-time systems
    Walid Karamti
    Adel Mahfoudhi
    The Journal of Supercomputing, 2014, 68 : 1604 - 1629
  • [39] Symbolic model checking for event-driven real-time systems
    Yang, J
    Mok, AK
    Wang, F
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (02): : 386 - 412
  • [40] Model checking real-time component based systems with blackbox testing
    Van Hung, D
    Anh, BV
    11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Proceedings, 2005, : 76 - 79