基于云计算平台的时态逻辑模型检测算法研究与实现

发布时间：2025-04-26 22:15

　　通过对动态、并发和实时系统的形式化验证保证其安全性已经成为近几十年来软件工程研究的焦点。由Edmund M.Clarke,Allen Emerson和Joseph Sifakis等人在20世纪80年代提出的模型检测是一种著名的软件形式化验证技术,它主要通过显式的系统状态搜索或者隐式的不动点计算自动地验证通信协议或者软件系统的模型是否满足要求的规格。模型检测由于其高度自动化而在工业界备受欢迎,提出者也因此在2007年荣获图灵奖。但是模型检测的状态空间随着系统组件的增加成指数增加。这个问题被称为状态空间爆炸问题。如何解决这个问题是当前科学家和学者的研究热点。在大数据和互联网+的时代背景下,云计算日新月异地迅速发展。云计算通过虚拟化技术扩展计算所需的软硬件资源,很大程度上提高了计算机的计算能力,也为应对模型检测的状态空间爆炸问题提供了新的可能的解决方案。本文首先对基于时态逻辑的模型检测技术的国内外研究现状进行了总结。然后,本文分别对云计算和大数据的起源和发展进行了深入研究,从而充分了解了云计算的发展现状和应用背景。不同的云计算的平台通常基于不同的模型实现并行分布式计算,并不能直接用于模型检测,...

【文章页数】：67 页

【学位级别】：硕士

【部分图文】：

图1.1学者们提出的应对模型检测空间爆炸问题的方法

获得了2007年的图灵奖。但是其状态空间的大小随着其成指数级的增加。这个问题又被称为状态空间爆炸问题的状态空间问题是当前科学家和学者的研究热点。者们提出的应对模型检测的状态空间爆炸问题的方法如二叉判定树是一种有效数据结构，它可以有效表示软件系]利用了软件系统中一些交织的组件的....

图1.2大数据平台和云计算的关系

当今社会是一个日新月异科技技术迅速发展的社会，人与人之间的交流、信息系统之间的交互越来越频繁，大数据（bigdata）[15]就是在这样的时代下产生的。对于大数据的定义，大数据的研究机构高德纳（Gartner）给出义是：大数据是需要新处理模式才能具有更强的决策力、洞察发现力和流....

图2.1Kripke结构的有向图表示

2预备知识子公式来表示。从某种角度来看，Kripke结构可以被看作是一机。但Kripke结构中的节点与经典的有限状态自动机中的状态是有标记的，因此具有更加丰富的内涵。图2.1给出了一个K图表示，其中可能世界集W是集合012{s,s,s}、可能世界之间二....

图2.2资源共享协议I

进程的资源共享问题[60]是一个在计算机软件系统设计过程中经常遇到举例来说，读写共享的磁盘文件或者访问数据库的时候都会涉及到资和互质访问的问题。在这类问题中，设计软件系统的时候要保证共享够被多个进程一起访问以防出现不一致的问题，例如，多个进程同时个文件就必须被禁止的。因此，设计的....

本文编号：4041445