【摘 要】
:
在分布式并发系统构造过程中,基于进程代数的并发系统模型检测是一种行之有效的减少设计错误、提高系统可靠性的重要途径。但并发系统本身随着规模增大其状态呈指数剧增,产生
论文部分内容阅读
在分布式并发系统构造过程中,基于进程代数的并发系统模型检测是一种行之有效的减少设计错误、提高系统可靠性的重要途径。但并发系统本身随着规模增大其状态呈指数剧增,产生的状态爆炸问题成了模型检测在实际应用中的绊脚石。实践表明,对并发系统进行性质验证出现的状态爆炸问题需要进行深入研究。 本文分析了模型检测中状态爆炸的成因,然后针对状态爆炸问题提出相应的模型检测方法。主要包括三个方面的工作: 1.分析了状态爆炸的成因,提出了一种有效的安全性和活性验证方法,在此方法上提出基于假设的状态约减算法(简称ABSR),将性质验证放在容易产生状态爆炸的环节上,限制子系统的交互环境从而避免冗余状态剧增。 2.分析了并发系统迁移之间的依赖关系,提出基于进程代数的偏序简化技术。不仅能更大程度上限制并发系统模型的状态空间,而且保留了冗余状态信息,在需要时可根据其将冗余状态恢复出来。最后在偏序简化技术基础上提出相应的安全性验证算法。 3.设计了支持上述算法的原型系统VerTool,分析了并发模型的五种进程并发合成类型,对每一种类型用VerTool进行测试并比较了算法验证前后的结果的化简效率。在保证并发系统性质验证结果正确的同时,提高了并发系统模型检测的效率。 实验数据表明,采用ABSR方法的VerTool能够大幅度约减模型组合过程产生的冗余状态,使得模型的状态增长方式从指数转为线性;采用基于进程代数的偏序简化可以精简模型的所有冗余状态,效果更强于ABSR;由于保留了被精简掉的冗余状态信息,所以根据需要还可以恢复出这些状态并参与高一层的模型组合。总之,偏序简化技术有效地解决了模型检测在实际应用中遇到的状态爆炸问题。
其他文献
目前,远程教育的教学方式中应用最广泛影响最深远的是基于Web的远程教育,然而基于Web的多媒体计算机远程教学系统存在着系统智能性不高、系统的弹性与适应性不足等缺点。Agen
对集值属性数据库进行查询与检索有赖于高效的检索机制。因此,如何将基于集值属性的数据库数据进行合理的分类,从而建立相应的索引机制并进行子集查询就成为了一个亟待解决的问
本项研究工作的背景是:四川省网络通信技术重点实验室对下一代Internet体系结构的研究——“单物理层用户数据传输与交换平台”(SUPA-Single User-data transfer & switching
在角色动画中人物模型是由动作数据驱动的,而动作数据一般通过动作合成编辑以及动作捕捉技术得到。随着动作数据的急速膨胀,动作数据检索技术变得尤为重要。本文首先讨论了动
随着互联网数据信息的爆炸式增长,以及现今云计算、云存储环境下大规模数据密集型应用的蓬勃发展,分布式文件系统以其高可靠性,高吞吐率以及海量的存储能力等优点,受到了学术界和
出于存储效率的考虑,纠删码存储策略已成为副本存储策略的重要补充。为节省存储空间,存储系统往往将低热度副本数据按纠删码方式进行归档存放;另外,相对于副本方式,纠删码方式存在
目前,嵌入式系统已经渗透到各个领域:工业控制,军事国防,消费类电子产品,网络通信等,但大部分领域的应用都是基于国外各大厂商的嵌入式处理器。在嵌入式领域使用国产芯片,走
体视化尤其是其中的体绘制是三维数据场可视化领域最重要、近年来发展最迅速的一项技术,在医学三维重建、计算流体力学、有限元后处理、地震地质等众多领域得到了广泛应用.但
随着计算机网络技术,数据库技术的飞速发展,实时数据库系统(RTDBS)的应用领域也越来越广,如科研、工业、军事、通讯和金融等领域。新的领域应用对RTDBS的性能提出了更高的要求。
芯片集成度的快速增长,使得集成电路工业进入SOC时代。既包括软件,又包括硬件的复杂的混合系统可以被集成到一块芯片上。提高设计的抽象层次,可以大大降低建模复杂度。传输级