LVT: a layered verification technique for distributed computing systems

This paper presents a layered verification technique, called LVT, for the verification of distributed computing systems with multiple component layers. Each lower layer in such a system provides services in support of functionality of the higher layer. By taking a very general view of programming languages as interfaces of systems, LVT treats each layer in a distributed computing system as a distributed programming language. Each relatively higher‐level language in the computing system is implemented in terms of a lower‐level language. The verification of each layer in a distributed computing system can then be viewed as the verification of implementation correctness for a distributed language. This paper also presents the application of LVT to the verification of a distributed computing system, which has three layers: a small high‐level distributed programming language; a multiple processor architecture consisting of an instruction set and system calls for inter‐process message passing; and a network interface. Programs in the high‐level language are implemented by a compiler mapping from the language layer to the multiprocessor layer. System calls are implemented by network services. LVT and its application demonstrate that the correct execution of a distributed program, most notably its inter‐process communication, is verifiable through layers. The verified layers guarantee the correctness of (1) the compiled code that makes reference to operating system calls, (2) the operating system calls in terms of network calls, and (3) the network calls in terms of network transmission steps. The specification and verification involved are carried out by using the Cambridge Higher Order Logic (HOL) theorem proving system. Copyright © 1999 John Wiley & Sons, Ltd.     

Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses

This paper describes our experience using the interactive theorem prover Athena for proving the correctness of abstract interpretation-based dataflow analyses. For each analysis, our methodology requires the analysis designer to formally specify the property lattice, the transfer functions, and the desired modeling relation between the concrete program states and the results computed by the analysis. The goal of the correctness proof is to prove that the desired modeling relation holds. The proof allows the analysis clients to rely on the modeling relation for their own correctness. To reduce the complexity of the proofs, we separate the proof of each dataflow analysis into two parts: a generic part, proven once, independent of any specific analysis; and several analysis-specific conditions proven in Athena.     

稠密自组网的网关选举策略

自组网是没有固定设施的临时无线系统．已经有多种路由算法被提出．因为自组网的网络拓扑动态改变且带宽有限,路由应当是可扩展且高效的．基于簇的算法是最有效和可以扩展的,然而,它不能有效地处理高密度网络环境．为了减少冗余广播以缓解该问题,该文给出了在高密度节点的网络环境下,存在隐藏网关的可能性定理,提出网关选举算法并证明了其正确性．仿真结果表明,在保证广播成功率的情况下,该方法可以有效地节省重播包比率和广播等待时间。     

Theorem prover approach to semistructured data design

The wide adoption of semistructured data has created a growing need for effective ways to ensure the correctness of its organization. One effective way to achieve this goal is through formal specification and automated verification. This paper presents a theorem proving approach towards verifying that a particular design or organization of semistructured data is correct. We formally specify the semantics of the Object Relationship Attribute data model for Semistructured Data (ORA-SS) modeling notation and its correctness criteria for semistructured data normalization using the Prototype Verification System (PVS). The result is that effective verification on semistructured data models and their normalization can be carried out using the PVS theorem prover.     

A formal specification and verification framework for TimeWarp-based parallel simulation

The paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified, describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and type-check condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations     

Theory Extension in ACL2(r)

ACL2(r) is a modified version of the theorem prover ACL2 that adds support for the irrational numbers using nonstandard analysis. It has been used to prove basic theorems of analysis, as well as the correctness of the implementation of transcendental functions in hardware. This paper presents the logical foundations of ACL2(r). These foundations are also used to justify significant enhancements to ACL2(r).      

Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance analysis quite complex. Thus, traditional techniques, such as simulation, or the state-based formal methods usually fail to produce reasonable results. In this paper, we propose to use higher-order-logic (HOL) theorem proving for the performance analysis of real-time systems. The idea is to formalize the real-time system as a logical conjunction of HOL predicates, whereas each one of these predicates define an autonomous component or process of the given real-time system. The random or unpredictable behavior found in these components is modeled as random variables. This formal specification can then be used in a HOL theorem prover to reason about both functional and performance related properties of the given real-time system. In order to illustrate the practical effectiveness of our approach, we present the analysis of the Stop-and-Wait protocol, which is a classical example of real-time systems. The functional correctness of the protocol is verified by proving that the protocol ensures reliable data transfers. Whereas, the average message delay relation is verified in HOL for the sake of performance analysis. The paper includes the protocol’s formalization details along with the HOL proof sketches for the major theorems.     

一种基于本体KNN的分布式缓存数据交换策略

以国家开放大学教务管理系统为例,以减少数据资源获取的时间开销以及提高数据质量作为目标,提出了一种基于本体KNN的分布式缓存数据交换策略,用于解决分布式系统在不同节点之间进行数据交换时产生的性能优化问题。仿真实验结果表明,该策略具有较为出色的优化访问性能,可以实现数据交换过程的进一步优化,进而提升系统的整体性能,具有一定的实用价值。     

A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.     

Verifying the SRT Division Algorithm Using Theorem Proving Techniques

We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper with much less guidance than existing general purpose theorem provers require for algebraic reasoning.     

Proving linearizability with temporal logic

Linearizability is a global correctness criterion for concurrent systems. One technique to prove linearizability is applying a composition theorem which reduces the proof of a property of the overall system to sufficient rely-guarantee conditions for single processes. In this paper, we describe how the temporal logic framework implemented in the KIV interactive theorem prover can be used to model concurrent systems and to prove such a composition theorem. Finally, we show how this generic theorem can be instantiated to prove linearizability of two classic lock-free implementations: a Treiber-like stack and a slightly improved version of Michael and Scott’s queue.     

一种基于延迟抢先的消息最大响应时间算法

分布式实时系统是实时系统的一个重要研究方向，有着广泛的应用背景，消息最大响应时间的定量分析是该研究方向中的一个关键问题，在深入分析国内外相关研究的基础上，针对采用TDMA协议的分布实时系统提出了一种基于延迟抢先的消息最大响应时间算法，解决了现有消息最大响应时间算法存在的正确性问题，对消息的最大响应时间做出完整、精确的分析。     

Serializability theory for replicated databases

In a one-copy distributed database, each data item is stored at exactly one site of a distributed system. In a replicated database, some data items are stored at multiple sites. The main motivation for replicated data is improved reliability: by storing important data at multiple sites, the system can tolerate failures more gracefully. This paper presents a theory for proving the correctness of algorithms that manage replicated data. The theory is an extension of serializability theory. We use the theory to give simple correctness proofs for two replicated data algorithms: Gifford's “quorum consensus” algorithm, and Eager and Sevcik's “missing writes” algorithm.     

基于模型诊断的分步求解

对诊断问题的分解进行研究,给出了候选诊断的分解与组合定理.在此基础上,提出了利用分步求解方法实现诊断分解的算法,并对算法的正确性、完备性和复杂性进行了证明.实验结果表明,分步求解方法明显提高了包含多个输出的系统的诊断效率.与利用变量假定例化值分解诊断问题的方法相比,该算法能提高了效率并且扩大了适用范围.     

时变时滞非线性系统的间歇控制

时变时滞广泛存在于各种非线性系统中,研究了时变时滞非线性系统的间歇控制及其在保密通信中的应用问题,提出了一种间歇控制策略,理论上分析了其正确性,并且给出一个定理来确定控制器的相关参数。根据提出的定理,设计出间歇控制器使得两个含有时变时滞的Chua电路指数达到同步。将该方法应用到混沌保密通信中,在两个系统达到同步的基础上,发送端的信号能够在接收端很好地恢复出来,表明了该方法的可行性。     

Verifikation von Webservicekompositionen:

Web service compositions coordinate Web services of different enterprises. They are expected to constitute the foundation of service-oriented architectures, to improve business processes as well as to foster intra- and inter-organizational integration. Especially in inter-organizational contexts, quality of service referring to non-functional requirements and conformance to functional requirements are becoming vital properties. With Web service compositions being asynchronous and distributed systems, the latter property – which is also called correctness – can be shown best by verification. This paper examines from a system-theoretic perspective how correctness can be operationalized for Web service compositions. It also proposes a requirements framework for service-oriented modeling techniques so that correctness can be shown by verification and Web service compositions can be modeled intuitively. In order to show the framework’s principle applicability, an example approach is analyzed with respect to the corresponding requirements.     

Inductive assertions and operational semantics

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.     

Correctness of a distributed transaction system

A distributed transaction system manages information that is dispersed over a number of storage devices. This paper deals with an experimental transaction system designed to satisfy real-time constraints through distributed control of the executions of transactions. Of interest is the correctness of the algorithm for distributed control. Demonstrating the correctness involves showing that the algorithm guarantees the consistency of distributed data, and equally importantly, that every transaction will eventually terminate. Proof of consistency is based on the notion of serializability of transactions while proof of termination is based on the conflict resolution and failure recovery strategies employed by the transaction system.     

Eliminating redundant search space on backtracking for forward chaining theorem proving

This paper introduces some improvements on the intelligent backtracking strategy for forward chaining theorem proving. How to decide a minimal useful consequent atom set for a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessary non-Horn clause used for forward chaining will be split only once. The increase of the search space by invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore.In this paper, the principle of the proposed method and its correctness are introduced. Moreover,some examples are provided to show that the proposed approach is powerful for forward chaining theorem proving.