基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。     

Formalization of the Standard Uniform random variable

Continuous random variables are widely used to mathematically describe random phenomena in engineering and the physical sciences. In this paper, we present a higher-order logic formalization of the Standard Uniform random variable as the limit value of the sequence of its discrete approximations. We then show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover, summarizing the proof steps. The formalized Standard Uniform random variable can be transformed to formalize other continuous random variables, such as Uniform, Exponential, Normal, etc., by using various non-uniform random number generation techniques. The formalization of these continuous random variables will enable us to perform an error free probabilistic analysis of systems within the framework of a higher-order-logic (HOL) theorem prover. For illustration purposes, we present the formalization of the Continuous Uniform random variable based on the formalized Standard Uniform random variable, and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.     

Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem

There are many papers describing problems solved using the Boyer-Moore theorem prover, as well as papers describing new tools and functionalities added to it. Unfortunately, so far there has been no tutorial paper describing typical interactions that a user has with this system when trying to solve a nontrivial problem, including a discussion of issues that arise in these situations. In this paper we aim to fill this gap by illustrating how we have proved an interesting theorem with the Boyer-Moore theorem prover: a formalization of the assertion that the arithmetic mean of a sequence of natural numbers is greater than or equal to their geometric mean. We hope that this report will be of value not only for (non-expert) users of this system, who can learn some approaches (and tricks) to use when proving theorems with it, but also for implementors of automated deduction systems. Perhaps our main point is that, at least in the case of Nqthm, the user can interact with the system without knowing much about how it works inside. This perspective suggests the development of theorem provers that allow interaction that is user oriented and not system developer oriented. This research was supported in part by ONR Contract N00014-94-C-0193. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Office of Naval Research, or the U.S. government.     

Fast string matching using an n-gram algorithm

Experimental results are given for the application of a new n-gram algorithm to substring searching in DNA strings. The results confirm theoretical predictions of expected running times based on the assumption that the data are drawn from a stationary ergodic source. They also confirm that the algorithms tested are the most efficient known for searches involving larger patterns.     

钟罩装置标准容积的数学模型研究与建立

在钟罩装置标准容积实测数据的基础上,通过描点图定性分析了钟罩罩体高度和半径的关系特性,提出采用傅里叶级数建立数学模型,借助Matlab获得理想的函数方程,并分析了其拟合标准差。实际应用中采用光栅尺测量钟罩下降的高度,运用定积分原理对函数进行积分获得钟罩下降任意高度时排出的气体容积值,在瞬时流量下限标准容积的相对扩展不确定度达到4×10^-4(k=2),相对以半径平均值为估计值的方法,降低了66.7%,同时可实现钟罩在检测过程中任意点的启停。     

嗅探模式Web过滤器设计与实现

对比Web过滤器的嵌入和嗅探工作模式,分析嗅探工作模式的部署方式和工作原理,使用原始套接字编程技术捕获网络数据包,按照IP、TCP和HTTP协议进行协议分析。当客户端向服务器端发送的HT—TP请求信息时,使用Boyer-Moore算法对预定义的模式进行模式匹配,并通过直接扣间接两种方式实现先于服务器端在客户端显示Web信息。实际运行测试效果说明,嗅探模式Web过滤器在模式匹配速度和反馈过滤信息上都达到嵌入式Web过滤器的运行效果。     

一种快速的基于BM模式匹配的改进算法

模式匹配算法是入侵检测系统(IDS) 中非常重要的一种算法. 在研究和分析几种常用模式匹配算法的基础 上, 提出一种快速的基于BM(Boyer-Moore) 模式匹配的改进算法—–IBM 算法. 该算法充分利用模式串的末字符和 末字符所对应的文本串的后两字符的唯一性, 同时参考文本串本身的信息来提高模式串的移动量, 使得每次失配后, 在保证不丢失匹配成功可能性的前提下尽可能多地向后跳跃. 实验结果表明, 该算法相比其他模式匹配算法, 在检测 性能和匹配效率上均具有很大优势, 并且能够有效地提高IDS 的检测效率和性能.

     

入侵检测中模式匹配算法的性能分析

模式匹配算法在入侵检测中有着广泛的应用,它直接影响到入侵检测系统的实时性能。论文主要研究了Boyer-Moore算法,Modified Wu—Manber算法,Exclusion—Based算法和Aho—Corasick算法。通过实验对上述四种算法在混合攻击和特定攻击的条件下进行了性能测试,根据实验结果,得出了不同算法的应用范围,为今后入侵检测系统开发者选择模式匹配算法提供了有价值的参考。