高阶逻辑验证系统HOL及其应用初探

形式化方法在硬件、软件的设计和验证中的应用越来越广泛,基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍,并结合例子说明HOL系统在硬件设计中的应用。

正则表达式与有穷自动机等价性在Isabelle/HOL中的形式化

针对正则表达式和有穷自动机,在机器辅助定理证明系统Isabelle/HOL中进行了形式化描述。通过对语言、正则表达式、确定和不确定有穷自动机在Isabelle/HOL中建立模型,定义了它们之间的相互转换函数并证明了这些函数的正确性,从而验证了正则表达式和有穷自动机在描述能力上的等价性,即:在同一有限字母表下,对任意正则表达式,都存在一个有穷自动机,使得二者描述的语言相同;反之亦然。通过分析与证明,表明采用机器辅助定理证明系统,对计算理论传统核心领域之一的自动机理论进行分析和证明是可行的。

文件比较算法fcomp在Isabelle/HOL中的验证

基于机器定理证明的形式验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法(file comparison algorithm)是一类成员众多,应用极为广泛,跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法.在交互式定理证明器Isabelle/HOL中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp做了形式化,改正了算法关于边界变量迭代的一个小错误,证明了改正后算法的可终止性和正确性;对算法时间复杂性做了完全形式化的分析,印证了算法的非形式化分析结论,为今后更多文件比较算法的形式验证提供了可供借鉴的经验.

SAODV协议在Isabelle/HOL中的正确性验证

将SAODV(secure Ad-hoc on-demand distance vector routing)协议的正确性性质划分为安全性性质和活动性性质。前者是指SAODV发现的路由具有某些期望的性质,如无环路等;后者是指节点一定能够找到合适的路由,并利用其成功传送数据。很多移动自组网路由协议的形式化验证工作关注安全性性质,而活动性性质却被忽略了。利用Paulson归纳法来描述SAODV协议并验证其安全性性质,扩展Paulson归纳法描述和验证SAODV的活动性性质。所有定义和推理都是在机器辅助定理证明工具Isabelle/HOL/Isar中进行的。

电梯控制系统在Isabelle/HOL中的活动性证明

电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统,利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。

ATM交换机输入缓存队列HOL阻塞研究

1.概述 在ATM交换机制中,输入缓存无阻塞交换技术成为提高交换效率的一个重要因索.输入缓存交换网的主要问题就是存在HOL(head of ine,队头)阻塞,即位于输入缓冲区H0L之后的信元,由于FIFO(first in,first out,先进先出)缓冲区HOL信元的阻塞,既使当前时隙该信元指向的输出端口处于空闲状态,也无法在此时隙参与交换的现象.为了解决这一问题,已经提出了许多排队方法及其调度规则,大致可概括为如下几类:(1)滑动窗口法:在一个信元交换时隙内,依秩观测并处理一个FIFO队列中前K(K＞1)个信元,从中选取一个满足交换条件的信元参与交换连接,以此消除HOL阻塞[1];(2)在每个输入端口设置与网络输出端口数相同的多输入缓冲队列,以此消除HOL阻塞[2];(3)使用不同连接调度算法,如神经网络或迭代算法,以使吞吐率达到最大[3].本文研究输入端口具有多FIFO队列、内部无阻塞的N×N交换网络,采用一种合理的机制,以求消除HOL阻塞,提高交换效率.

VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.

命题演算形式系统在Isabelle/HOL中的形式化

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle/HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明。通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。

基于Isabelle/HOL的离散数学实验教学设计与实践

传统的离散数学实验教学,通常使用C、C++等程序设计语言来完成相应的课程验证性实验.学生在花费大量的时间和精力完成程序设计后,依然对程序的正确性没有直观的认识.借助Isabelle/HOL交互式定理证明器工具和形式化方法,构建离散数学实验环境,解决离散数学课程实验教学的直观表达问题以及逻辑推理实验的设置.以二叉树这种离散结构的知识点学习为例,阐述如何使用Isabelle/HOL来完成“离散数学”课程的实验教学设计.通过这种实验教学,能使学生对逻辑演算和推理有清晰的认识,同时培养学生的数学和逻辑思维以及创新、应用能力.

基于HOL4的形式化方法

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.

用多FIFO输入缓冲队列消除HOL阻塞

对于输入端口具有单输入FIFO(先入先出)队列的输入缓冲信元交换机(如 ATM),影响交换吞吐率的主要因素是信头阻塞(HOL)。本文分析了在单FIFO队列情况下的信元阻塞的原因及解决办法,给出了输入端口具有多FIFD队列的信元交换结构,描述了基于N-FIFO输入缓冲的排队策略和迭代匹配算法,并对它们的性能进行了分析。

Gauge积分在HOL4中的形式化

积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则,并根据相关性质对反相积分器进行了验证。

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.

HELMHOLTZ FREE ENERGY IN A SYSTEM OF ANISOTROPIC CHAINLIKE MOLECULES AND ITS APPLICATIONS FOR NORMAL MONOHYDRIC ALCOHOLS AND NORMAL ALKANES

1 INTRODUCTIONAfter Prausnitz et al.published the perturbed hard-sphere chain theory(PHCT),manymodified theories have been put forward,such as the perturbed soft-sphere chain theory(PSCT),the perturbed anisotropic chain theory(PACT)and the associated perturbedanisotropic chain theory(APACT).These theories are all concerned with the parameter3c.But,Wertheim in his work proved that the free energy of hard-sphere chain couldbe calculated without 3c.Induced by the work done by Wertheim,Chapman

拉普拉斯变换微积分性质在HOL4中的形式化

拉普拉斯变换是系统时域频域分析转换的基本工具,基于拉普拉斯变换的数值计算广泛用于信号传输的评估和重要安全系统的分析等,但是其存在计算不精确等问题.高阶逻辑定理证明是验证系统的一种严密的形式化方法.本文在高阶逻辑证明工具HOL4中使用积分、微分、超越函数、复数等定理建立了拉普拉斯变换形式化模型,并且对拉普拉斯变换的线性性质、微分性质、积分性质、频移性质进行了逻辑推理证明.最后通过对电机传递函数的形式化验证说明拉普拉斯变换形式化的有效性和正确性.

实数二项式系数在HOL4中的形式化

定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。

一种基于Isabelle/HOL的安全通信协议验证方法

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。

基于缓解HoL堵塞的单组播混合调度算法

针对联合输入交叉队列(CICQ)结构的单组播混合调度研究不多,且没有针对性研究头分组(HoL)堵塞问题,提出了以缓解HoL堵塞为目标的一种新的单组播混合调度算法,即单组播低Ho L堵塞(MULHB)算法,使交换机尽量逼近work-conserving状态。该算法还充分考虑了单组播之间的差异性,利用权重裁决单组播之间的竞争,避免"饿死"现象发生。同时,还给出了一种新的组播分组入队算法,即动态组播分组入队(DMQ)策略,该策略在不乱序的前提下,允许新到达分组选择合适的队列入队。仿真结果表明,在不同业务下,DMQ-MULHB算法的通过率及平均时延均优于现有主流的单组播混合调度算法,尤其在非均匀业务下,该算法性能接近输出排队(OQ)调度。

堆栈机器简单编译器在Isabelle/HOL中的验证

堆栈机器(stack machine)作为一种计算模型,不仅执行部分高级语言的效率很高,而且其编译器也简单、快速.在形式化领域,目前已有不少定理证明器用来验证模型的正确性.本文对堆栈机器的简单编译器进行介绍,对布尔表达式和算术表达式、机器指令、编译器、机器运行行为在Isabelle/HOL中进行形式化,验证编译器的正确性.

基于Isabelle/HOL的安全操作系统形式化验证方法

操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况。