SBIP 2.0: Statistical Model Checking Stochastic Real-Time Systems

被引：19
|
作者：
Mediouni, Braham Lotfi [1 ]
Nouri, Ayoub [1 ]
Bozga, Marius [1 ]
Dellabani, Mahieddine [1 ]
Legay, Axel [2 ]
Bensalem, Saddek [1 ]
机构：
[1] Univ Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, F-38000 Grenoble, France
[2] INRIA, Rennes, France
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2018) | 2018年 / 11138卷
基金：
欧盟地平线“2020”; 英国工程与自然科学研究理事会;
关键词：
D O I：
10.1007/978-3-030-01090-4_33
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents a major new release of SBIP, an extensible statistical model checker for Metric (MTL) and Linear-time Temporal Logic (LTL) properties on respectively Generalized Semi-Markov Processes (GSMP), Continuous-Time (CTMC) and Discrete-Time Markov Chain (DTMC) models. The newly added support for MTL, GSMPs, CTMCs and rare events allows to capture both real-time and stochastic aspects, allowing faithful specification, modeling and analysis of real-life systems. SBIP is redesigned as an IDE providing project management, model edition, compilation, simulation, and statistical analysis.
引用
收藏
页码：536 / 542
页数：7
相关论文
共 50 条
  • [1] Statistical model checking QoS properties of systems with SBIP
    Nouri, Ayoub
    Bensalem, Saddek
    Bozga, Marius
    Delahaye, Benoit
    Jegourel, Cyrille
    Legay, Axel
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (02) : 171 - 185
  • [2] Statistical model checking QoS properties of systems with SBIP
    Ayoub Nouri
    Saddek Bensalem
    Marius Bozga
    Benoit Delahaye
    Cyrille Jegourel
    Axel Legay
    [J]. International Journal on Software Tools for Technology Transfer, 2015, 17 : 171 - 185
  • [3] A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models
    Bohlender, Dimitri
    Bruintjes, Harold
    Junges, Sebastian
    Katelaan, Jens
    Viet Yen Nguyen
    Noll, Thomas
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: SPECIALIZED TECHNIQUES AND APPLICATIONS, PT II, 2014, 8803 : 177 - 192
  • [4] Statistical Model Checking of Distributed Real-Time Actor Systems
    Nigro, Libero
    Sciammarella, Paolo F.
    [J]. 2017 IEEE/ACM 21ST INTERNATIONAL SYMPOSIUM ON DISTRIBUTED SIMULATION AND REAL TIME APPLICATIONS (DS-RT), 2017, : 188 - 195
  • [5] Bounded model checking for GSMP models of stochastic real-time systems
    Alur, Rajeev
    Bernadsky, Mikhail
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2006, 3927 : 19 - 33
  • [6] Statistical Model Checking for Real-Time Database Management Systems: A Case Study
    Cai, Simin
    Gallina, Barbara
    Nystrom, Dag
    Seceleanu, Cristina
    [J]. 2019 24TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2019, : 306 - 313
  • [7] Symbolic model checking of real-time systems
    Logothetis, G
    Schneider, K
    [J]. EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 214 - 223
  • [8] Local model checking for real-time systems
    Sokolsky, OV
    Smolka, SA
    [J]. COMPUTER AIDED VERIFICATION, 1995, 939 : 211 - 224
  • [9] SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS
    HENZINGER, TA
    NICOLLIN, X
    SIFAKIS, J
    YOVINE, S
    [J]. INFORMATION AND COMPUTATION, 1994, 111 (02) : 193 - 244
  • [10] On statistical model checking of stochastic systems
    Sen, K
    Viswanathan, M
    Agha, G
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 266 - 280
12345