基于约束依赖图的并发程序模型检测工具

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.     

基于模糊约束规划的自动协商

给出了一个基于模糊约束规划模型的自动协商系统。建立了模糊约束规划模型并利用模糊模拟、神经网络和遗传算法给出了求解Pareto最优解的混合智能算法;协商过程中卖方智能体根据神经网络拟合的效用函数并运行混合智能体算法得到当前协商步的Pareto最优解,避免了对大型商品数据库的反复搜索,为系统推向实际应用奠定了基础;协商模型仿真实验表明了协商系统返回的解与实际调查得到的用户偏好相一致。     

基于变约束规划模型的炼钢连铸动态调度

针对炼钢连铸生产过程中时常出现各种扰动, 采用人工调度存在反应慢、调度结果不优化的问题, 在分析各种调整方式基础上, 建立了在线调整非线性规划模型, 通过约束变化满足不同的调整方式要求, 并将模型转化为线性规划模型后对其进行求解. 在国内某大型钢厂应用结果表明: 采用该方法在缩短动态调度时间、减少钢水冗余等待时间、提高设备负荷率方面取得显著成效.     

基于线性约束规划问题的神经网络模型

提出了一种基于梯度投影矩阵下的求解线性约束下规划问题的神经网络模型,并导出了线性约束下规划问题的稳定解法,该网络模型既适合于求解线性约束下线性或非二次规划问题,又适合于求解线性或非线性方程组,与其它规划问题的神经网络相比,更具有一般性。     

基于本体的智能规划方法研究及应用

针对经典智能规划方法在利用领域知识方面存在的不足,将先进的知识工程方法与通用智能规划算法相结合,提出了一种新型的基于本体的智能规划技术,它能够综合利用本体知识库中的领域知识对特定领域问题进行合理高效的规划求解,同时给出了一套构建用于支持这类规划过程的领域知识本体库的实用方法。实验结果表明,该方法能够有效地解决复杂的实际应用问题,使由此建立的规划系统真正达到实用水平。     

基于特定入侵检测问题的规划识别模型的研究

该文在特定的入侵检测问题中,对于规划识别技术进行了初步研究,提出了基于特定入侵检测问题的规划识别模型。     

基于约束分析与模型检测的代码安全漏洞检测方法研究

与传统的程序分析相比,模型检测具有较高的检测精度,但无法将其直接应用于缓冲区溢出、代码注入等安全漏洞的检测.为解决此问题,提出了基于约束分析与模型检测相结合的安全漏洞自动检测方法.首先,通过约束分析跟踪代码中缓冲区的信息,在涉及缓冲区操作的危险点生成相应的属性传递和属性约束语句,并将安全漏洞检测问题转化为模型检测方法可接受的可达性检测问题.然后,采用模型检测方法对安全漏洞的可达性进行判断.同时采用程序切片技术,以减少状态空间.对6个开源软件的检测结果表明,基于该方法实现的CodeAuditor原型系统发现了18个新漏洞,误报率为23％.对minicom的切片实验显示,检测性能有较大提高.     

基于约束规划的一类排序问题通用求解方法

多约束排序问题是生产调度中常遇到的问题,传统的优化模型及方法在适应约束改变等方面存在诸多不足。鉴于此,将多约束排序问题定义为约束满足问题,系统设计时将模型定义与求解算法分离,利用约束规划平台的基本约束构建特定领域的抽象约束库,形成可重构的多约束排序问题通用求解框架。应用时,根据问题需求不同可利用抽象约束库快速重构优化模型,针对重构的优化模型配置相应的求解算法即可实现问题求解。应用结果表明,提出的方法通用性强,可满足实际应用的要求。     

自动获取派生谓词规划领域的通用规划

通用规划(解)是针对某个领域的像算法一样的规划解,通过对其的解释可以直接得出具体问题的规划解,而不需要调用任何规划系统.但是目前通用规划的提取只能在一些简单或者特殊的领域中进行,没有推广到复杂或者一般的规划领域.该文提出在包含派生谓词的规划领域自动获取通用规划的方法.与已有获取方法不同的是:首先,基于派生谓词规则,文中方法明确指出派生谓词目标与动作效果之间的依赖关系,用以完善通用规划中动作应用的目的;其次,在提取过程中借助角色来帮助识别规划解中的循环结构.实验结果表明,文中方法不仅容易在派生谓词规划领域中获取通用规划,而且还能够以较好的性能求解一类以派生谓词为主要目标的规划"难"题.该文是在派生谓词规划领域中提取通用规划的首创性工作.     

基于规划识别的入侵检测研究

规划识别是人工智能的重要研究分支之一,在入侵检测领域中已有初步的应用。本文在介绍规划识别和入侵检测基本概念的基础上,按照规划识别方法分门别类地研究了基于事件层的规划识别、基于贝叶斯网络的规划识别、基于扩展目标规划图的规划识别、彩色Petri网、对手规划、行为状态图等在入侵检测领域的应用现状和进展;接着深入分析了规划识别和入侵检测的关系和相似之处;最后讨论了基于规划识别的入侵检测存在的问题,并指出了未来的发展趋势。本文综述了智能规划在入侵检测中应用的关键技术和存在的问题,研究内容对于相关人员从事入侵检测研究具有重要的参考价值。     

基于模型检验的规划综述

基于模型检验的规划是当今通用的规划研究的热点,其求解效率比较高.详细阐述了基于模型检验的规划的发展与研究现状.介绍了基于模型检验的规划的基本框架,分别阐述了模型检验技术在规划领域的重要应用,并介绍了两种典型的基于模型检验的规划工具,分析了今后的发展趋势.     

领域知识优化的蚁群规划算法

在智能规划领域的传统图规划算法中,规划解的提取是从规划图的最后一层不断向前提取。提取过程中要不断进行大量状态互斥判断。提取过程中一旦发生失败就要回溯,即使再遇到相同的互斥情形也要重新计算,大量判断互斥的计算被带入主循环搜索过程,极大地影响了搜索效率。将领域知识通过禁忌连接集的形式加入蚁群规划算法中,相邻动作层的很多互斥信息通过禁忌连接集只需计算一次,不带入主循环计算中,可以较好地提升算法的执行效率,实例分析表明这一策略是有效的。     

基于约束的并行工程产品开发过程规划

本文分析了并行工程产品开发过程中约束的特点,探讨了不同类型约束对产品开发过程规划的不同影响,提出了基于设计约束的过程规划原理推理算法,开发过程活动的划分算法和信息预发布点的选取准则;从整个产品生命周期角度,给出了基于约束的产品开发过程规划的方法和步骤。     

领域信息提取的缩规划图算法

传统的图规划技术在处理规模较大的智能规划问题时,由于计算量的递增爆炸,导致算法在规划问题上容易出现效率瓶颈。对图规划技术进行了一些改进：（1）加入领域信息的动态提取和使用;（2）提出了缩规划图的概念和算法,通过引入基于领域信息的启发式函数,对不同的扩展分支进行优选排序,剪除一些执行希望小甚至不合理的扩展分支,从而提高了系统执行效率。实验表明该策略是有效的。     

一种基于模型的特征交互检测方法

为了适应业务的不断更新,许多软件系统通过向公共的基础系统插入新的扩展来实现演化.这种演化策略虽然有利于并行开发和部署,但也面临着扩展间可能发生非预期特征交互的问题.目前,形式化方法在检测特征交互问题方面仍然是最有效的方法之一.这类方法着眼于检测扩展之间是否会发生冲突.虽然在小规模实验上较为成功,但是它们也面临着一些挑战.例如:扩展的非单调性、扩展组合的激增以及扩展模型可能无法获知的问题.实际上,许多特征交互都源于新扩展对基系统和已有扩展造成的不恰当影响.基于这种认识,集中关注由于扩展的不恰当影响所导致的交互冲突问题,提出了如何从已知的特征交互实例来分析产生冲突的原因的具体方法,并说明了如何制定约束以限制扩展中易导致冲突的行为,从而预防同一类行为可能导致的各种冲突.该方法被应用到电信系统特征交互的分析上,实验结果表明,大部分特征交互中导致冲突的行为都可以被检测出来.该方法不仅能够保证原有基系统或扩展模型的稳定、有效,避免扩展组合带来的问题,而且它无须公布扩展的模型细节.     

模型检测在软件测试中的应用

随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。在为此提出的诸多理论和方法中,模型检测（model checking）以其简洁明了和自动化程度高而引人注目。具体介绍了模型检测的一些理论,同时将它应用于具体的软件程序,运用模型检测方法对软件进行测试。从而证明了模型检测方法与测试结合对于软件可靠性和正确性所起的巨大作用。     

智能规划器StepByStep的研究和开发

智能规划器是智能规划研究成果的重要表现形式,规划器的求解效率和规划质量是智能规划理论研究的直接反映.首先介绍智能规划器的一般结构和StepByStep规划器的总体结构,然后详细阐述StepByStep规划器各组成部分所采用的方法和策略,定义谓词知识树来提取领域知识.在谓词知识树的基础上定义谓词规划树,并用各种策略来提高规划树的生成效率.在谓词规划树的基础上设计StepByStep的规划策略,最后用8个规划器对3个具有代表性的基准规划领域及其规划问题进行实际的求解实验,分析了StepByStep规划器在求解效率和规划质量上的具体表现.实验数据表明,StepByStep规划器的规划策略对3个不同规划领域都具有很好的指导作用,验证了领域知识在规划求解过程中的实际价值.     

不确定规划中的多Agent带权值强规化算法

在智能规划领域中,以往对不确定规划问题的研究主要集中于单个Agent,而对多Agent规划的研究则侧重于确定规划。针对该问题,提出基于多Agent的带权值不确定规划问题,对所求解的强规划解,设计使其所需动作权值总和近似最小的算法。根据基于模型检测的强规划分层方法,对每个Agent进行强规划分层,合并所有Agent的分层信息,并在合并的过程中得到同层状态之间的冲突表。在保证冲突最小的情况下,以最小动作权值优先的贪心方法,求出强规划解。实验结果表明,该算法能较快地求解出使所选择的动作权值总和近似最小的强规划解。     

基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.     

一个改进的基本方向约束一致性的判定算法

基本方向约束的一致性判定是定性空间推理中的基本问题之一。本文采用将基本方向约束集转化成有向图的方法,给出了一致性判定的相关结论,并据此在Skiadopoulos算法基础上提出了一种改进算法。新算法不但能判定出所有导致不一致的约束子集,而且还提高了执行效率。