Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

An autonomous multistrategy theorem proving system using knowledge-based techniques

Most general-purpose theorem-proving systems have weak search control. There is no alternative to the use of a large number of heuristics or strategies for search guidance. Choosing appropriate strategies for solving a given problem may require the knowledge of different strategies and may involve a lot of painstaking trial-and-error. To encourage the widespread use of computer reasoning systems, it is important that a theorem prover be usable by those with little knowledge of problem-solving strategies, and that a theorem prover be able to select good strategies for the user. An autonomous multistrategy theorem-proving system is developed, using knowledge-based techniques, to entirely free the user from the necessity of understanding the system or the merits of different strategies. All the user has to do is input his or her problem in first-order logic, and the system solves the problem efficiently for him or her without any manual intervention. The system embodies much of expert knowledge about how to solve problems. The knowledge is represented as metarules in knowledge base which guide a hyperlinking theorem prover to solve problems automatically and efficiently.     

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.     

Constructor-based observational logic

This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. In the first part of this work, we develop the essential ingredients that are needed to define the constructor-based observational logic institution, called COL, which takes into account both the generation- and observation-oriented aspects of software systems. The underlying paradigm of our approach is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the “black box” semantics of a specification which is useful to study the behavioral properties a user can observe when he/she is experimenting with the system.In the second part of this work, we develop proof techniques for structured COL-specifications. For this purpose we introduce an institution encoding from the COL institution to the institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language Casl. This means, in particular, that any inductive theorem prover, such as e.g. the Larch Prover or PVS, can be used to prove theorems over structured COL-specifications.     

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.     

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies, which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.     

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.     

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     

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     

The design and analysis of real-time systems using the ASTRAL software development environment

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the ASTRAL Software Development Environment (SDE), which is an integrated set of design and analysis tools based on the ASTRAL formal framework. The tools that make up the support environment are a syntax-directed editor, a specification processor, a verification condition generator, a browser kit, a model checker, and a mechanical theorem prover. This revised version was published online in June 2006 with corrections to the Cover Date.     

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.     

Specification and Verification of Concurrent Programs Through Refinements

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.     

Using induction and rewriting to verify and complete parameterized specifications

In software engineering there is a growing demand for formal methods for the specification and validation of software systems. The formal development of a system might give rise to many proof obligations. We must prove the completeness of the specification and the validity of some inductive properties. In this framework, many provers have been developed. However they require much user interaction even for simple proof tasks. In this paper, we present new procedures to test sufficient completeness and to prove or disprove inductive properties automatically in para-meterized conditional specifications. The method has been implemented in the prover SPIKE. Computer experiments illustrate the improvements in length and structure of proofs, due to parameterization. Moreover, SPIKE offers facilities to check and complete specifications.     

Formal Memory Models for the Verification of Low-Level Operating-System Code

This article contributes to the field of operating-systems verification. It presents a formalization of virtual memory that extends to memory-mapped devices. Our formalization consists of a stack of three detailed formal memory models: physical memory (i.e., RAM), physically-addressable memory-mapped devices (including their respective side effects, access and alignment requirements), and page-table based virtual memory. Each model is formally shown to satisfy the plain-memory specification, a memory abstraction that enables efficient reasoning for type-correct programs. This stack of memory models was developed in an attempt to verify Nova, the Robin micro-hypervisor. It is a key component of our verification environment for operating-system kernels based on the interactive theorem prover PVS.     

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

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

A case-based approach to software reuse

This software reuse system helps a user build programs by reusing modules stored in an existing library. The system, dubbed caesar (Case-basEd SoftwAre Reuse), is conceived in the case-based reasoning framework, where cases consist of program specifications and the corresponding C language code. The case base is initially seeded by decomposing relevant programs into functional slices using algorithms from dataflow analysis. caesar retrieves stored specifications from this base and specializes and/or generalizes them to match the user specification. Testing techniques are applied to the construct assembled by caesar through sequential composition to generate test data which exhibits the behavior of the code. For efficiency, inductive logic programming techniques are used to capture combinations of functions that frequently occur together in specifications. Such combinations may be stored as new functional slices.     

Automated structural analysis of SCR‐style software requirements specifications using PVS

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)‐style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd.