【摘 要】
：
随着计算机应用的不断发展,人们对软件的高可靠性要求越来越高。形式化方法是基于数学和逻辑语言的精确性规格、验证,保证软件高可靠性的重要方法。模型检测是一种形式化的验
论文部分内容阅读
随着计算机应用的不断发展,人们对软件的高可靠性要求越来越高。形式化方法是基于数学和逻辑语言的精确性规格、验证,保证软件高可靠性的重要方法。模型检测是一种形式化的验证技术,对该理论的研究和应用成为国内外近几年的热点问题。在计算机硬件、安全协议验证等领域,模型检测技术已经取得了丰硕的成果。为了实现软件的高可靠性,首先要对影响软件可靠性的软件漏洞进行学习和研究。论文不仅介绍了软件漏洞的分类而且对几种具体的漏洞进行了分析和定义。时序逻辑语言是模型检测的基础,为了掌握模型检测技术,对线性时序逻辑语言LTL进行了详细的描述,使用LTL对分析得到的漏洞定义进行了描述,从而得到了LTL公式。并且详细地介绍了模型检测工具SPIN。通过对SET购买过程协议使用SPIN进行验证,更深入的了解了该模型检测工具的建模语言promela以及属性定义语言LTL。模型检测技术应用在软件漏洞检测领域主要包括对需求分析和设计阶段的软件模型进行模型检测和对目标代码的模型检测。本课题选择了对软件开发初期阶段的设计模型进行形式化验证,可以及早的规避软件逻辑漏洞和安全漏洞,大大减少软件开发成本,缩短软件开发周期。并且对软件设计模型的形式化验证基于UML行为模型。UML建模是目前软件开发中最主要的可视化建模方法,而模型检测等形式化方法在建模过程中存在可视化困难,因此,将两种方法结合进行软件漏洞的检测,可以有效地减少形式化建模方面的难题。本课题主要研究在软件开发初期,对UML行为模型进行模型检测。首先,对UML行为模型转换为扩展层次自动机EHA模型的转换规则进行了描述,结合ATM工作流程的状态图模型,对该转换过程进行了实现。其次,给出了部分活动图的模型元素对应的EHA模型转换为promela模型的描述框架。同时,结合哲学家就餐问题的活动图模型的SPIN模型检测过程进行了详述,给出了死锁问题的验证结果。
其他文献
无线传感器网络从概念出现开始就引起人们广泛关注并被寄予厚望,在最近的几年内,各种无线传感器网络产品不断投入到生产、生活、科研等应用中,尤其近期温家宝总理关于“感知
IEEE 802.15.4标准是提供给低速率、低功耗和低成本设备使用的短距离无线通信协议并定义了低速无线传感器网络的MAC层和物理层规范。本文通过深入研究该协议标准,在低功耗的
汉字是历史悠久的中华民族文化的结晶,闪烁着中国人民智慧的光芒。汉字识别是一种难度非常大的模式识别。其中脱机手写汉字识别是目前最为困难也最具挑战性的研究课题。在办
随着Web技术的发展,非关系型数据库已经成为国际数据库界研究热点。同时,伴随着XML技术的发展,XML正逐渐成为Web上数据表示与交换的统一标准。因此,有关XML数据管理技术的研
电力变压器作为电力系统中最重要的输变电设备之一,它的性能直接影响到电力系统运行的安全和可靠。及时、准确地掌握其运行状态和故障情况,并采取相应的处理措施,对于提高电力系统运行的安全性、可靠性和经济性具有重要的意义。针对变压器的故障诊断,前人提出了很多的解决方法,但都有这样或那样的缺陷,不能迅速、准确的做出判断。本文针对目前变压器故障诊断技术在实际应用中所存在的主要问题,引入神经网络理论,将改进的粒子
学科建设是高等学校建设和发展的核心，是高等学校长期而艰巨的任务。学科建设的状态体现高等学校的整体办学实力、学术地位和核心竞争力，其内容涉及到学科队伍建设、科学研究、
由于互联网资源的“成长性”、“自治性”和“多样性”，传统的C/S模式的资源搜索方法逐渐不能满足发展需求。近年来，人们提出建立基于DHT(distributed Hash table)的对等网络实
虚拟化技术凭借充分利用宿主机资源、快速部署、高可用性等优势在企业中得到了广泛应用。近几年,随着企业信息化规模的不断扩大,虚拟服务器的部署规模也在不断扩大,相对于传
随着Wleb技术在互联网中发展,用户不再是简单地从网络中获取信息,而是采取更加主动的方式产生信息。由于用户数量的急剧增长,以用户为中心的信息产生模式,导致了互联网信息量
随着Web作为互联网上最重要的应用之一,它提供了便捷的文档发布和信息的获取,并且各地的信息资源聚集在互联网上,成为生活中不可缺少的一部分。根据官方资料的显示,在互联网