PVS Strategies for Proving Abstraction Properties of Automata

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the “natural” proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.     

Proving Invariants of I/O Automata with TAME

This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.     

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.     

Validation of HOL Proofs by Proof Checking

Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps.     

A general technique for proving lock-freedom

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.     

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.     

Verification and synthesis of addition programs under the rules of correctness of statements

Deductive verification and synthesis of binary addition programs are carried out on the base of the rules of proving the correctness for statements of the predicate programming language P. The paper presents key fragments of verification and synthesis of the programs for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the programs were translated into the specification language of the PVS verification system. The proof is found to be a tedious procedure as compared with the ordinary programming. However, for program synthesis, the development of theories and proofs on PVS are easier and faster than for program verification.     

Finding Proofs in Tarskian Geometry

We report on a project to use a theorem prover to find proofs of the theorems in Tarskian geometry. These theorems start with fundamental properties of betweenness, proceed through the derivations of several famous theorems due to Gupta and end with the derivation from Tarski’s axioms of Hilbert’s 1899 axioms for geometry. They include the four challenge problems left unsolved by Quaife, who two decades ago found some OTTER proofs in Tarskian geometry (solving challenges issued in Wos’s 1998 book). There are 212 theorems in this collection. We were able to find OTTER proofs of all these theorems. We developed a methodology for the automated preparation and checking of the input files for those theorems, to ensure that no human error has corrupted the formal development of an entire theory as embodied in two hundred input files and proofs. We distinguish between proofs that were found completely mechanically (without reference to the steps of a book proof) and proofs that were constructed by some technique that involved a human knowing the steps of a book proof. Proofs of length 40–100, roughly speaking, are difficult exercises for a human, and proofs of 100–250 steps belong in a Ph.D. thesis or publication. 29 of the proofs in our collection are longer than 40 steps, and ten are longer than 90 steps. We were able to derive completely mechanically all but 26 of the 183 theorems that have “short” proofs (40 or fewer deduction steps). We found proofs of the rest, as well as the 29 “hard” theorems, using a method that requires consulting the book proof at the outset. Our “subformula strategy” enabled us to prove four of the 29 hard theorems completely mechanically. These are Ph.D. level proofs, of length up to 108.     

Proof assistance for real-time systems using an interactive theorem prover

This paper discusses the adaptation of the PVS theorem prover for performing analysis of real-time systems written in the ASTRAL formal specification language. Several issues arose during the encoding of ASTRAL that are relevant to the encoding of many real-time specification languages such as encoding formulas as types, handling partial functions, dealing with noninterleaved concurrency, and defining irregular operators. These issues and possible solutions are presented as well as how they were handled in the ASTRAL encoding. A translator was written that translates any ASTRAL specification into its corresponding PVS encoding. After performing the proofs of several systems using their translations, PVS strategies were developed to automate the proofs of certain types of properties. In particular, strategies are presented for fully automating the proofs of certain classes of untimed properties. In addition, strategies were developed for partially automating the derivation of timed executions using transition steps. The encoding was used as the basis for a fully automated transition sequence generator tool, which has a wide variety of applications.     

A man-machine theorem-proving system

This paper describes a man-machine theorem-proving system at the University of Texas at Austin which has been used to prove a few theorems in general topology. The theorem (or subgoal) being proved is presented on the scope in its natural form so that the user can easily comprehend it and, by a series of interactive commands, can help with the proof when he desires. A feature called DETAIL is employed which allows the human to interact only when needed and only to the extent necessary for the proof.The program is built around a modified form of IMPLY, a natural-deduction-like theorem proving technique which has been described earlier.A few examples of proofs are given.     

The Use of Proof Planning for Co-operative Theorem Proving

We describebarnacle: a co-operative interface to theclaminductive theorem proving system. For the foreseeable future, there will be theorems which cannot be proved completely automatically, so the ability to allow human intervention is desirable; for this intervention to be productive the problem of orienting the user in the proof attempt must be overcome. There are many semi-automatic theorem provers: we call our style of theorem provingco-operative, in that the skills of both human and automaton are used each to their best advantage, and used together may find a proof where other methods fail. The co-operative nature of thebarnacleinterface is made possible by the proof planning technique underpinningclam. Our claim is that proof planning makes new kinds of user interaction possible.Proof planning is a technique for guiding the search for a proof in automatic theorem proving. Common patterns of reasoning in proofs are identified and represented computationally as proof plans, which can then be used to guide the search for proofs of new conjectures. We have harnessed the explanatory power of proof planning to enable the user to understand where the automatic prover got to and why it is stuck. A user can analyse the failed proof in terms ofclam's specification language, and hence override the prover to force or prevent the application of a tactic, or discover a proof patch. This patch might be to apply further rules or tactics to bridge the gap between the effects of previous tactics and the preconditions needed by a currently inapplicable tactic.     

Formal Foundations of Operational Semantics

In this paper we report on the results of a sophisticated and substantial use of PVS to establish a recent result in operational semantics. The result we establish is a context lemma for operational equivalence for very wide class of programming languages, known as the CIU theorem. The proof uses the annotated holes technique to represent contexts and compute with them. Thus this paper demonstrates that that it is possible to use PVS as a tool in the development of modern operational techniques, and a productive tool at that. The process of formalizing the CIU theorem revealed several gaps in published proof. The proof of the CIU theorem in PVS took approximately six months to develop. The actual machine checked proof involves the proving of around one thousand facts, and takes PVS slightly less than three hours of CPU time running on a Linux machine configured with 2 GBytes of main memory and four 550 MHz Xeon PIII processors.     

Proof by analogy in mural

An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct? One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming. This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.     

区间时序逻辑的标记相继式演算

区间逻辑在许多领域如人工智能,形式化方法中都有成功应用。其中,区间时序逻辑及其各种扩充近年来越来越多地受到人们的重视,由于区间时序逻辑具有较强的表达能力,这也使得该逻辑的定理证明变得相当困难,该文提出了区间时序逻辑的一个标记相继式演算,并给出其可靠性和相对完备性结论。该演算应用于机器辅助定理证明工具中,可以有效地提高证明的自动化程度,在高阶逻辑证明了工具ＰＶＳ中,作者尝试性地实现了这一演算,获得了     

基于程序生成的自动化服务组合技术

自动化服务组合技术是程序生成方法在Semantic Web Services领域的一种应用。该文提取了服务的“输入”、“输出”、“前置条件”、“执行效果”、“执行功能”,定义了服务的语义5元组。通过一个转换模版,把服务描述表述成一阶谓词逻辑公式,根据“证明与程序等价”的理论,利用自动化定理证明系统,完成从已有服务到目标服务的逻辑证明,从所记录的证明路径中提取目标服务的实现体,介绍了实现这一技术的原型系统。     

Refinement verification of the lazy caching algorithm

The lazy caching algorithm of Afek et al. (ACM Trans. Program. Lang. Syst. 15, 182–206, 1993) is a protocol that allows the use of local caches with delayed updates. It results in a memory model that is not atomic (linearizable) but only sequentially consistent as defined by Lamport. In Distributed Computing 12 (1999), specifying and proving sequential consistency for the lazy caching algorithm was made into a benchmark for verification models. The present note contains such a specification and proof. It provides a simulation from the implementation to the abstract specification. The concrete verification only relies on the state space and the next-state relation. All behavioural aspects are treated in theories independent of the specific algorithm. The proofs of the underlying theories and of the concrete algorithm have been verified with the proof assistant PVS.     

Comparing Approaches to the Exploration of the Domain of Residue Classes

We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proof techniques, which are implemented as strategies in a multi-strategy proof planner. The search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. To test the effectiveness of our approach we carried out a large number of experiments and also compared it with some alternative approaches. In particular, we experimented with substituting computer algebra by model generation and by proving theorems with a first-order equational theorem prover instead of a proof planner.     

Theorem proving with abstraction

A class of mappings called abstractions are defined, and examples of abstractions are given. These functions map a set S of clauses onto a possibly simpler set T of clauses. Also, resolution proofs from S map onto possibly simpler resolution proofs from T. In order to search for a proof of a clause C from S, it suffices to search for a proof from T and attempt to invert the abstraction mapping to obtain a proof of C from S. Some theorem proving strategies based on this idea are presented. Most of these strategies are complete. A method of using more than one abstraction at the same time is also presented. This requires the use of ‘multiclauses’, which are multisets of literals, and associated ‘m-abstraction mappings’ on multiclauses. Certain abstractions are especially interesting, because they correspond to particular interpretations of the set S of clauses. The use of abstractions permits the advantages of set-of-support strategies to be realized in arbitrary complete non set-of-support resolution strategies.     

Social and Semiotic Analyses for Theorem Prover User Interface Design 1

We describe an approach to user interface design based on ideas from social science, narratology (the theory of stories), cognitive science, and a new area called algebraic semiotics. Social analysis helps to identify certain roles for users with their associated requirements, and suggests ways to make proofs more understandable, while algebraic semiotics, which combines semiotics with algebraic specification, provides rigorous theories for interface functionality and for a certain technical notion of quality. We apply these techniques to designing user interfaces for a distributed cooperative theorem proving system, whose main component is a website generation and proof assistance tool called Kumo. This interface integrates formal proving, proof browsing, animation, informal explanation, and online background tutorials, drawing on a richer than usual notion of proof. Experience with using the interface is reported, and some conclusions are drawn. Received November 1998 / Accepted in revised form June 1999