【作者】 杨琛；

【导师】 房鼎益；

【作者基本信息】 西北大学 ， 计算机软件与理论， 2006， 硕士

【摘要】 在分布式并发系统构造过程中,基于进程代数的并发系统模型检测是一种行之有效的减少设计错误、提高系统可靠性的重要途径。但并发系统本身随着规模增大其状态呈指数剧增,产生的状态爆炸问题成了模型检测在实际应用中的绊脚石。实践表明,对并发系统进行性质验证出现的状态爆炸问题需要进行深入研究。 本文分析了模型检测中状态爆炸的成因,然后针对状态爆炸问题提出相应的模型检测方法。主要包括三个方面的工作: 1.分析了状态爆炸的成因,提出了一种有效的安全性和活性验证方法,在此方法上提出基于假设的状态约减算法(简称ABSR),将性质验证放在容易产生状态爆炸的环节上,限制子系统的交互环境从而避免冗余状态剧增。 2.分析了并发系统迁移之间的依赖关系,提出基于进程代数的偏序简化技术。不仅能更大程度上限制并发系统模型的状态空间,而且保留了冗余状态信息,在需要时可根据其将冗余状态恢复出来。最后在偏序简化技术基础上提出相应的安全性验证算法。 3.设计了支持上述算法的原型系统VerTool,分析了并发模型的五种进程并发合成类型,对每一种类型用VerTool进行测试并比较了算法验证前后的结果的化简效率。在保证并发系统性质验证结果正确的同时,提高了并发系统模型检测的效率。 实验数据表明,采用ABSR方法的VerTool能够大幅度约减模型组合过程产生的冗余状态,使得模型的状态增长方式从指数转为线性;采用基于进程代数的偏序简化可以精简模型的所有冗余状态,效果更强于ABSR;由于保留了被精简掉的冗余状态信息,所以根据需要还可以恢复出这些状态并参与高一层的模型组合。总之,偏序简化技术有效地解决了模型检测在实际应用中遇到的状态爆炸问题。更多还原

【Abstract】 For developing concurrent distributed system, process algebra based model checking is widely considered as a feasible and important approach to reducing errors and increasing system reliability. However practical application of model checking to real systems has been stymied by the state explosion problem, an exponential growth in the number of states to be explored as the number of processes which composed the system increases.After investigating and analyzing the cause of state explosion problem, much research has been done about process algebra based model checking. Main contributions in this thesis are:1. The method called ABSR for verifying safety and liveness property isproposed, which advocates proving properties of a system by checking properties of its components and performs assume-guarantee reasoning in an incremental and fully automated fashion. ABSR can reduce state-space of the system during the compositional verification.2. Partial-order reduction method for process algebra is proposed, by which more redundant states can be reduced. In addition the safety property verification using partial-order reduction is presented, compared with traditional verifying method this one can resume those reduced states.3. A supported tool VerTool (Verifying Tool) is implemented to verify concurrent system using ABSR and partial-order reduction. A-B protocol and Dining Philosophers problem are deeply studied as real cases, efficiency of verification is significantly improved and the complexity is decreased.As the experiment result showing, ABSR only reduces redundant states during compositional verification. Partial-order reduction can do more extensively reduction, In addition the reduced states can be resumed and participated in higher-level model checking. Partial-order reduction availably copes with thestate-explosion problem which does harm to model checking technology.更多还原