【摘 要】
：
近年来，随着时代的发展，计算机从单核变成多核，计算能力大大增强，如何高效利用多核处理器的性能优势来提高模型检测算法和工具的效率已成为模型检测领域的一个热门课题。时间自动
论文部分内容阅读
近年来，随着时代的发展，计算机从单核变成多核，计算能力大大增强，如何高效利用多核处理器的性能优势来提高模型检测算法和工具的效率已成为模型检测领域的一个热门课题。时间自动机是对实时系统进行建模的一种形式化方法，线性时序逻辑(LTL)是当前常用的描述性质的时序逻辑。CTAV是国际上最早实现的一个关于时间自动机的线性时序逻辑性质的符号化模型检测工具，它当初是基于Büchi自动机的（单核）空性判定算法实现的，本文将利用Büchi自动机的多核空性判定算法改造CTAV，使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具，提高模型检测的效率。 为了改造CTAV工具，在研究对比了Büchi自动机现有的一些多核空性检测算法后，采用了一种基于寻找强连通分量的多线程并行检测算法，它通过多个线程并行展开状态空间的方式加速模型检测的过程，并采取并查集的数据结构共享多个线程之间的状态信息。算法依然采取深度优先遍历的方式展开状态，在展开状态的过程中各个线程随机选取下一个后继状态，并共享状态信息，同时检测接收条件是否已得到满足。本文将Büchi自动机的这个空性判定算法应用于CTAV工具，实现了时间Büchi自动机的多核符号化模型检测，并最终采取了一种混合多种算法的方式完成了工具开发。然后，将新版本的CTAV工具和旧版以及其它主流模型检测工具进行了对比，展示了多线程算法对模型检测时间效率的提升效果。 在时间自动机的符号化状态展开过程中，符号化状态之间可能存在包含关系，通过判定符号化状态之间的包含关系实现了多核空性检测算法的一种优化，减少了不必要的状态展开，同时也可以更快的找到可接受路径，实验对比显示了我们的优化具有较好的效果。 此外，还完善了CTAV工具对Uppaal时间自动机建模语言的支持，使CTAV工具能够支持带优先级的时间自动机模型。
其他文献
网络资源管理系统是某新能源动力公司电动车充电站运营管理系统的子系统,主要完成对电动车加电站网络中各种设备资源的集中管理功能。加电站网络资源管理涉及到城市管理,场所
Web服务可视为具有并发性的分布式软件系统,可通过相关标准实现不同应用程序间的互操作。然而,并发系统往往存在非确定性进程调用,程序员在编写代码时很难考虑到大量并发进程
旅行商问题(Traveling Salesman Problem,TSP)是19世纪由爱尔兰数学家Sir William Rowan Hamilton和英国数学家Thomas Penyngton Kirkman提出的一个数学问题,是指一个旅行商,
变电站是电力系统的重要组成部分，随着变电站自动化水平的不断提高，变电站需要逐步改进为无人职守的运行模式，电力用户希望能通过浏览器随时查看变电站的历史信息及实时运行状况
物联网(Internet of Things，IoT)是一个物理对象无缝集成接入构成的信息网络世界，包括了人、机、物构成的巨大信息通信网络。随着物联网技术和应用的迅速发展，巨量的设备广泛应
RFID (Radio Frequency Identification)射频识别技术,是一种非接触式的自动识别技术,它通过射频信号自动识别目标对象并获取相关的数据。在RFID技术构成的系统中,中间件扮演
当今即时消息的主流协议SIMPLE是基于对SIP协议的扩展,SIP协议具有灵活、简单和扩展性好等优点,并且已经成为构建即时通信系统的主流信令协议。然而传统的SIP服务是基于客户
随着软件的发展,软件的质量显得越来越重要。因此,有效的软件质量保证就成为软件工程中越来越重要的环节。而软件测试是保证软件质量的最有效的方法。根据测试过程中是否执行
近年来,随着互联网技术的迅速发展,IP多媒体系统支持的服务类型越来越多,用户可选择空间随之增大。然而,虽然服务类型的多样化和服务的大量涌现很大程度丰富了人们的生活、满
随着信息化程度不断提高，数据量的不断增大，软件产品的更新换代也成为了比较常见的现象。一些软件项目没有很好的按照软件开发模型来进行，需求的满足程度和软件的扩展能力都不是