【摘 要】
：
随着软件规模和复杂度的不断提高,软件缺陷问题不断出现。如何提高软件的可靠性已经成为软件工程领域的一个重要研究问题。程序验证技术被广泛应用于提高软件可靠性。当前的程序验证技术主要分为静态验证和动态验证两类。静态验证对程序进行抽象建模,然后验证模型是否满足给定性质,能够确保程序的覆盖率,但是受限于分析误报、自动化程度低或可扩展性差等问题。动态验证实际执行程序,基于程序的运行时信息来检查程序的正确性,能
论文部分内容阅读
随着软件规模和复杂度的不断提高,软件缺陷问题不断出现。如何提高软件的可靠性已经成为软件工程领域的一个重要研究问题。程序验证技术被广泛应用于提高软件可靠性。当前的程序验证技术主要分为静态验证和动态验证两类。静态验证对程序进行抽象建模,然后验证模型是否满足给定性质,能够确保程序的覆盖率,但是受限于分析误报、自动化程度低或可扩展性差等问题。动态验证实际执行程序,基于程序的运行时信息来检查程序的正确性,能够确保分析的精确性,但是会漏掉输入相关的错误。基于符号执行的程序验证能在静态验证和动态验证之间取得平衡:能够比静态验证获取更高的程序抽象精度,与动态验证相比又能够确保输入空间的覆盖。然而,由于程序路径数目与分支语个数成指数增长,路径空间爆炸问题成为制约符号执行的瓶颈。在分析并行程序时,由于程序执行的并行性,该问题变得更加严重。如何提高基于符号执行的程序验证的可扩展性是一个挑战性问题。本文的主要贡献涵盖以下三个方面:1.在软件工程领域,正规性质被广泛应用于性质规约。本文提出了符号化验证技术SRV来高效地验证串行程序是否满足给定正规性质。SRV将面向正规性质的路径切片与正规性质引导的动态符号执行有机结合起来:（1）本文提出了一种面向正规性质的路径切片技术来裁剪冗余路径;（2）SRV使用正规性质引导的动态符号执行技术来更快找到违背正规性质的反例路径。本文实现了SRV并将其应用于实际Java程序（总计25.9万行代码）的正规性质验证。相比动态符号执行、正规性质引导的动态符号执行和结合路径切片的动态符号执行,SRV能够获取平均至少8.4倍、8.6倍和7倍的验证加速比。2.消息传递接口（Message Passing Interface,MPI）是高性能计算领域并行编程的标准范式。由于MPI程序的复杂性,例如非确定性和异步性,MPI程序很容易出错。本文提出了一种面向非消息通信依赖MPI程序的符号化验证技术MPI-SV,能够对包含非阻塞和非确定性通信操作的MPI程序进行自动化验证。MPI-SV将符号执行与模型检验有机结合起来:符号执行自动地为模型检验抽取路径层面的通信模型;模型检验可以有效裁剪符号执行的路径空间,并扩大符号执行能够验证的性质范围。本文实现了MPI-SV,并将其应用到实际MPI C程序（总计4.7万行代码）的死锁和时序安全性质验证。实验结果展示了MPI-SV的有效性:（1）对于102个死锁验证任务,MPI-SV在1个小时内能够验证完成90个,而单纯符号执行只验证完成52个;（2）在遍历完程序路径空间和找到死锁方面,MPI-SV相比单纯符号执行能够分别获取平均7.6倍和4.96倍的验证加速比;（3）在验证时序安全性质时,MPI-SV能够成功找到违背性质的反例,而单纯符号执行则不能够发现反例。3.为提高MPI程序性能,基于Master-Slave模式的动态调度策略在MPI编程中被广泛用来实现并行工作进程的负载均衡。动态调度MPI程序由于高度的不确定性导致其可靠性难以保证。本文提出了一种面向Master-Slave模式的符号化验证方法。具体来说,本文扩展了之前的MPI-SV来支持对Master-Slave模式的验证:（1）能够在MPI程序符号执行的过程中自动识别Master-Slave模式;（2）能够对Master-Slave模式的动态调度特征进行建模,使得路径模型能够精确表示给定输入下所有可能的调度策略。本文实现了面向Master-Slave模式的符号化验证方法,并将其应用到实际动态调度MPI程序（总计1.39万行代码）的死锁验证。实验结果显示我们的符号化验证方法能够比单纯符号执行获取平均21.24倍的验证加速比。
其他文献
近年来,随着生活水平的提高和交通的快速发展,世界人口的指数增长和随之而来的城市化导致人群聚集得更加频繁。在这种情况下,人群密度分析的问题对于在人群监视和场景理解等拥挤场景中建立更高水平的认知能力至关重要,在公共安全领域意义重大。人群密度分析旨在对拥挤场景中的人数进行分析,计算总人数和密度估计,其中密度估计旨在将输入的人群图像映射到其对应的人群密度图。但像其他任何计算机视觉问题一样,人群密度分析也面
多智能体编队控制是指多个智能体在向目标机动的过程中,形成并保持某种特定构型,同时能够躲避障碍以适应环境约束的控制技术,在工业、军事、航天等众多领域有着重要的应用价值。本文以此为研究背景,开展了相对位置约束型编队机动控制方法设计、相对方位约束型编队机动控制方法设计、智能体之间的碰撞规避以及编队控制建模与仿真分析等问题的研究,取得的主要成果如下:相对位置约束型编队机动控制方法设计。假设各跟随智能体能够
漏洞是危害计算机系统安全的主要因素之一,程序漏洞的自动检测具有非常重要的研究意义,也是一个非常具有挑战的研究问题。通常,漏洞检测需要分析不完整的程序（Partial Program）,而传统基于规则的静态漏洞检测方法和工具在分析不完整程序上具有较高的漏报率和误报率。机器学习（特别是深度学习）为不完整程序漏洞检测提供了新的思路,但已有方法在真实程序上的效果仍然有待验证。我们提出了基于图神经网络的不完
近年来,伴随着大数据的兴起,大规模正则化经验风险极小化问题出现在各个领域中。作为一种求解此类大规模问题的途径,临近增量累积梯度方法（PIAG）得到了研究者的广泛关注。临近增量累积梯度方法可对应多种具体的算法实现,包括循环指标、随机指标、中心分布式等,因而有着广泛的应用前景。本文对PIAG将会涉及的研究工作进行了系统的设想和构建,从非精确算法、Bregman距离、加速格式、非凸分析、对偶算法、原对偶
惯性导航是一种自主导航方式,可以不依赖于任何外部信息支持而独立的完成导航任务,在军用与民用领域都有着广泛应用。加速度计与陀螺仪是惯性导航的核心器件。本文在对比分析了传统加速度计的优缺点基础上,针对基于双光纤光阱的光力加速度传感系统展开了初步的理论与实验研究。简单回顾了惯性导航技术的发展历程,比较了不同种类加速度计的原理和优缺点,重点分析了光力加速度传感技术的原理优势与前沿进展,指出了其高精度、小型
近年来,随着新媒体信息技术的飞速进步和传播手段的多样发展,各国国防部网站不断发展完善,网站面貌更迭焕新,但官方网站的权威属性和价值传播的实战效能始终位于核心增长点。作为最早建立的国防部门户网站,美国国防部网站几经改版,成为当今国际社会最具代表性的国防部网站之一,其重要功能之一是发布兼备机构话语、新闻话语、国防话语、军事话语的语类特征的军事新闻报道。这些报道表现出以网页为载体的多模态文本的形式特征,
随着人工智能技术的快速发展以及智能汽车应用需求的日益增长,车辆智能驾驶技术已成为当前的研究热点。智能驾驶关键技术包括环境感知、行为决策、路径规划、运动控制等,其中行为决策与运动控制技术是衡量智能驾驶车辆自主能力的关键指标,也是智能驾驶研究的重点和难点。目前,智能车辆环境感知技术已经取得了大量的研究成果,但车辆行为决策与运动控制方法仍较依赖人工先验知识来设计专家规则或模型,对复杂环境适应性不强。在动
视频是人类获取信息的重要来源。在当前信息时代,数据爆炸式的增长,随着各种视频拍摄设备的普及,人们日常拍摄并上传视频,互联网和社交媒体上已经积累了大量视频。据有关统计,每分钟上传到某知名视频网站上的视频就有300小时。如此大量的视频内容和播放量给我们带来了巨大的机遇的同时,也带了非常大的挑战。如此大量的视频,使用人力来逐个进行分析以及过滤几乎是不可能的,因此,我们迫切地需要开发能够自动理解分析视频内
干涉型光纤传感系统在水声探测、石油勘探、地震波监测等领域获得了广泛应用。随着干涉型光纤传感系统向远程化、大规模化方向发展,系统中各种非线性效应的影响日益凸显。目前,远程干涉型光纤传感系统中受激布里渊散射（SBS）已经得到了有效抑制,调制不稳定性（MI）在系统中的影响逐渐凸显。当MI发生时,系统相位噪声急剧增加,系统探测性能严重下降,故远程干涉型光纤传感系统最大输入功率必须限制在MI阈值以下,MI成
智能设备的大量普及和计算机计算能力的长足进步,为智慧城市的发展提供了强有力的基础。通过对无处不在的智能设备产生的城市大数据进行分析利用,智慧城市可以在城市规划、交通优化、环境改善、应急响应等方面提高资源利用效率,解决城市痛点问题。在多种智慧城市解决方案中,空间众包技术是一种应用非常广泛的基础性问题解决方案。其利用群体智慧和人所携带的智能设备,可以高效完成具有空间要求的任务,例如城市噪音地图的构建、