Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm

The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.     

主动式活塞体积管流量标准装置阶跃特性研究

动态流量测量在研发和生产过程中越来越重要,为了开展流量计的动态响应特性相关试验,使用激光干涉仪对燃油流量标准装置的活塞位移进行了动态测量,并分析了该装置的阶跃特性。试验结果表明,在一定阶跃流量范围内,该装置的时间常数在7~60 ms之间。建议进一步优化装置的传动结构和伺服控制参数,改善装置的阶跃特性。     

可由用户持续发展的几何自动推理平台的推理算法

目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法,初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识,如几何对象、谓词和规则,并可以综合使用多种推理算法,如前推搜索法和一部分面积法,它将更适合用于几何教学。     

A New String Matching Algorithm

In this paper a new exact string-matching algorithm with sub-linear average case complexity has been presented. Unlike other sub-linear string-matching algorithms it never performs more than n text character comparisons while working on a text of length n . It requires only O ( m +σ) extra pre-processing time and space, where m is the length of the pattern and σ is the size of the alphabet.     

安全协议的形式化需求及验证

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。     

标准体积管检定过程中的误差来源

着重介绍了容积法（称重法）检定标准体积管和用标准体积管检定计量体积量（质量）流量计的检定原理及其检定修正公式的理论分析，以及在实际检定过程中各种误差的来源分析，消除或减小各种误差的有效方法。     

Gas Oil Piston Prover,primary reference values for Gas-Volume

The paper describes the design, measurement results and uncertainty analyses of the hydraulic driven piston-prover system which has been in operation at VSL since 2008. The 12-meter long, 0.6 m bore piston-prover is used for the realization of Reference Values for Gas-Volume at pressures between 1 and 65 bar(a) at several gases. The principle is based on the displacement of a piston acting as a Gas–Oil separator. The standard has a flow-rate range from 5 to 230 m³/h. The system is designed to calibrate reference meters. The Calibration and Measurement Capability (CMC) of the system is proven to be smaller than 0.1% (k=2). The paper also explains the coherence between the Gas–Oil piston-prover and other traceability generators and ‘flow rate bootstrapper systems’.     

断言语言支持自定义谓词的程序验证器原型

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.     

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.     

基于复数法的几何定理可读机器证明

已有的机器证明方法在处理一些涉及大规模符号运算的几何问题时,常因算法复杂度过高或机器能力的限制,有时并不能在合理时间内实现可读机器证明. 故提出了复数法这一新的几何定理机器证明算法,并选用符号计算功能较为强大的软件Mathematica创建了新证明器CNMP(complex number method prover).新提出的复数法能有效地解决构造型几何命题,对用于测试与评价几何定理证明器性能的综合性平台TGTP(thousands of geometric problems for geometric theorem provers)上的180个几何问题的实验结果表明,CNMP的解题能力与运行效率均令人满意.尤其是对于一些具有相当难度的几何定理,如五圆定理、Morley定理、Lemoine圆定理、Thebault定理、Brocard圆定理等,CNMP均能在短时间内给出可读机器证明.