Translation Templates to Support Strategy Development in PVS

In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover's representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (Timed Input/Output Automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.     

A Java Card CAP converter in PVS

The Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card specifies its own class file format (the Java Card Converted APplet (CAP) format) that is optimised with respect to the limited space resources of smart cards. This paper deals with the certified development of algorithms necessary for the conversion of ordinary Java class files into the CAP format. More precisely, these algorithms are concerned with constructing and compressing method tables and constant pools. The main contribution of this paper is to specify and prove the correctness of these algorithms using the theorem prover PVS.     

高可靠性温室环境测控系统架构形式化建模与特性证明

温室环境测控系统由多个可并发执行的子系统共同协作来构造适宜的温室环境以确保作物有效生长.为提高温室环境测控系统设计的效率和可靠性,本文提出一个能为设计者提供指导性框架的融入容错技术的高可靠性温室环境测控系统架构.并且运用PVS形式化语言对系统架构进行了精确而无二义性的形式化建模,以及PVS证明工具对系统架构的容错特性进行了机械化证明,以确保系统架构能满足高可靠性需求.     

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

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

Modular Verification of SRT Division

We describe a formal specification and mechanized verification in PVS of the general theory of SRT division along with a specific hardware realization of the algorithm. The specification demonstrates how attributes of the PVS language (in particular, predicate subtypes) allow the general theory to be developed in a readable manner that is similar to textbook presentations, while the PVS tabletable construct allows direct specification of the implementation's quotient lookup table. Verification of the derivations in the SRT theory and for the data path and lookup table of the implementation are highly automated and performed for arbitrary, but finite precision; in addition, the theory is verified for general radix, while the implementation is specialized to radix 4. The effectiveness of the automation stems from the tight integration in PVS of rewriting with decision procedures for equality, linear arithmetic over integers and rationals, and propositional logic. This example demonstrates that the resources of an expressive specification language and of a general-purpose theorem prover are not inimical to highly automated verification in this domain, and can contribute to clarity, generality, and reuse.     

Convergence and comparison results for double splittings of Hermitian positive definite matrices

Abstract For single splittings of Hermitian positive definite matrices, there are well-known convergence and comparison theorems. This paper gives new convergence and comparison results for double splittings of Hermitian positive definite matrices. Keywords: Hermitian positive definite matrix; convergence theorem; comparison theorem; double splitting Mathematics Subject Classification (2000): 65F10     

Verification of a sliding window protocol in μCRL and PVS

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. Received November 2004 Revised June 2005 Accepted July 2005 by J. V. Tucker     

A general lock-free algorithm using compare-and-swap

The compare-and-swap register (CAS) is a synchronization primitive for lock-free algorithms. Most uses of it, however, suffer from the so-called ABA problem. The simplest and most efficient solution to the ABA problem is to include a tag with the memory location such that the tag is incremented with each update of the target location. This solution, however, is theoretically unsound and has limited applicability. This paper presents a general lock-free pattern that is based on the synchronization primitive CAS without causing ABA problem or problems with wrap around. It can be used to provide lock-free functionality for any data type. Our algorithm is a CAS variation of Herlihy’s LL/SC methodology for lock-free transformation. The basis of our techniques is to poll different locations on reading and writing objects in such a way that the consistency of an object can be checked by its location instead of its tag. It consists of simple code that can be easily implemented using C-like languages. A true problem of lock-free algorithms is that they are hard to design correctly, which even holds for apparently straightforward algorithms. We therefore develop a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on Lamport’s refinement mappings, and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and formulate without considering the internal structure of the final implementation.     

Subtypes for specifications: predicate subtyping in PVS

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called “predicate subtyping” that uses this capability and illustrate its utility as mechanized in PVS     

Weakest pre-condition reasoning for Java programs with JML annotations

This paper distinguishes several different approaches to organising a weakest pre-condition (WP) calculus in a theorem prover. The implementation of two of these approaches for Java within the LOOP project is described. This involves the WP-infrastructures in the higher order logic of the theorem prover PVS, together with associated rules and strategies for automatically proving JML specifications for Java implementations. The soundness of all WP-rules has been proven on the basis of the underlying Java semantics. These WP-calculi are integrated with the existing Hoare logic, and together form a verification toolkit in PVS: typically one uses Hoare logic rules to break a large verification task up into smaller parts that can be handled automatically by one of the WP-strategies.     

High-automation proofs for properties of requirements models

We describe an approach and experimental results in the application of mechanized theorem proving to software requirements analysis. Serving as the test article was the embedded controller for SAFER, a backpack propulsion system used as a rescue device by NASA astronauts. SAFER requirements were previously formalized using the prototype verification system (PVS) during a NASA pilot project in formal methods, details of which appear in a NASA guidebook. This paper focuses on the formulation and proof of properties for the SAFER requirements model. To test the prospects for deductive requirements analysis, we used the PVS theorem prover to explore the upper limits of proof automation. A set of property classes was identified, with matching proof schemes later devised. After developing several PVS proof strategies (essentially prover macros), we obtained fully automatic proofs of 42 model properties. These results demonstrate how customized prover strategies can be used to automate moderate-complexity theorem proving for state machine models.     

RETE网络中的优化编译模式及其PVS形式验证

In the compilation of rule program to the intermediate code-RETE network,optimizing compilation is an important compiler schema,and is a necessary step in the compiler verification.In this paper,we discuss optimization schemas in rule program compilation,and prove the semantic equivalence theorems of these schemas.Firstly,the structure of RETE network and its PVS specification are represented.Secondly,three kinds of optimization schemas are listed.Then algorithms evaluating semantics of target RETE network are given.Finally,we prove the semantic equivalence theorems with theorem prover PVS (Prototype Verification System).     

Approximation by rational spline functions

Abstract We discuss the linear precision property of NURBS functions. The degree of approximation of continuous functions is studied. Keywords: NURBS functions; linear precision; approximation degree; modulus of smoothness Mathematics Subject Classification (1991): 41A15, 41A25, 41A28, 41A36, 41A63, 65D07, 65D17     

A queue based mutual exclusion algorithm

A new elegant and simple algorithm for mutual exclusion of N processes is proposed. It only requires shared variables in a memory model where shared variables need not be accessed atomically. We prove mutual exclusion by reformulating the algorithm as a transition system (automaton), and applying simulation of automata. The proof has been verified with the higher-order interactive theorem prover PVS. Under an additional atomicity assumption, the algorithm is starvation free, and we conjecture that no competing process is passed by any other process more than once. This conjecture was verified by model checking for systems with at most five processes.     

Formal Verification of Square Root Algorithms

We discuss the formal verification of some low-level mathematical software for the Intel® Itanium® architecture. A number of important algorithms have been proven correct using the HOL Light theorem prover. After briefly surveying some of our formal verification work, we discuss in more detail the verification of a square root algorithm, which helps to illustrate why some features of HOL Light, in particular programmability, make it especially suitable for these applications.     

融合图像感知哈希技术的运动目标跟踪

目的 为解决运动目标跟踪时因遮挡、尺度变换等产生的目标丢失以及传统匹配跟踪算法计算复杂度高等问题,提出一种融合图像感知哈希技术的运动目标跟踪算法.方法 本文算法利用感知哈希技术提取目标摘要进行模板图像识别匹配,采用匹配跟踪策略和搜索跟踪策略相配合来准确跟踪目标,并构建模板评价函数和模板更新准则实现目标模板的自适应更新,保证其在目标发生遮挡和尺度变换情况下的适应性.结果 该算法与基于NCC(normalized cross correlation)的模板匹配跟踪算法、Mean-shift跟踪算法以及压缩跟踪算法相比,在目标尺度变换和物体遮挡时,跟踪的连续性和稳定性更好,且具有较低的计算复杂度,能分别降低跟踪系统约6.2%、 6.3%、 9.3%的计算时间.结论 本文算法能有效实现视频场景中目标发生遮挡及尺度变换情况下的跟踪,跟踪的连续性和稳定性良好,且算法具有较低的计算复杂度,有利于实时性跟踪系统的构建.     

On the convergence of subproper (multi)-splitting methods for solving rectangular linear systems

Abstract We give a convergence criterion for stationary iterative schemes based on subproper splittings for solving rectangular systems and show that, for special splittings, convergence and quotient convergence are equivalent. We also analyze the convergence of multisplitting algorithms for the solution of rectangular systems when the coefficient matrices have special properties and the linear systems are consistent. Keywords: Rectangular linear system, iterative method, proper splitting, subproper splitting, regularity, Hermitian positive semi-definite matrix, multi-splitting, quotient convergence AMS Subject Classification: 65F10, 65F15     

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.     

阵列众核结构上的一种多层分区Hash连接算法

连接是数据查询处理中最耗时、使用最频繁的操作之一,对提高连接操作的速率具有重要意义。阵列众核处理器是一类重要的众核处理器,具有强大的并行能力,可用来加速并行计算。基于阵列众核处理器的结构,设计和优化了一种高效的多层分区Hash连接算法。该算法通过多层划分的策略大大降低了主存访问次数,通过分区重排方法有效消除了数据倾斜的影响,获得了很高的性能。在异构融合阵列众核处理器DFMC(Deeply-Fused Many Core)原型系统上的实验结果表明,DFMC上多层分区Hash连接算法的性能是CPU-GPU耦合结构上最快的连接算法的8.0倍,表明利用阵列众核处理器加速数据查询应用具有优势。     

PVS Embedding of cCSP Semantic Models and Their Relationship

This paper demonstrates an embedding of the semantic models of the cCSP process algebra in the general purpose theorem prover PVS. cCSP is a language designed to model long-running business transactions with constructs for orchestration of compensations. The cCSP process algebra terms are defined in PVS by using mutually recursive datatype. The trace and the operational semantics of the algebra are embedded in PVS. We show how these semantic embeddings are used to define and prove a relationship between the semantic models by using the powerful induction mechanism of PVS.