计算机科学 ›› 2017, Vol. 44 ›› Issue (Z6): 499-503.doi: 10.11896/j.issn.1002-137X.2017.6A.111
高婉玲,洪玫,杨秋辉,赵鹤
GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He
摘要： 近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响。主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境。选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算法、智能假设检验算法及蒙特卡罗算法。采用无线局域网协议验证和哲学家就餐问题的状态可达性验证为实例进行分析,使用PLASMA模型检测工具进行验证。实验结果表明,不同的统计算法在不同的环境中对模型检测的效率有不同的影响。序贯算法适用于状态可达性性质的验证,时间性能最优；智能假设检验算法与蒙特卡罗算法适合验证复杂模型。这一结论有助于在模型检测时对统计算法的选择,从而提高模型检测的效率。
| [1] YOUNES H L S,SIMMONS R G.Statistical probabilistic modelchecking with a focus on time-bounded properties[J].Information and Computation (JIC),2006,204(9):1368-1409. [2] ZULIANI P,PLATZER A,CLARKE E M.Bayesian statistical model checking with application to Stateflow/Simulink verification[J].Formal Methods in System Design,2010,3(2):243-252. [3] YOUNES H L S,KWIATKOWSKA M,NORMAN G,et al.Numerical vs.statistical probabilistic model checking[J].Software Tools for Technology Transfer (STTT),2006,8(3):216-228. [4] HENRIQUES D,MARTINS J G,ZULIANI P,et al.Statistical Model Checking for Markov Decision Processes[C]∥International Conference on Quantitative Evaluation of Systems.2012:84-93. [5] 代声馨,洪玫,郭兵,等.多处理器实时系统可调度性分析的UPPAAL模型[J].软件学报,2015,6(2):279-296. [6] DAVID A,LARSEN K G,LEGAY A,et al.Schedulability ofHerschel revisited using statistical model checking[J].International Journal on Software Tools for Technology Transfer,2012,7(2):293-307. [7] HASTINGS W K.Monte Carlo sampling methods using Markovchains and their applications[J].Biometrika,1970,7(1):97-109. [8] BUCKLEW J.A,Sadowsky,et al.A Contribution To The Theory Of Chernoff Bounds[J].IEEE Transactions on Information Theory,1991,39(1):75-75. [9] 顾雅娟,仰枫帆.基于修正的切尔诺夫界的尾部概率的估计[C]∥全国青年通信学术会议.2010. [10] MALLOY M,NOWAK R.Sequential analysis in high-dimen-sional multiple testing and sparse recovery[J].Mathematics,2011,42(4):2661-2665. [11] http://plasma-lab.gforge.inria.fr/plasma_lab_doc/1.4.0/html/algorithms/mdp.html#smart-sampling-algorithms. [12] KIM Y,KIM M,KIM T H.Statistical Model Checking for Safety Critical Hybrid Systems:An Empirical Evaluation[M].Hardware and Software:Verification and Testing.2013:162-177. [13] KWIATKOWSKA M,NORMAN G,SPROTON J.Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol[M].Process Algebra and Probabilistic Methods:Performance Modeling and Verification.Springer Berlin Heidelberg,2002:411-423. [14] PNUELI A,ZUCK L D.Probabilistic Verification[J].Information & Computation,1993,103(1):1-29. [15] https://project.inria.fr/plasma-lab. |
| No related articles found! |
|
||
首页