基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

基于SMT求解器的路径敏感程序验证

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.     

输气管线的分布参数数学模型及工程应用

本文研究了用传递函数描述长距离输气管线这种分布参数调节对象的布法.长距离输气管线输送的是可压缩的天然气,表征其动态特性的偏微分方程组较复杂.本文所用方法是将其偏微分方程组经拉普拉斯变换,由时域变为频域,直接求解以管线长度为变量的线性变系数微分方程--贝塞尔方程,从而得到描述这种分布参数调节对象动态特性的传递函数.将此传递函数经数学处理,得到工程实用的简洁形式,并给出其频率特性曲线和动态响应过程.     

地下管线巡检维护管理系统的设计与实现

基于浏览器/服务器架构,结合GIS、WEB、定位和数据库等技术,针对地下管线巡检、维修和抢险工作的特点,设计一套地下管线巡检维护管理系统。该系统改变了地下管线巡检工作的传统方式,大大提高管理质量和效率,为地下管网安全运营提供有力的技术保障,适用于市政工程行业对地下管网及其附属设施的日常维护和管理,具有广阔的应用前景。     

利用GIS技术实现电信管线的管理与维护

通过地理信息系统技术的运用，实现对电信管线高效的管理与维护。本文详细阐述了系统开发技术及主要功能并给出关键问题的解决方法。     

基于仿真模型的蒸汽管网故障诊断研究

运用先进的化工工艺流程模拟软件PipePhase建立蒸汽管网的仿真模型,对管道泄漏、保温层因腐蚀而导致保温性能降低两种故障进行仿真试验,建立起诊断知识库,综合运用流量平衡法对两种故障进行诊断,并基于压力梯度法提出了一种解直线方程组的方法对泄漏进行定位,最后得出了故障诊断总体方案流程图。     

非交互式Petri网可覆盖性验证的高效实现

近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中.然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况.而Petri网的一个子系统——非交互式Petri网,其可覆盖性和可达性复杂性均是NP完备的,同时表达力又可以作为某类并发程序的验证模型.设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV.采用基于约束的方法,从模型中提取约束,并使用Z3 SMT求解器对约束进行求解,同时,通过子网可标记方法对候选解进行验证,从而保证每组解都是正确解.通过实验分析了该工具的成功率、迭代次数以及运行效率,发现该算法不仅验证成功率高,而且性能非常优异.     

液体管道的泄漏仿真

为了找出管道参数的动态变化规律,基于管道的机理模型,通过引入附加边界条件,对泄漏量、泄漏位置和泄漏上升时间对管道内参数的影响进行仿真。结果表明,其他两个因素保持不变的条件下,泄漏量主要影响管道参数的幅值,泄漏上升时间主要影响其波形,泄漏位置会同时影响其幅值和波形,而管道泄漏量和孔的大小及其位置密切相关,而且泄漏管道参数具有和停泵显著不同的特征,可以为运行指导、泄漏检测和人员培训提供必要的辅助手段。     

NC图形验证与仿真技术的研究概况

数控程序图形验证与仿真技术的研究对保证加工质量提高加工效率具有重要意义,同时也是虚拟制造技术的主要研究内容之一,该文从国外NC几何验证、NC物理验证以及我国的NC图形验证三个方面对NC图形验证技术的发展概况作了较全面的论述,并指出其中存在的不足和尚待解决的问题。最后提出一种新的复杂曲面NC图形验证的体系结构。     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.     

基于SMT求解器的微处理器指令验证数据约束生成技术

处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法：利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法：首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益.     

基于一阶逻辑的可满足求解方法研究进展

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。     

微处理器功能验证方法研究

微处理器验证是微处理器设计的关键环节。该文探讨了微处理器模拟、硬件仿真、形式验证等方法的原理、特点和适用场合,提出了进行多层次微处理器功能验证的总体思路。     

基于信号特征参数的复杂体制信号全脉冲数据动态生成技术

全脉冲数据在电子侦察处理中具有重要价值,为逼真模拟电子侦察接收机在真实信号环境下接收的全脉冲数据,提出了一种复杂体制信号的全脉冲数据动态生成技术;该技术综合考虑了天线方向图、天线扫描方式、空间传输衰减、信号时频特性、信号到达时间、脉冲交错等因素对全脉冲数据产生的影响,可基于信号特征参数(载频类型、载频变化范围等)动态产生载频捷变、脉冲重复间隔参差等各类复杂体制信号的交错全脉冲数据流;测试和验证表明,该技术可适应各类复杂体制信号全脉冲数据流产生,具有逼真性高、适应性强、可扩展性强的优势。     

Automated Verification of Signalling Principles in Railway Interlocking Systems

In this paper we present a verification strategy for signalling principles for the control of a railway interlocking system written in ladder logic. All translation steps have been implemented and tested on a real-world example of a railway interlocking system. The steps in this translation are as follows: 1. The development of a mathematical model of a railway interlocking system and the translation from ladder logic into this model. 2. The development of verification conditions guaranteeing the correctness of safety conditions. 3. The verification of safety conditions using a satisfiability solver. 4. The generation of safety conditions from signalling principles using a topological model of a railway yard.     

龙芯2号微处理器的功能验证

开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务.龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍,如何保证设计的正确性是一个重大挑战.简单的系统级测试已经不能满足设计的需要,这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误.主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法.模拟仿真是主要的验证手段,新的形式化验证方法也应用到了验证流程当中.