摘要:形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专刊收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.

摘要:几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等,都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后,为了说明几何代数形式化的有效性和实用性,在共形几何代数空间中,给刚体运动问题提供了一种简单有效的形式化建模与验证方法.

摘要:运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法.该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.

摘要:基于实时演算(real-time calculus,简称RTC)理论,为单/双行道两类城市交通网络的定时和自适应两类信号控制系统建立了统一的形式化模型.首先,将车流和交叉路口分别建模为RTC的到达曲线和资源曲线;然后,根据不同信号控制策略,将紧邻路口间的曲线进行综合计算,得到整个交通网络的RTC模型.应用最小加代数方法,RTC模型能够计算车辆在路口的最长等待时间D和路口拥堵车队的最大长度B.基于RTC模型,应用MATLAB对8组不同规模的城市交通网格进行仿真,实验结果表明:(1)与双行道网络相比,单行道网络更能有效处理较稀疏的交通流.以定时控制为例,在车流频率u≤1/2时,单行道网络能够将交通拥堵指标D和B分别降低至少2.66倍和3倍;(2)双行道网络中,车流频率u存在一个临界区域,在临界域内,拥堵指标随车流频率递增变化,一旦u低于或超出临界域,拥堵指标则分别保持稳定不变或不可控;(3)自适应策略优于定时控制策略,例如在双行道网络中,自适应控制策略对应的拥塞指标D和B比定时控制策略分别降低1.68倍和1.26倍.

摘要:在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具SpaceDRC.实验结果表明,SpaceDRC能够在145ms内检测出约21400行程序中的真实数据竞争.SpaceDRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.

摘要:安全苛刻系统的可信性需求迫切,支持可信性评估的数据主要来自于测试.为了保证测试数据的可靠性和正确性,特别是对安全苛刻系统这类复杂系统,手工测试实际不可行.研发测试语言是实现自动化测试的有效途径,也是安全苛刻系统自动化测试发展的必然趋势.针对安全苛刻系统通用测试语言应独立于具体设备包括被测安全苛刻系统、测试设备的应用需求,对安全苛刻系统测试中的测试设备协同语句展开研究.针对安全苛刻系统测试中测试设备协同任务中的高阶性、实时性等特点,通过给出测试语言中测试设备协同相关类型、设备协同表达式,定义测试设备协同语句,并通过设备协同表达式求值定义设备协同语句的操作语义规则.最后,对语句的正确性给出相关证明,从而支持安全苛刻系统测试过程中测试设备协同过程的动态性和开放性,支持安全苛刻系统测试语言的通用性.

摘要:精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.

摘要:条件判定覆盖(condition/decision coverage,简称C/DC)准则是各种安全攸关软件测试中常用的测试覆盖准则,它要求软件测试覆盖程序中每个判定以及条件的真/假取值.现有的自动测试生成方法在针对该准则的测试用例生成过程中存在很多不足.例如:符号执行方法很难处理较为复杂的非线性条件约束,并在处理程序的规模上受到很大限制;希尔攀登法由于在搜索过程中易陷入局部最优,而难以达到满足C/DC准则的高覆盖率;模拟退火法和遗传算法依赖于用户使用过程中的复杂配置,测试用例生成效果具有一定的随机性.针对这一现状,提出了一种线性拟合制导测试用例生成方法.依据C/DC准则,该方法将程序中的每一个条件判定规范化为一个与零值比较的数值函数,并以插桩与执行获得该函数当前输入下的采样.通过拟合这些采样,能够逐步判断出程序中各个条件判定与输入的关系,并利用这些关系生成高覆盖率的测试用例.相对于传统方法,该方法具有参数配置简易、生成过程高效等优点,并且能够处理带非线性条件约束、逻辑复杂的程序.在3个开源软件库中的25个真实程序上运行的实验结果表明,所提出的方法比目前以覆盖率见长的遗传算法(genetic algorithm,简称GA)制导方法具备更好的覆盖能力与更高的执行效率.

摘要:能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用,但是由于现代处理器所使用的流水线、乱序执行、动态分支预测、Cache等性能提高机制以及多核之间的资源共享,使得系统的最坏执行时间分析变得非常困难.为此,国际学术界提出时间可预测系统设计的思想,以降低系统的最坏执行时间分析难度.已有研究主要关注硬件层次及其编译方法的调整和优化,而较少关注软件层次,即,时间可预测多线程代码的构造方法以及到多核硬件平台的映射.提出一种基于同步语言模型驱动的时间可预测多线程代码生成方法,并对代码生成器的语义保持进行证明;提出一种基于AADL(architecture analysis and design language)的时间可预测多核体系结构模型,作为研究的目标平台;最后,给出多线程代码到多核体系结构模型的映射方法,并给出系统性质的分析框架.

摘要:干涉问题是指基础程序和方面之间或者方面之间发生不需要的相互作用,导致最终程序中产生不想要的功能,危害程序的正确性.很难检测和修正在面向方面设计中存在的干涉,已经成为推广面向方面技术的阻碍.受到技术自身可扩展能力的局限,现有的基于模型验证技术的工作不能有效地处理功能干涉问题.设计开发了基于推理验证技术直接检查和去除面向方面设计中功能干涉的工具,它可以根据类和方面的功能规约自动产生确保不发生干涉的条件,并引入交互式证明工具PVS来提高证明过程的自动化程度.证明可以确认设计中无干涉存在或者为修正干涉问题提供线索.

摘要:栅栏函数在连续系统验证方面有着广泛的应用,其主要想法在于:在可达集和非安全集之间寻找一个栅栏,从初始区域出发的路径不会越过这个栅栏,而非安全区域在栅栏的另外一端.这样,就可以通过寻找栅栏函数来验证一个系统的安全性.近年来,已有一些工作讨论连续系统在无界时间情况下的栅栏函数生成.但是对于有些系统,人们可能只关心其在有界时间内的安全性.因为在无界时间内不安全并不能说明在给定时间内也是不安全的,所以对于这类问题,无界时间栅栏函数方法并不适用.受无界时间栅栏函数方法的启发,针对有界时间的情况,给出有界时间栅栏函数生成方法.首先给出有界时间栅栏函数的一些充分条件,对于多项式系统,将多项式非负的条件做平方和松弛后利用平方和规划工具求解这些充分条件得到栅栏函数;对于初等系统(包含一些初等函数),先将该初等系统转化为一个多项式系统,然后求解对应多项式系统的栅栏函数.对一些无界时间不安全的实例,演示了该方法在验证有界时间安全性问题上的有效性.

摘要:近年来,智能大厦的概念在国内外受到了高度的关注.相比于传统的建筑,智能大厦更加节能、舒适、易维护,已成为未来建筑的发展趋势.作为智能大厦空调通风系统的关键部分,空调系统及其调度策略决定了大厦整体的节能效果以及大厦中用户的舒适度.然而,由于智能大厦所处的环境具有许多不确定因素,极大地增加了空调系统调度策略设计与评估的复杂程度.因此,如何设计与评估不确定环境下空调系统的调度策略成为了智能大厦设计者面临的一大挑战.已有的方法主要针对智能大厦空调系统进行能耗与性能等方面的分析,但尚未有方法针对调度策略本身进行分析与评估.提出一种基于价格时间自动机的调度策略评估框架,支持对不确定环境下的智能大厦进行精确建模与定量评估.该框架使用UPPAAL-SMC作为属性查询引擎对模型进行随机模拟运行,根据模拟结果对不同调度策略下大厦的能耗及用户的舒适度进行定量分析.实验结果表明,该方法能够有效地帮助设计者进行策略的制定和选取.

摘要:由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTL^SL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(separation logic)与命题投影时序逻辑PPTL(propositional projection temporal logic),能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTL^SL的相关理论,并详细介绍了工具SAT-PPTL^SL的工作原理.该工具主要利用PPTL^SL与PPTL之间构建起来的同构关系进行PPTL^SL公式的可满足性检查.此外,结合一些实例展示了SAT-PPTL^SL的执行过程,并通过实验分析了关键参数对SAT-PPTL^SL执行效率的影响.

摘要:无穷数据广泛存在于计算机程序和数据库系统中.受到形式验证与数据库两方面应用需求的推动,面向无穷数据的形式模型已经成为理论计算机科学的研究热点之一.对面向无穷数据的形式模型(逻辑与自动机)进行了相对全面而详细的总结.主要按照不同自动机模型对无穷数据的处理方式加以组织,并关注相关判定问题,即:自动机的非空性问题、语言包含问题以及逻辑的可满足性问题的可判定性与复杂性.

摘要:排序学习技术尝试用机器学习的方法解决排序问题,已被深入研究并广泛应用于不同的领域,如信息检索、文本挖掘、个性化推荐、生物医学等.将排序学习融入推荐算法中,研究如何整合大量用户和物品的特征,构建更加贴合用户偏好需求的用户模型,以提高推荐算法的性能和用户满意度,成为基于排序学习推荐算法的主要任务.对近些年基于排序学习的推荐算法研究进展进行综述,并对其问题定义、关键技术、效用评价、应用进展等进行概括、比较和分析.最后,对基于排序学习的推荐算法的未来发展趋势进行探讨和展望.

摘要:精准地抽取新闻网页的内容,是提高Web新闻分析等应用系统工作质量的关键技术之一.由于缺少Web新闻出版的标准,存在大量不同的出版格式,并且Web本身是一种具有高度异构性的大数据载体,导致Web新闻内容抽取成为一个开放性问题.经大量实例分析发现,新闻网页内容与其上的标签路径存在潜在的关联性.因此,设计了标签路径特征系,以从不同视角区分网页内容和噪音.在特征相似性分析的基础上,提出了一种基于组合特征选择的特征融合策略,并设计了基于融合特征的Web新闻内容抽取方法CEPF.CEPF是一种快速的通用、无需训练的在线Web新闻内容抽取算法,可抽取多种来源、多种风格、多种语言的Web新闻网页.在CleanEval等测试数据集上的实验结果表明,CEPF方法优于CETR等抽取方法.

摘要:互联网的飞速发展,也使网络能耗急剧增长.但目前网络设备能效低下,未实现能耗比例计算的理念.而网络却为峰值负载而设计,在众多时间处于低负载,存在巨大的节能契机.首先介绍网络设备的能耗模型,继而从两方面阐述网络能耗优化的理论与技术:一方面,在假设网络总流量无法改变的前提下,为网络设备增加能源和性能状态,并优化本地控制策略,从而使单个网络设备实现能耗比例计算,或者在不提高现有网络设备能效的前提下,通过网络范围的协同和流量工程,使网络整体实现能耗比例计算的理念;另一方面,为网络提供缓存能力可以降低或缓解网络流量,从而减少网络的传输能耗或缓解其增长速度,智能的缓存部署、内容存储和请求路由能够进一步优化网络的能耗.在上述基础上,比较了各种技术的优劣,并分析了未来的研究方向.

摘要:对公钥密码体制的密码分析历史的形成,给出一些重要结果的描述和重要文献的历史发展线索,同时对2010年~2014年有限域和椭圆曲线的离散对数问题的突破性进展给予了简单介绍.自公钥密码学1976年诞生以来,公钥密码体制的密码分析已经发展成为非常庞大的多学科交叉研究领域,希望可以给同行和学习密码学的研究生进入该领域起到帮助作用.