【摘 要】
:
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。确保这些系统的可靠性成为计算机科学领域中重要研究领域。为此提出的诸多方法和理论中,模型检
论文部分内容阅读
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。确保这些系统的可靠性成为计算机科学领域中重要研究领域。为此提出的诸多方法和理论中,模型检测以其简洁明了和自动化程度高而倍受注目。模型检测是一种重要的形式化自动验证技术,此技术的成功应用归功于有效验证工具的开发和支持。SPIN是一种著名的分析验证并发系统逻辑一致性的模型检测工具。模型检测的瓶颈问题是状态爆炸问题,如何以使用精简方式描述系统,避免因为模型复杂而引起状态爆炸是一个值得研究的方向。本文在阐述SPIN模型检测形式化分析机理及线性时态逻辑LTL性质的基础上,详细分析了基于SPIN的系统建模语言Promela中的并发进程、通道操作、基本数据结构及其功能,设计了模型检测求解离散化问题的方法——通过Promela建立模型,在描述系统属性(性质)中运用分支界限技术,验证过程中LTL公式动态变化,旨在减少模型状态空间,提高搜索效率,实例分析验证了此方法的正确性;同时采用了启发式策略优化模型,即根据SPIN模型检测深度优先搜索的原则,通过静态分析和动态分析方法优化模型,实验结果分析表明SPIN不但可以验证所求解系统模型的正确性,还可以寻找模型的最优解。
其他文献
信息全球化和家庭网络的兴起极大地改变了人们的家居生活方式,智能家居的概念应运而生。而嵌入式技术、网络技术以及人工智能技术等各学科的交叉应用,为智能家居的发展提供了
社会经济的快速发展情况下,交通工具的数量和种类也越来越多,从而道路上频繁出现交通阻塞,同时发生交通事故概率也在不断增加,因而不仅要对道路交通进行合理管理还要增加对交
传统单核处理器采用超标量和流水结构提高处理器的主频,充分开发指令级的细粒度并行以提高性能。但是在当前技术条件下,如果再单纯借助于提高主频获取性能,会遇到不可逾越的
基于身份的加密方案(Identity-Based Encryption)是近几年来密码学的热门研究领域之一。它大大降低了传统公钥密码系统中公钥和证书管理的难度,具有非常高的现实价值。2008年
随着多媒体和网络技术的高速发展,越来越多的数字多媒体产品通过网络进行传播。在信息获取与交流更加便捷的同时,由于多媒体产品可以轻易地被拷贝及复制,信息隐患也随之而来
粒子群算法是一种新型的进化计算技术。本文首先对中文分词技术和文本特征选择技术进行了深入研究,分析了这些技术的原理以及基本步骤,以及一些常见的算法,根据本文特点,对已
数据挖掘技术是信息技术研究领域的方向之一。目前,数据挖掘技术在电信、商业、银行以及企业的生产、市场营销等方面都得到了广泛的应用,而在教育界的应用相对较少。高校的教务
作为现代信息采集的重要技术,无线传感器网络(WSN)从诞生以来,一直是研究和应用的热点。受到传感器节点自身资源的制约,WSN在工业监控领域的应用受到很大的限制。针对工业监
随着3G网络技术的发展,IMS(IP Multimedia Subsystem)得到了越来越广泛的应用,它是下一代网络的核心技术方案之一。IMS是3GPP在Release5版本中提出的支持IP多媒体业务的子系
随着Internet的迅速发展和应用,WEB应用已经渗透到国计民生的各个领域。相比一般传统软件,WEB应用具有更高的质量需求。WEB应用本身的高复杂性使的对其验证、测试都相当困难,基