Statistical model checking of stochastic component-based systems

被引：0
|
作者：
Zhang, Lianyi [1 ,2 ]
Lo, Kueiming [3 ]
Qing, Duzheng [1 ,2 ]
Wang, Weijing [1 ,2 ]
Yu, Lixin [1 ,2 ]
机构：
[1] Beijing Simulat Ctr, Sci & Technol Special Syst Simulat Lab, Beijing, Peoples R China
[2] Beijing Inst Elect Syst Engn, State Key Lab Intelligent Mfg Syst Technol, Beijing, Peoples R China
[3] Tsinghua Univ, Sch Software, Beijing, Peoples R China
来源：
JOURNAL OF STATISTICAL COMPUTATION AND SIMULATION | 2017年 / 87卷 / 13期
基金：
中国国家自然科学基金;
关键词：
Stochastic BIP component systems; bisimulation minimization; statistical model checking; probabilistic model checking; 68Q60; 68N30; 60J20;
D O I：
10.1080/00949655.2017.1320401
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
Behaviour-interaction-priority (BIP) is a component-based framework that supports the rigorous design of embedded systems. This paper discusses stochastic BIP (SBIP) component systems, which involve semantics-based Markov chain models. We develop a method to translate the systems from SBIP into the models specified in the PRISM language. A bisimulation minimization approach is proposed to overcome the problem of state-space explosion of model checking. Finally, to illustrate the effectiveness of the proposed methods, we discuss a case study involving clock synchronization protocols for statistical and probabilistic model checking.
引用
收藏
页码：2509 / 2525
页数：17
相关论文
共 50 条
  • [1] Optimized Symbolic Model Checking for Component-based Systems
    Zhang, Lianyi
    Meng, Qingdi
    Luo, Guiming
    [J]. 2014 IEEE 13TH INTERNATIONAL CONFERENCE ON COGNITIVE INFORMATICS & COGNITIVE COMPUTING (ICCI-CC), 2014, : 373 - 378
  • [2] Stochastic Contracts for Runtime Checking of Component-based Real-time Systems
    Nandi, Chandrakana
    Monot, Aurelien
    Oriol, Manuel
    [J]. 2015 18TH INTERNATIONAL ACM SIGSOFT SYMPOSIUM ON COMPONENT-BASED SOFTWARE ENGINEERING (CBSE), 2015, : 111 - 116
  • [3] Automatic checking of component protocols in component-based systems
    Zimmermann, Wolf
    Schaarschmidt, Michael
    [J]. SOFTWARE COMPOSITION, 2006, 4089 : 1 - 17
  • [4] Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
    Hufflen, Jean-Michel
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (178): : 33 - 46
  • [5] On statistical model checking of stochastic systems
    Sen, K
    Viswanathan, M
    Agha, G
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 266 - 280
  • [6] Model Checking of Control-User Component-Based Parametrised Systems
    Varekova, Pavlina
    Cerna, Ivana
    [J]. COMPONENT-BASED SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 5282 : 146 - 162
  • [7] A refinement checking based strategy for component-based systems evolution
    Dihego, Jose
    Sampaio, Augusto
    Oliveira, Marcel
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2020, 167
  • [8] Statistical Model Checking for Stochastic Hybrid Systems
    David, Alexandre
    Larsen, Kim G.
    Mikucionis, Marius
    Poulsen, Danny Bogsted
    Legay, Axel
    Sedwards, Sean
    Du, Dehui
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (92): : 122 - 136
  • [9] Model-Checking for the Functional Safety of Control Component-based Heterogeneous Embedded Systems
    Khalgui, Mohamed
    Hanisch, Hans-Michael
    Gharbi, Atef
    [J]. 2009 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION (EFTA 2009), 2009,
  • [10] Checking deadlock-freedom of parametric component-based systems
    Bozga, Marius
    Iosif, Radu
    Sifakis, Joseph
    [J]. JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2021, 119
12345