基于概率模型的Raft协议形式化验证.pdf

计算机与现代化JISUANJI YU XIANDAIHUA2023年第9期总第337期文章编号：1006-2475（2023）09-0077-05收稿日期：2022-09-22；修回日期：2022-11-09基金项目：广东省自然科学基金资助项目（2020A1515010445）作者简介：管金平（1997），男，湖南衡阳人，硕士研究生，研究方向：模型检测，协议验证，E-mail：；通信作者：杨晋吉（1968），男，教授，博士，研究方向：模型检测，协议验证，E-mail：；杨成龙（1996），男，硕士研究生，研究方向：模型检测协议验证。0引言随着Internet的迅速发展，分布式系统应用也越来越广泛。它与传统的集中式系统相比较更适合目前的大数据时代，但分布式系统目前也存在一些缺点亟需解决，比如在可能出现故障的各节点间保证同一数据的多个副本的一致性问题。在分布式系统中，有很多复杂的理论，从CAP理论1到BASE理论2，学者们不断地在可用性以及一致性之间做出权衡，就分布式一致性而言，又有许多协议，如从 Paxos算法3到ZAB 协议4，再到 Raft共识协议5（以下简称 Raft协议或Raft算法）。Raft协议是目前分布式系统中常见且有效的共识算法，因此稳定可靠的Raft算法能够保证分布式系统的数据一致性以及高效运转。概率模型检测6是一种高度自动化的形式化验证技术，基于数学理论依据和模型检测工具对具体的计算机系统抽象建模并分析验证，在软件开发、博弈论、生物工程、通信协议和网络安全等领域都有大量成果。概率模型检测作为模型检测技术里的重要分支，近年来在各形式化验证领域都有了显著的研究结果。任胜兵等人7设计了基于概率模型检测的软件缺陷定位算法，用于缺陷定位分析。Mohsin等人8使用概率模型检测来评估并分析了物联网中由于不同的配置部署，而带来的不同级别的安全风险，并通过模型计算出每个配置的可能性与攻击者的成本。王晶等人9使用概率模型检测方法对Web服务组合进行了建模，定量分析并验证了Web服务组合的有效性和可靠性。本文使用概率模型检测技术对分布式系统中的Raft协议进行形式化建模，并用概率计算树逻辑表达式描述要检测的性质，对该协议的一致性与高效性进基于概率模型的Raft协议形式化验证管金平，杨晋吉，杨成龙（华南师范大学计算机学院，广东 广州 510631）摘要：共识协议作为分布式系统的关键要素和核心组件，用于解决分布式场景下可能出现故障的节点间保证同一数据一致的问题，其准确性和高效性直接决定了系统的性能。Raft共识协议是目前分布式系统中常见且有效的算法。本文首先使用概率模型检测方法对Raft共识协议进行形式化建模，然后利用概率模型检测的属性规约技术对它的相关属性进行描述，最后通过模型检测工具验证并分析Raft共识协议的一致性和高效性。实验结果表明，Raft共识协议满足一致性，但是在领导者选举阶段，当跟随者维护的最新日志序号的差值范围增加时，选举回合数也会增多，使得整个服务周期选举时间增加，从而影响协议的执行效率。关键词：分布式系统；Raft共识协议；概率模型检测；形式化验证；属性规约中图分类号：TP391文献标志码：ADOI：10.3969/j.issn.1006-2475.2023.09.012Formal Verification of Raft Protocol Based on Probabilistic ModelGUAN Jin-ping，YANG Jin-ji，YANG Cheng-long（School of Computer Science，South China Normal University，Guangzhou 510631，China）Abstract：Consensus protocol is important element and core component of distributed system，it is dedicated to solve the problem of ensuring the same data consistency among nodes that may fail in a distributed scenario，and its accuracy and efficiency directly determine the performance of the system.Raft consensus protocol is common and effective consensus algorithm in currentdistributed systems.This paper firstly models the Raft consensus protocol formally using a probabilistic model detection method，then describes its relevant properties using property spcification technique of probabilistic model checking，and finally verifiesand analyses the consistency and efficiency of the Raft consensus protocol.The experimental results show that it satisfies consistency，but the number of election rounds increases during the leader election phase when the difference range of the latest log serial numbers maintained by followers increases，resulting in the election time increase throughout the service cycle，thus affecting the execution efficiency of Raft.Key words：distributed system；Raft consensus protocol；probabilistic model checking；formal verification；property specification计算机与现代化2023年第9期行定量分析，最终对验证结果进行分析与讨论。目前，已有学者对Raft算法的形式化验证进行了一些相关的工作。Schultz等人10对基于Raft协议的复制系统的重新配置协议进行了形式化验证，并使用 TLA+和 TLAPS（TLA+证明系统）来形式化和机械验证协议中的归纳不变量和安全证明。Woos 等人11对Raft协议的状态机安全性进行形式化验证，并提出了一种在验证过程中证明不变量的方法。周浩洋12使用形式化方法对共识算法PBFT进行形式化建模，验证并分析了协议的安全性，并提出了改变参与协议执行的节点数量来探究协议容错性上限的方法。顾佳仪13使用概率模型检测对动态系统领导者选举协议进行分析与验证，在模型构建的过程中，引入了“假设-保证”的组合式验证思想，将层次式协议进行分别处理，建立了一个具有双层结构的领导者选举协议模型，并通过实验，得出了结果，显示了模型的有效性。Evrard14使用LNT过程代数对Raft协议进行建模，指出了Raft算法的原始TLA+规范存在的一些问题，并讨论了如何最好地使用 LNT形式语言的特性和相关的 CADP 验证工具箱来模拟分布式协议，包括网络和服务器故障。1相关基础知识1.1Raft协议Raft协议是一种用于管理状态复制机集群的复制日志算法15。Raft集群包含多个服务器，在任何给定的时刻，每个服务器都处于以下3种角色之一：领导者（Leader）、候选者（Candidate）和追随者（Follower）：1）Follower：每个服务器的初始角色，主要负责执行来自Leader的指令。如果收到客户端的操作请求会转发给 Leader。2）Candidate：这是一个过渡角色，如果 Follower在一定的时间没有接收到 Leader的心跳，此时进入领导者选举，本节点切换为Candidate，直到选举结束。3）Leader：整个集群中只有一台服务器是Leader，主要负责处理客户端的所有请求，并发送指令给所有Follower。它们之间的转换关系如图1所示。图1Raft协议中角色转换Raft算法中是以任期（Term）为时间单位，如图2所示，每个任期都会以领导者选举开始，选举成功后，领导者会管理这个任期内的所有操作直到任期结束。在某些情况下，选举会导致分裂投票。此时，任期将在没有领导者的情况下结束，紧接着会开始下一个新的任期。Raft算法确保在给定的任期内最多有一个领导者。图2Raft协议的任期1.2概率模型检测1.2.1连续时间的马尔可夫链连续时间马尔可夫链16（Continuous-Time Markov Chain，CTMC）扩展了DTMC17，使得CTMC可以描述状态迁移随时间连续变化的系统。定义1连续时间的马尔可链定义为C=，其中：S是非空有限状态集；s是初始状态，且sS；R：SSR+是迁移比率函数；AP是一个原子谓词集合；：S2AP是状态映射到AP的标记函数。CTMC的状态转换只有在R（s，s）0的情况下发生，在这种情况下，t个单位时间内触发状态转换的概率为1-e-R（s，s）t。当一个状态中有多个可能的转换可用时，就会发生竞争状况。引入出逃率E（s）来表示状态迁移的概率 E（s）=defssR（s，s）=1，sS，如果 E（s）=0，则状态s为吸收状态，表示状态s没有对外发生迁移。因此状态s迁移到s的概率为：P(s，s)=R(s，s)E(s)，E(s)01，E(s)=0且 s=s0，其他1.2.2概率计算树逻辑概率计算树逻辑（PCTL）18-19是一个著名的概率时间逻辑，也是计算树逻辑（CTL）20的扩展。PCTL是能够定量描述概率系统的时序命题。定义2PCTL语法表示如下：状态公式：=true|a 12|pp()路径公式：=X|12|F|G|1W 2|1R 2其中，a是一个原子命题；p是概率界限值；X（next）表示路径的下一个状态；U（until）表示某状态直到另一状态；F（future）表示某状态在结束时的状态；G（globally）表示某状态直到结束时的状态；W（weak until）是U的变体，相当于1U 2|G1，要求1直到2前永远为真；R（release）相当于!(!1U!2)，表示2在1变为真之前一直为真。1.2.3概率模型检测工具PRISM是由牛津大学 Kwiatkowska 教授课题组开发的概率模型检测工具21，它可以对具有随机行为的系统进行自动验证。图3是PRISM工具的工作过程。PRISM建模语言是一种基于状态的描述性语言，它的基本组成部分是模块和变量。其语法结构如下所示：跟随者候选者领导者跟随者跟随者开始超时时间片到，开始选举选举超时，开始新一轮收到大多数赞同的选票发现新的领导者或更高任期发现其他服务器有更高的任期Term1Term2Term3Term4Terms选举正常操作选举被分裂782023年第9期actionguard（p1：up1）+（pn：upn）其中，guard是模型中变量的谓词逻辑；upi描述了一个状态转换，如果 guard为真，模块可以进行状态转换；pi表示当前转换的概率（或速率）；action可以是为了对转换进行注释，或者可以是为了同步。图3PRISM工作过程2Raft协议建模与分析Raft算法中Leader负责处理客户端的所有请求，以及将日志分发给其他Followers，本章将详细介绍领导者选举过程的形式化建模与分析。2.1Raft协议建模领导者选举采用投票机制，只要某个 Candidate得到大多数Follower的支持，那它就能成为Leader，并开始向客户端提供服务。单个任期中的领导者选举流程如图4所示。图4单个Term内领导者选举流程Step1：CandidateFollower：RequestVoteRPC（CID，TermID，LogIndexID）Step2：FollowerCandidate：（voteResultID）其中，ID表示集群中某台服务器的唯一身份码，CID表示 Candidate 的 ID，LogIndex 表示最新日志的标号，Term表示当前领导者的任期，voteResult表示Follower的投票结果。当Follower收到投票申请时，会比较自身的最新日志序号与Candidate的日志序号，如果自身日志旧或是一样新则投赞同票，否则投反对票，并告知当前Candidate：日志不是最新的，宣告本轮选举失败。最后Candidate只有获得大部分的赞同票才能当选成功。单轮选举具体流程见图5。Raft协议中每个任期都是连续递增，并且在一个任期内所进行的操作都是领导者选举和处理日志复制的，因此将Raft协议建模为连续时间的马尔可夫链模型，其中各个模块的变量定义见表1。定义整个模型到达选举成功（有且仅有一个领导者）的状态如下：label“success”=leader=true&phase=4&state1=2&state2=2&state3=2&state4=2&state5=2使用 PRISM 语言描述跟随者模块如算法 1 所示，其中vote动作是模拟跟随者进行投票表决；retry命令表示当前Candidate没能当选成功，需要接受新的Candidate的投票请求。算法1Follower模块核心代码module Follower1 vote state1=1&phase=2-voteProbability：（voteResult1=（logIndex1C_logIndex赞同Candidate担任LeaderCandidate选举成功，担任Leader选票是否过半？当前Candidate日志不是最新，开始新一轮选举否是是否图5Raft协议领导者选举流程表1领导者选举变量定义变量名NKvoteProbabilityphasecandidateLogIndexleaderstatelogIndexvoteResult描述服务器节点数量日志序号范围跟随者回复成功率表示控制投票过程：0：初始化阶段1：Candidate发起选举投票2：Follower开始投票表决3：重新发起投票4：结束candidate的日志序号选举成功的标志：true：本次选举成功false：不成功，重新选举Follower的状态枚举：0：随机生成日志序号1：开始投票表决2：重新下一轮投票日志序号投票表决结果：0：不赞同1：赞同2：候选者日志不是最新的，终止本轮选举管金平，等：基于概率模型的Raft协议形式化验证79计算机与现代化2023年第9期+（1-voteProbability）：（voteResult1=false）&（state1=2）；retryphase=3&!leader-（state1=1）；endmodule候选者模块的建模如算法2所示，其中round动作标志选举开始，后面也会用来记录回合数；request动作用来模拟当集群中没有Leader时，随机选择一个节点发起投票请求；retry动作表示当本轮选举的赞同票数没有过半时，重新进行下一轮选举；done命令表示选举成功，当前 Candidate_ID担任集群的领导者；最后3行代码表示概率模型检测中的奖励机制，为每个候选者发起投票请求时分配1的奖励。算法2候选者模块核心代码module Candidateroundphase=0-（phase=1）&（leader=false）；request phase=1&end_init-1/N：（phase=2）&（candidateLogIndex=logIndex1）+1/N：（phase=2）&（candidateLogIndex=logIndex5）；retryphase=3&num_ticket（phase=0）；done phase=3&num_ticket=N-（phase=4）&（leader=true）；endmodulerewards“rounds”roundphase=0：1；endrewardsPRISM建模结果如算法 3所示。算法3Raft协议建模日志Model constants：K=8，voteProbability=0.5Computing reachable states.Reachability（BFS）：9iterationsin0.03seconds（average0.003222，setup 0.00）Time for model construction：0.239 seconds.Type：CTMCStates：8476782（1 initial）Transitions：38004665Rate matrix：58992 nodes（12 terminal），38004665 minterms，vars：38r/38c2.2Raft协议分析本节将对Raft协议领导者选举的有效性、时效性以及通过选举的回合数对选举所耗时间进行定量分析。属性1 有效性。领导者选举的有效性是指保证能够在一定时间内选举出一个领导者。本文实验将从跟随者回复成功率与集群节点数 2 个维度验证Raft协议中领导者选举过程的有效性。验证各种回复成功率的情况下是否能达到稳定状态，使用PCTL表达式描述如下：P1 F“success”从图6可以得知，当voteProbability0 时，模型最终到达选举成功的状态概率1。下面验证集群中节点数对达到选举成功状态的影响；由于概率模型检测中的状态爆炸问题22-23的存在，所以本次仅模拟节点数达到7，属性的PCTL表达式描述如下：P=？F“success”由图7可知，当N=3|5|7时，它们的概率变化曲线一样，换言之，集群中节点个数并不影响模型达到选举成功的状态。图7节点数对有效性的影响综合上述2个验证实验可知，只要有跟随者能对此次投票进行表决（voteProbability0），Raft协议就能保证一定能选出唯一的领导者，即满足有效性。属性2时效性。时效性是领导者选举过程中的衡量资源消耗的一个重要指标。如果选举过程较长，会使整个集群的服务效率大大降低，从而影响系统的效率和用户满意度。本次实验利用选举的回合数（rounds）来模拟从开始选举到选举成功所需时间。首先验证前T个单位时间内，不同的回复成功率下所需rounds的总数量，利用PCTL表达式描述如下：R“rounds”=？CT由图 8中变化曲线可知，跟随者回复成功率越高，模型达到success状态所需的单位时间越少；当T 50 时，选举成功率 0.5 的所需rounds明显减少，且都能达到success状态。Raft协议规定各节点的本地状态机上的日志序号连续递增，并且跟随者的日志不会比领导者的新，因此在选举过程中，一定是日志最新的节点当选领导者，所以本次实验将验证各节点最新日志的范围对选举回合数的影响。为了尽量排除跟随者回复率对实验的影响，本次实验取voteProbability0.5，单位时间T 0，50。属性描述如下：R“rounds”=？F“success”其 中，K 表 示 最 新 日 志 范 围，即 logIndex_max-logIndex_min；由图9可知：K值越大，模型达到success状态的回合数就多。结合上述2个实验可知，当节点回复成功率大于或等于0.5时，能选举出唯一的领导者平均也需要23回合，但这是不可避免的，因为分布式系统中单点故障是客观存在的；而对于日志范围较大的情况下，0.00.10.20.30.40.50.60.70.80.91.0voteProbabiltityN=5N=3N=71.000.750.500.250.00Probability图6跟随者回复率对有效性的影响802023年第9期所需选举的回合数还会持续增加，原因就是由于每次选举都是随机产生的，并且可能会出现同一选举周期内，候选者重复提交选举申请。3结束语随着分布式系统的快速发展，使各节点在可能出现故障的情况下，依然能对同一数据的多个副本保持一致就成为了影响整个分布式系统运行的关键一环，本文通过概率模型检测技术对解决分布式系统数据一致性问题的Raft协议进行建模与分析，发现Raft协议能够有效地解决某一时间内数据一致性，然而在投票选举中，随着最新日志序号的范围不断增大，所需的选举回合数也会增加，即选举时间会变长，从而影响系统效率。相比于何东炼等人27使用模型检测技术去验证分布式协议的研究，本文采用概率模型检测技术可以量化地表示分布式协议的设计和运行指标，从而使得协议逐步完善，以满足设计所需；且本文采取分阶段建模方法，化繁为简，验证了分布式协议算法中的核心选举阶段，从而提出了Raft协议在选举阶段所需回合数较多，耗时较长。因此本文的工作可以给Raft协议选举阶段的优化提供参考方案，通过优化Raft协议选举阶段的选举回合数来提高Raft协议的执行效率。下一步工作可以进一步分析和优化Raft协议选举阶段，然后进行实验验证。参考文献：1 GILBERT S，LYNCH N.Perspectives on the CAP theoremJ.IEEE Computer，2012，45（2）：30-36.2 PRITCHETT D.BASE：An acid alternative：In partitioneddatabases，trading some consistency for availability canlead to dramatic improvements in scalabilityJ.Queue，2008，6（3）：48-55.3LAMPORT L.The part-time parliamentM/Concurrency：The Works of Leslie Lamport.2019：277-317.4 JUNQUEIRA F P，REED B C.Brief announcement ZAB：A practical totally ordered broadcast protocol C /InternationalSymposiumonDistributedComputing.2009：362-363.5ONGARO D，OUSTERHOUT J.In search of an understandable consensus algorithm C/2014 USENIX AnnualTechnical Conference（Usenix ATC 14）.2014：305-319.6 KWIATKOWSKA M，NORMAN G，PARKER D.Probabilistic model checking：Advances and applications J.Formal System Verification.2018：73-121.7 任胜兵，陈军，谭文钊，等.基于概率模型检测的软件缺陷定位方法 J.计算机应用研究，2021，38（11）：3387-3392.8MOHSIN M，SARDAR M U，HASAN O，et al.IoTRiskAnalyzer：A probabilistic model checking based frameworkfor formal risk analytics of the Internet of Things J.IEEEAccess，2017，5：5494-5505.9 王晶，戎玫，张广泉，等.基于概率模型检测的Web服务组合验证 J.计算机科学，2012，39（1）：120-123.10 SCHULTZ W，DARDIK I，TRIPAKIS S.Formal verification of a distributed dynamic reconfiguration protocol C/Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs.2022：143-152.11 WOOS D，WILCOX J R，ANTON S，et al.Planning forchange in a formal verification of the Raft consensus protocolC/Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs.2016：154-165.图8投票成功率对选举回合数的影响图9日志范围对选举回合数的影响TK（下转第86页）管金平，等：基于概率模型的Raft协议形式化验证81计算机与现代化2023年第9期RNN模块的VGG网络对花卉的识别率高于其他网络，达到86.8%。但DF-RNN模块对于人眼视觉感知系统来说还是过于简单，如何设计一种完全符合人眼视觉感知特性的卷积神经网络是今后进一步研究的方向。参考文献：1 NILSBACK M E，ZISSERMAN A.Automated flower classification over a large number of classes C/The 6th IndianConference on Computer Vision，Graphics&Image Processing.2008：722-729.2 ANGELOVA A，ZHU S.Efficient object detection and segmentation for fine-grained recognitionC/2013 IEEEConference on Computer Vision and Pattern Recognition.2013：811-818.3ZHANG C，LIU J，LIANG C，et al.Image classificationusing Harrlike transformation of local features with codingresiduals J.Signal Processing，2013，93（8）：2111-2118.4 TIAY T，BENYAPHAICHIT P，RIY-AMONGKOL P.Flowerrecognition system based on image processingC/20143rd ICT International SeniorProject Conference（ICT-ISPC2014）.2014：99-102.5 谢晓东.面向花卉图像的精细图像分类研究 D.厦门：厦门大学，2014.6LECUN Y，BOTTOU L，BENGIO Y，et al.Gradient-based learning applied to document recognitionJ.Proceedings of the IEEE，1998，86（11）：2278-2324.7ZAREMBA W，SUTSKEVER I，VINYALS O.Recurrentneural network regularizationJ.arXiv reprint arXiv：1409.2329，2014.8KRIZHEVSKY A，SUTSKEVER I，HINTON G，et al.ImageNet classification with deep convolutional neural networks J.Communications of the ACM，2017，60（6）：84-90.9 SZEGEDY C，WEI L，JIA Y，et al.Going deeper with convolutionsC/Proceedings of the IEEE Conference onComputer Vision and Pattern Recognition.2015：1-9.10 SIMONYAN K，ZISSERMAN A.Very deep convolutionalnetworks for large-scale image recognitionJ.ComputerScience，2014，30（6）：1409-1556.11 HE K M，ZHANG X Y，REN S Q，et al.Deep residuallearning for ima-ge recognitionC/Proceedings of the2016 IEEE Conference on Computer Vision and PatternRecognition.2016：770-778.12 HUANG G，LIU Z，KILIAN Q.Densely connected convolutional networksC/IEEE Computer Society.2017：4700-4708.13 张川.面向图像分类的深度残差网络优化结构研究D.北京：中国科学院大学，2016.14 王丽雯.基于AlexNet的Oxford花卉识别方法 J.科技视界，2017（14）：83-83.15高建瓴，王竣生，王许.基于DenseNet的图像识别方法研究 J.贵州大学学报（自然科学版），2019，36（6）：58-62.16 郭玉荣，张珂，王新胜，等.端到端双通道特征重标定DenseNet 图像分类 J.中国图象图形学报，2020，25（3）：486-497.17 武慧琼，张素兰，张继福，等.一种基于三支决策的花卉图像分类J.小型微型计算机系统，2019，40（7）：1558-1563.18 叶鑫焱.花卉图像精细分类的研究 D.福州：福州大学，2018.19 MURABITO F，SPAMPINATO C，PALAZZO S，et al.Top-down saliency detection driven by visual classificationJ.Computer Vision and Image Understanding，2018，40（7）：1130-1141.20任意平，夏国强，李俊丽.基于优化 AlexNet的花卉识别J.电子测量技术，2020，43（19）：94-98.21 张秋颖，金雪松.基于卷积神经网络和迁移学习的花卉图像分类 J.哈尔滨商业大学学报（自然科学版），2020，36（3）：323-327.22何文静，唐庭龙，吴义熔.基于同步重建与分类的深度自编码的分类网络 J.长江信息通信，2022，35（5）：21-24.23 刘德建.基于LeNet的花卉识别方法 J.电子技术与软件工程，2015（23）：13-14.24 尹红，符祥，曾接贤，等.选择性卷积特征融合的花卉图像分类 J.中国图象图形学报，2019，24（5）：762-772.25 张力.基于反馈信息的深度学习推荐算法研究 D.武汉：华中师范大学，2019.26 邓远远，沈炜.基于注意力反馈机制的深度图像标注模型 J.浙江理工大学学报（自然科学版），2019，41（2）：208-216.27高欣.卷积神经网络的改进及其在图像分类中应用研究D.秦皇岛：燕山大学，2021.28曹春水.深度卷积神经网络中反馈机制的计算建模及应用研究 D.合肥：中国科学技术大学，2018.12周浩洋.基于模型检测的区块链共识协议形式化分析与验证 D.南昌：华东交通大学，2021.13顾佳仪.基于概率模型检测的动态系统领导者选举协议分析与验证 D.南京：南京航空航天大学，2016.14 EVRARD H.Modeling the Raft distributed consensus protocol in LNT J.arXiv preprint arXiv：2004.13284，2020.15 ONGARO D，OUSTERHOUT J.In Search of an Understandable Consensus Algorithm（Extended Version）R.Tech Report，2013：551-563.16 KATOEN J P，KWIATKOWSKA M，NORMAN G，et al.Faster and symbolic CTMC model checking C/Joint International Workshop von Process Algebra and ProbabilisticMethods，PerformanceModelingandVerification.2001：23-38.17 NORRIS J R，NORRIS J R.Markov ChainsM.Cambridge University Press，1998：9-15.18 HANSSON H，JONSSON B.A logic for reasoning abouttime and reliabilityJ.Formal Aspects of Computing，1994，6（5）：512-535.19 ZHOU C H，LIU Z F，WANG C D.Bounded model checking for probabilistic computation tree logicJ.Journal ofSoftware，2012，23（7）：1656-1668.20 MURANO A，PARENTE M，RUBIN S，et al.Model-checking graded computation-tree logic with finite path semanticsJ.Theoretical Computer Science，2020，806：577-586.21 KWIATKOWSKA M，NORMAN G，PARKER D.PRISM4.0：Verification of probabilistic real-time systemsC/International conference on computer aided verification.2011：585-591.22 屈媛媛，杜伊.软件模型检测中状态爆炸问题的解决方法 J.现代计算机（专业版），2017（2）：35-38.23 侯刚，周宽久，勇嘉伟，等.模型检测中状态爆炸问题研究综述 J.计算机科学，2013，40（S1）：77-86.24高洪皓，缪淮扣，刘浩宇，等.基于概率模型检验的云渲染任务调度定量验证 J.软件学报，2020（6）：1839-1859.25 ZHAO X Y，ROBU V，FLYNN D，et al.Probabilisticmodel checking of robots deployed in extreme environmentsC/Proceedings of the AAAI Conference on Artificial Intelligence.2019，33（1）：8066-8074.26 骆翔宇，黄欣玥，古天龙，等.基于时态测试器的实时分支时态逻辑模型检测J.软件学报，2022，33（8）：2930-2946.27何东炼，杨晋吉，管金平，等.使用模型检测方法对Paxos算法进行验证与改进 J.小型微型计算机系统，2022，43（5）：1109-1113.28 夏奴奴，杨晋吉，赵淦森，等.基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 J.计算机科学，2019，46（8）：206-21