基于逻辑的形式化验证方法: 进展及应用

近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。     

B方法在PVS中的应用

针对B方法和原型验证系统(PVS)的特点,提出了将B方法引入到PVS中,即将一个用B方法描述的系统转换为由PVS描述,以此来实现形式化的检验证明.B方法中的抽象机在PVS中转换为一个方法,而B方法中的不变量不变式要转换为PVS中的一个类型,由B方法描述的性质则转换为PVS中的推测、猜想,并借助于PVS自带的证明器有效地完成相应证明工作.最后,通过1个电梯控制系统来阐述上述转换方法.     

面向SOA架构分布式系统的会话交互建模及其安全验证

研究了SOA架构分布式系统在基于社区的Web服务动态会话交互的安全性,提出了一种基于形式化规格说明的Web服务组合行为建模和验证框架.基于OWL-S描述的若干个Web服务的组合和交互的安全性保障问题,构建了一种基于WS-Trust和WS-Secure Conversation规格的安全会话验证方法.该方法首先将Web服务组合行为建模为带有标签的迁移系统AKTS来描述服务的观察行为;进而将安全会话约束翻译为DPDL公式即将SOA系统的会话安全性验证问题规约为保障安全会话约束的前提下的Web服务组合行为的满足性问题;最后通过经典算法在有效时间内得到该满足性问题的验证.该框架为基于SOA架构的分布式系统的交互安全提供了理论支持和保障,在安全关键的分布式系统设计阶段及早发现安全隐患,节约了开发成本、提高了系统安全性.     

硬件设计的形式化验证技术

形式化验证用数学可证明的方式来验证系统.硬件设计的形式化验证通常有三种方法：定理证明、等价性检验和模型检验.文章着重分析了这三种方法的优缺点，探讨了形式化验证技术所面临的挑战，以及目前形式化验证技术可能的一些研究方向.     

Lebesgue积分在PVS中的证明分析

为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用Lebesgue积分的运算特征在PVS定理证明器中进行形式化证明与分析.主要对其分裂定理、不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则和极限定理等多个方面进行了形式化,且依据数学定理与推论形式化,说明Lebesgue积分在PVS中的形式化是可行的、有效的.以标准反相积分器为应用模型,对其通用电路原理与机制进行了形式化证明,通过数理分析测试了本文Lebesgue积分形式化定理库的正确性.     

基于Z语言的互联网登陆系统的形式化规格与验证

Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可产生精确地需求规格说明.本文用形式化语言Z对互联网登陆系统的主要操作模式进行规格说明,接着通过形式化验证,证明设计的规格说明能够满足用户的需求,提高了系统的可靠性和稳定性.     

基于PVS的数据库安全策略形式化分析方法

基于安全策略模型的形式化分析对于数据库管理系统达到高安全保障等级的重要性,提出了新的基于PVS的数据库安全策略模型分析方法,该方法结合了PVS函数式语言的特点,通过一系列算法和流程展示了模块化的系统状态、安全属性、操作规则的定义过程.借助PVS定理证明器对BeyonDB数据库管理系统进行安全性分析,结果表明,该方法不但能够提高形式化建模效率,而且可以有效地发现系统设计中存在的漏洞.     

基于模式识别的Lebesgue积分在PVS中的形式化证明与分析

针对传统模型验证方法存在效率低和模型较为复杂的缺点,将Lebesgue积分的运算特征引入模型验证和测试,提出一种基于Lebesgue积分的形式化验证和测试方法。通过不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则以及极限定理等方面的形式化,实现Lebesgue积分的运算特征在PVS(Prototype Verification System)定理证明器中的形式化。以标准反相积分器为应用模型验证数学理论和公式推导的正确性,通过数理分析验证Lebesgue积分形式化定理库在计算机信息安全领域应用的正确性。测试结果证明了Lebesgue积分在PVS中进行形式化的可行性和有效性。     

概率模型检验的CBTC系统通信协议的形式化验证

通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.     

PLC程序形式化的设计与验证

从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.     

卫星定位系统的验证原型

用模型检查的方法对卫星定位系统进行了验证,对把模型检查应用于实际系统进行了初步的探索。     

基于人工神经网络的病症诊断原型系统

知识获取是目前专家系统和知识库系统的“瓶颈”问题。解决这个问题的关键在于知识的自动获取方法的实现，也就是希望能够达到智能获取。这里以知识库系统理论为基础，在中医医案的研究中，实现对病症推断的自动获取，探讨知识获取实现的方法，研究人工神经网络的BP算法的应用。     

控制系统快速原型设计方法

利用RT-LAB快速原型开发平台生成空空导弹控制系统快速原型,实现数字/半实物仿真的一体化设计开发和测试环境。快速原型技术可以克服空空导弹控制系统传统开发流程的弊端,快速完成控制系统的性能分析、建模、仿真。     

Brief Introduction of TianHe Exascale Prototype System

Facing the challenges of the next generation exascale computing, National University of Defense Technology has developed a prototype system to explore opportunities, solutions, and limits toward the next generation Tianhe system. This paper briefly introduces the prototype system, which is deployed at the National Supercomputer Center in Tianjin and has a theoretical peak performance of 3.15 Pflops. A total of 512 compute nodes are found where each node has three proprietary CPUs called Matrix-2000+. The system memory is 98.3 TB,and the storage is 1.4 PB in total.     

服务资源一体化发现原型系统

资源和服务的获取是当前互联网最主要的两种应用,几乎所有的网络活动都需要两者的支持.现有的服务或资源发现系统均是单独存在的,它们很少考虑服务与资源两者之间的关系.为了给用户提供更便利、一体的服务与资源查询处理机制,并能减少服务和资源两套处理系统带来的网络资源浪费,本文充分利用服务与资源两者之间的关系,发掘出两者之间的联系,提出并设计了基于语义的服务资源一体化发现原型系统.实验结果表明,服务资源一体化发现方法与传统的发现方法相比,提高了用户的满意度.     

军事文本标图系统的设计与原型实现

军事文本标图的概念，指由机器对指挥人员口授生成的文本进行分析，在相关地理信息平台上自动生成军事标图的过程。针对军事文本标图的需求和汉语语言的特点，提出了一套综合利用多种自然语言处理技术和机器翻译方法的完整的面向受限领域的“类”机器翻译解决方案，设计出一个受限领城内的军事文本标图系统。     

A Prototype of CAPP System for Rotational Parts

Noticing in recent years that the world is running out of mineral resources, the price of engineering materials will continually rise in the future, the percentage of the cost of manufactured part that is due to the cost of materials is also rising. The amount of material must be removed away to produce the final product should be minimized, excess stock will increase not only the material cost, but also processing cost, fixture cost, tooling cost, and increases machine cycle times. This paper proposed a va...     

AskTheWeb--一个基于Web的问题回答原型系统

问题回答(Question Answering,简称QA)系统是当前检索等领域的研究热点之一,其目标是回答用户用自然语言提出的简单问题.文中给出了一个基于Web的中文QA原型系统--AskTheWeb的设计与实现机制.AskTheWeb利用搜索引擎获取相关网页,而后基于综合词频统计和概念的评分模型从这些网页中提取答案.文中给出的评测数据,验证了使用数据密集的思想实现基于Web的中文QA系统的可行性,而概念匹配技术对答案精度的提高有促进作用.     

FAST观测管理系统设计与原型实现

位于贵州省平塘县的500 m口径球面射电望远镜(FAST)建成后将是世界上最大最灵敏的单口径射电望远镜。为提高望远镜的观测效率和易用性,设计了观测管理系统来优化观测序列和监控观测过程。采用原型迭代开发方法进行了系统设计及原型实现。本文详细阐述了基于观测场景的业务流程分析和观测调度策略、观测翻译等关键设计。然后在4.5m射电望远镜上测试了原型的实现效果,验证了系统设计的可行性,为完整系统的开发提供借鉴。     

光学过程层析成像技术及其原型系统

提出了一个用于两相流参数检测的红外激光过程层析成像原型系统,并对系统的结构、算法、性能以及特点进行了分析.模拟实验结果表明,光学过程层析成像技术可以获得高成像速度和分辨率,是一种有发展潜力和应用前景的多相流参数检测技术.