面向安全关键内存管理系统分层验证方法

安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.     

基于离散事件仿真的复杂冗余系统可用度分析

介绍了如何利用离散事件仿真技术对复杂冗余系统可用度进行分析。首先,对复杂冗余系统进行了介绍,提出了利用BS树来描述复杂冗余系统的结构。其次,对复杂冗余系统的行为、状态转移规律进行了分析。然后,利用离散事件仿真技术,给出了复杂冗余系统可用度仿真算法,并介绍了BS树的描述及常用方法、确定系统状态、部件转移状态等细节问题。最后,给出了计算实例。结果证明,该仿真算法不仅可以对状态独立系统进行可用度计算,而且可以对具有冗余关系和嵌套关系的状态相关系统进行可用度计算,具有很强的实用性与通用性。     

基于协同侦测技术的移动主体模型验证策略研究

移动主体模型可以实现协同侦测网络攻击和区域预警的功能;它利用元组空间(TUPLE—SPACE)构建移动主体服务集群(RMAS—CMAS)网络结构及侦测ARP攻击的主体．为了证明该模型逻辑的有效性,验证策略设计了可以分析ARP攻击数据包从初始组态到终结组态的动态空间树;利用空间树嵌套演算推理协同侦测系统的组态迁移过程,分析模块的动态移动重组以及消息的并行传递机制．对模型验证策略的研究可以消除在模型设计阶段出现的冗余组态,提高移动系统的设计水平．     

易于硬件实现的集合树块图像压缩编码

提出一种易于硬件实现的集合树块图像压缩算法,将小波系数按照零树的方法排列为树集合,并将树集合排列为集合树块,利用分辨率之间的相似性和相邻系数之间的相关性进行编码,提高数据压缩效率;树块之间独立进行编码,以提高系统抗误码能力.对算法进行了系统仿真,结果表明本算法压缩效率与JPEG2000相当,优于SPIHT压缩算法,但编码算法更简单,有利于系统的硬件实现.     

关于非线性Morgan问题的一个充分条件

研究一般右可逆非方非线性系统的Morgan问题.在系统结构分解的框架下,先利用一个类Singh算法来刻画系统本性阶与无穷零点的差集,然后给出一个求取积分串的新算法.如果上述差集与积分串的长度满足一个简单的不等式关系,则可以证明,此时Morgan问题一定有解,并给出一组解耦反馈的构造方法.     

超长整数运算的PVS规范与验证

超长整数的运算是现代密码系统的应用基础,运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性,利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后,给出了超长整数及其算法的形式规范,通过把算法需要满足的性质描述为定理,将算法的一致性验证问题转化为逻辑定理证明的问题,在PVS定理证明器上完成了相关定理的证明,从而表明这些算法是满足设计需求的。     

在线算法验证系统的设计与实现

针对远程教学练习环节中存在的问题,提出了一种利用ASP.NET技术构建在线算法验证系统的实现方法.系统用命令行编译和批处理技术实现对算法程序的自动编译;利用运行结果的捕获技术和数据库技术实现算法程序的自动测试;利用数据库技术、哈希表技术,算法相似度计算等技术实现算法练习的管理.实践运行结果表明,该系统有效解决了练习提交的及时性和练习批改及管理的自动化问题,大大地改善了教学手段、提高了教学效果.     

流调度算法验证平台的设计与实现

在VOD（视频点播）系统中,优秀的流调算法可以显著的提高系统服务能力和服务质量,典型流调度算法都针对大型视频点播系统,因此我们不可能为验证算法而建立实际的系统。我们设计和实现了一个媒体流调度算法的验证平台,在这个平台中,我们建立了用户行为的数学模型,实现了用户行为仿真器;用户行为仿真器生成的用户行为样本,可以运行在装载了不同算法的仿真系统中,在这个平台中,我们还提出了变强度用户流的概念,使平台对实际用户点播服务的仿真更加客观。     

基于悖论证明与局部搜索的不可满足子式求解算法

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.     

基于多故障模糊组的序贯多故障诊断方法

由于系统复杂性的显著提高,多故障发生的概率也逐渐增大;针对多故障诊断的困难性,提出一种序贯多故障诊断算法;算法以构建的单故障诊断树为基础,利用集合划分思想和多故障模糊组,并根据信息熵理论实现测试选择,逐渐扩展单故障诊断树,最终得到多故障诊断树;最后的系统实例详细阐述了序贯多故障诊断算法的应用过程,生成了多故障诊断树,可以有效地实现对系统多故障的检测.     

Automated Flaw Detection in Algebraic Specifications

In interactive theorem proving practice a significant amount of time is spent on unsuccessful proof attempts of wrong conjectures. An automatic method that reveals them by generating finite counter examples would offer an extremely valuable support for a proof engineer by saving his time and effort. In practice, such counter examples tend to be small, so usually there is no need to search for big instances. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose constraints which guarantee a correct axiomatization on finite structures and present an approach which uses the Alloy Analyzer to generate finite instances of theories in the theorem prover KIV. It is evaluated on the library of basic data types as well as on some challenging case studies in KIV. The technique is implemented using the Kodkod constraint solver which is a successor of Alloy.     

Light-Weight SMT-based Model Checking

Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a “light-weight” algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach.     

A Tutorial on Stålmarck's Proof Procedure for Propositional Logic

We explain Stålmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification.     

Pascal in LCF: Semantics and examples of proof

An axiomatization in LCF of a substantial subset of PASCAL (including $\text{I}\text{O}$) is presented. The syntax of such a subset is introduced and the LCF axioms defining the corresponding semantics are discussed. Sample theorems about the semantic definitions are shown.As an example of use of this axiomatization for proving properties of programs (with a machine checked proof), we present the correctness of a program for the “McCarthy Airline” reservation system. An interesting aspect of such a program is that it deals with a potentially infinite sequence of inputs. An LCF theorem asserting its (partial) correctness is then presented, with its proof, carried out using the Stanford LCF proof checker.     

一种构造代码安全性证明的方法

提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.     

SETHEO: A high-performance theorem prover

A sound and complete theorem prover for first-order logic is presented, which is based on the connection method. The inference machine is implemented using PROLOG technology, an approach taken also with other systems, most prominently with Stickel's PTTP. But SETHEO differs from those in essential characteristics, among which are the following ones. It incorporates a powerful preprocessing module for a reduction of the input formula. The main proof procedure is realized as a variant of Warren's abstract machine. For search pruning we perform subsumption and regular proofs. Factorization, lemma generation, and the application of proof schemata are offered as options. The entire system is implemented in C and is running on several machines. The most remarkable feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips. The paper comprises the theoretical background, the system architecture as well as details of the implementation.     

Completeness of fair ASM refinement

ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi-Lamport setting.     

Stability of two-dimensional feedback systems

Stability conditions for discrete-time linear dynamical systems in two independent variables are considered. A new proof of a known condition is given, enabling a more transparent interpretation. It is shown that closed-loop stability of a feedback system can be determined from open-loop information by using an infinite family of Nyquist plots. On the basis of these results, the extension of classical design methods, using root loci and frequency response, is advocated.     

Verification of a multiprocessor cache protocol using simulation relations and higher-order logic

We present a formal verification method for concurrent systems. The technique is to show a correspondence between state machines representing an implementation and specification behavior. The correspondence is called asimulation relation, and is particularly well suited for theorem provers. Since the method does not rely on enumerating all the states, it can be applied to systems with an infinite or unknown number of states. The method is illustrated by proving the correctness of a particularly subtle example that is likely to be of increasing importance: a directory based multiprocessor cache protocol. The proof is carried out using the HOL (higher-order logic) theorem prover.     

Automatic Derivation of the Irrationality of e

As part of a project on automatic generation of proofs involving both logic and computation, we have automatically generated a proof of the irrationality of e. The proof involves inequalities, bounds on infinite series, type distinctions (between real numbers and natural numbers), a subproof by mathematical induction, and significant mathematical steps, including correct simplification of expressions involving factorials and summing an infinite geometrical series. Metavariables are instantiated by inference rules embodying mathematical knowledge, rather than only by unification. The proof is generated completely automatically, without any interactive component.