Clopper-Pearson Algorithms for Efficient Statistical Model Checking Estimation

被引:0
作者
Bu, Hao [1 ]
Sun, Meng [1 ]
机构
[1] Peking Univ, Sch Math Sci, Beijing 100871, Peoples R China
基金
国家重点研发计划;
关键词
Estimation; Model checking; Software algorithms; Testing; Numerical models; Costs; Computational modeling; Statistical model checking; formal methods; quantitative verification; SEQUENTIAL CONFIDENCE-INTERVALS; INEQUALITIES;
D O I
10.1109/TSE.2024.3392720
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Statistical model checking (SMC) is a simulation-based formal verification technique to deal with the scalability problem faced by traditional model checking. The main workflow of SMC is to perform iterative simulations. The number of simulations depends on users' requirement for the verification results, which can be very large if users require a high level of confidence and precision. Therefore, how to perform as fewer simulations as possible while achieving the same level of confidence and precision is one of the core problems of SMC. In this paper, we consider the estimation problem of SMC. Most existing statistical model checkers use the Okamoto bound to decide the simulation number. Although the Okamoto bound is sound, it is well known to be overly conservative. The simulation number decided by the Okamoto bound is usually much higher than it actually needs, which leads to a waste of time and computation resources. To tackle this problem, we propose an efficient, sound and lightweight estimation algorithm using the Clopper-Pearson confidence interval. We perform comprehensive numerical experiments and case studies to evaluate the performance of our algorithm, and the results show that our algorithm uses 40%-60% fewer simulations than the Okamoto bound. Our algorithm can be directly integrated into existing model checkers to reduce the verification time of SMC estimation problems.
引用
收藏
页码:1726 / 1746
页数:21
相关论文
共 39 条
[1]  
Agha K., 2018, ACM Trans. Model. Comput. Simul., V28, P1
[2]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[3]   Model-checking algorithms for continuous-time Markov chains [J].
Baier, C ;
Haverkort, B ;
Hermanns, H ;
Katoen, JP .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) :524-541
[4]  
Ballarini P., 2011, Proceedings of the 2011 Eighth International Conference on Quantitative Evaluation of Systems (QEST 2011), P143, DOI 10.1109/QEST.2011.24
[5]   HASL: A new approach for performance evaluation and model checking from concepts to experimentation [J].
Ballarini, Paolo ;
Barbot, Benoit ;
Duflot, Marie ;
Haddad, Serge ;
Pekergin, Nihal .
PERFORMANCE EVALUATION, 2015, 90 :53-77
[6]  
Bu, 2024, Zenodo, DOI 10.5281/ZENODO.10654358
[7]   An efficient statistical model checker for nondeterminism and rare events [J].
Budde, Carlos E. ;
D'Argenio, Pedro R. ;
Hartmanns, Arnd ;
Sedwards, Sean .
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2020, 22 (06) :759-780
[8]  
Bustan D, 2004, LECT NOTES COMPUT SC, V3114, P189
[9]   Sampling Adaptively using the Massart Inequality for Scalable Learning [J].
Chen, Jianhua ;
Xu, Jian .
2013 12TH INTERNATIONAL CONFERENCE ON MACHINE LEARNING AND APPLICATIONS (ICMLA 2013), VOL 2, 2013, :362-367
[10]   ON THE ASYMPTOTIC THEORY OF FIXED-WIDTH SEQUENTIAL CONFIDENCE-INTERVALS FOR THE MEAN [J].
CHOW, YS ;
ROBBINS, H .
ANNALS OF MATHEMATICAL STATISTICS, 1965, 36 (02) :457-462