A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol

We present a formal model of asynchronous communication between two digital hardware devices. The model takes the form of a function in the Boyer-Moore logic. The function transforms the signal stream generated by one processor into that consumed by an independently clocked processor, given the phases and rates of the two clocks and the communications delay. The model can be used quantitatively to derive concrete performance bounds on communications at ISO protocol level 1 (physical level). We use the model to show that an 18-bit/cell biphase mark protocol reliably sends messages of arbitrary length between two processors provided the ratio of the clock rates is within 5% of unity.     

Snort研究及BM算法改进

Snort是一个轻型的入侵检测系统,在检测过程中,字符串匹配算法的效率决定了Snort系统的性能.分析了Snort的系统结构和工作流程,对Snort的BM字符匹配算法进行深入研究,提出了BM字符匹配算法的改进方法.实验数据表明,改进的BM字符匹配算法可提高Snort的效率.     

An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness pro...     

汉语定义语句的抽取方法

该文介绍了在汉语文本中抽取定义语句的方法。方法的主要特点是：给定被定义的词汇（字符串）,应用Bo-yer-Moore算法查找该串在文本中的位置,继而在该句子中查找符合定义特征的谓词。在这个工作基础上,根据谓词字符串的特征排除谓词歧义,并按照句法分析的结果对定义语句修饰谓词的不同语法单元进行识别,从而实现了基于字符串和语法特征的识别的定义语句抽取。     

定理证明辅助工具PVS剖析

ＰＶ查斯坦福机构开发的强大的规约。验证系统,它的适用领域广泛,在概要介绍ＰＶＳ的构成。功能后,着重分析了ＰＶＳ的规约语言,验证系统的特点,以及使得ＰＶＳ灵活,强大的设计决策和内在机制。     

基于多模板匹配和可信度分析的中文文档图像关键词过滤方法*

针对互联网中文文档图像非法信息过滤提出了一种多模板匹配结合可信度分析的方法。该方法克服了传统OCR速度慢的缺点,同时改善了基于图像特征匹配方法对字体和噪音敏感的特性。通过改变关键词搜索方式有效地减小了计算量,提高了识别速度。实验结果表明了该方法的有效性。     

BWT-Boyer-Moore压缩域搜索算法的研究

针对BoyerMoore匹配算法对压缩文本文件搜索的不足,分析了当前对于压缩文件搜索的主要方法,提出了一种基于BW转换的高效的搜索算法并予以验证。     

关于提升装载机电子秤检定结果测量准确度的探讨

装载机电子秤广泛应用于货场、建筑工地,如何使检定结果准确可靠,本文对自动衡器检定装置标准器量值的管理方法进行了一些探讨。     

Correlation of the leakage flow rate with pressure changes in a clearance-sealed piston prover

Leakage flow rate is one of the most important contributions to the measurement uncertainty when measuring small gas flow rates with a clearance-sealed piston prover. Our previous study has shown that the systematic effects related to the change of the gas viscosity can be successfully corrected, whereas the effects related to the reproducibility of the leakage flow rate are poorly understood. This paper focuses on the interpretation and correction of the reproducibility related effects by analysing experimentally identified variations of the leakage flow rate and the gas pressure in the inclined piston prover. Small changes of the leakage flow in the inclined piston prover indicate that the position of the piston relative to the cylinder remains approximately the same. The obtained relationship between the leakage flow rate and the gas pressure below the piston led to the pressure-based correction of the leakage flow rate.     

Integrating a SAT Solver with an LCF-style Theorem Prover

This paper describes the integration of a leading SAT solver with Isabelle/HOL, a popular interactive theorem prover. The SAT solver generates resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem prover. The presented approach significantly improves Isabelle's performance on propositional problems, and furthermore exhibits counterexamples for unprovable conjectures.