CAJ | 학술논문

随机模型检验作为模型检验理论的延伸和推广，可用于验证分析系统模型的定性或定量性质，其已经应用到随机分布式算法验证、通信协议性能分析甚至是系统生物学等跨学科领域。从20世纪90年代末至今，随机模型检验引起了形式验证等领域的广泛关注，并取得了很大的进展。该文追溯了随机模型检验的渊源，系统地概括了其最基本的原理及几类典型的 PCTL、概率的 LTL、PCTL*和 CSL 模型检验随机系统的算法框架。然后归纳总结了随机模型检验的主要研究方向及其进展，分析了基于随机模型检验的验证过程及其优势与劣势，并分类列出了目前出现的随机模型检验工具。最后介绍了随机模型检验的应用领域并指出了其未来的应用挑战。
수궤모형검험작위모형검험이론적연신화추엄，가용우험증분석계통모형적정성혹정량성질，기이경응용도수궤분포식산법험증、통신협의성능분석심지시계통생물학등과학과영역。종20세기90년대말지금，수궤모형검험인기료형식험증등영역적엄범관주，병취득료흔대적진전。해문추소료수궤모형검험적연원，계통지개괄료기최기본적원리급궤류전형적 PCTL、개솔적 LTL、PCTL*화 CSL 모형검험수궤계통적산법광가。연후귀납총결료수궤모형검험적주요연구방향급기진전，분석료기우수궤모형검험적험증과정급기우세여열세，병분류렬출료목전출현적수궤모형검험공구。최후개소료수궤모형검험적응용영역병지출료기미래적응용도전。
Stochastic model checking is extension and generalization of the theory of model checking,which can verify and analyze system model quantitatively and qualitatively,and has been applied in the areas of verification of randomized distributed algorithms,performance analysis of communication protocols,and even the cross-disciplinary fields such as systems biology.Since the late 1990s,stochastic model checking has received widespread concern in the formal verification filed,and has made great progress.In this paper,we retrospect the origin of stochastic model checking,and discuss the basic principle of stochastic model checking systematically including the PCTL,LTL with probability bounds,PCTL* and CSL model checking algorithm.Then we summarize the main research direction and progress of stochastic model checking in recent years, analyze the verification process and advantages/disadvantages of stochastic model checking deeply, classify and list tools for stochastic model checking.Finally,we introduce the application areas of stochastic model checking and point out its future challenge.