A Highly Dependable Computing Architecture for Safety-Critical Control Applications

More and more technical systems are supervised, controlled and regulated by programmable electronic systems. The dependability of the entire system depends heavily on the safety of the embedded software. But the technological trend to entrust software with tasks of growing complexity and safety relevance conflicts with the lacking acceptance of rigorous proofs of software safety. Based on an international standard for higher level programming languages for programmable logic controllers (PLC, IEC 1131-3), a mathematically based method for validating the behavioral correctness and the functional safety of graphical designs of safety-critical control applications is introduced. The design elements taken from a domain specific module library are proven correct and safe only once. The functional correctness and satisfaction of safety requirements of new application graphical programs can then be shown effectively by reference to the proven properties of the library components used. This approach is part of an comprehensive computing architecture for safety-critical control programs which is presented in a survey.     

Adapting functional programs to higher order logic

Higher-order logic proof systems combine functional programming with logic, providing functional programmers with a comfortable setting for the formalization of programs, specifications, and proofs. However, a possibly unfamiliar aspect of working in such an environment is that formally establishing program termination is necessary. In many cases, termination can be automatically proved, but there are useful programs that diverge and others that always terminate but have difficult termination proofs. We discuss techniques that support the expression of such programs as logical functions. Electronic Supplementary Material  The online version of this article () contains supplementary material, which is available to authorized users.     

A Trustworthy Proof Checker

Proof-carrying code (PCC) and other applications in computer security require machine-checkable proofs of properties of machine-language programs. The main advantage of the PCC approach is that the amount of code that must be explicitly trusted is very small: it consists of the logic in which predicates and proofs are expressed, the safety predicate, and the proof checker. We have built a minimal proof checker, and we explain its design principles and the representation issues of the logic, safety predicate, and safety proofs. We show that the trusted computing base (TCB) in such a system can indeed be very small. In our current system the TCB is less than 2,700 lines of code (an order of magnitude smaller even than other PCC systems), which adds to our confidence of its correctness.     

Equivalent logic programs and symmetric homogeneous forms of logic programs with equality

This article introduces the notion of CAS-equivalent logic programs: logic programs with identical correct answer substitutions. It is shown that the notions CAS-equivalence, refutational equivalence, and logical equivalence do not coincide in the case of definite clause logic programs. Least model criteria for refutational and CAS-equivalence are suggested and their correctness is proved. The least model approach is illustrated by two proofs of CAS-equivalence. It is shown that the symmetric extension of a logic program subsumes the symmetry axiom and the symmetric homogeneous form of a logic program with equality subsumes the symmetry, transitivity, and predicate substitutivity axioms of equality. These results contribute towards the goal of building equality into standard Prolog without introducing additional inference rules.     

Semantic Determinism and Functional Logic Program Properties

In modern functional logic languages like Curry or Toy, programs are possibly non-confluent and non-terminating rewrite systems, defining possibly non-deterministic non-strict functions. Therefore, equational reasoning is not valid for deriving properties of such programs. In a previous work we showed how a mapping from CRWL –a well known logical framework for functional logic programming– into logic programming could be in principle used as logical conceptual tool for proving properties of functional logic programs. A severe problem faced in practice is that simple properties, even if they do not involve non-determinism, require difficult proofs when compared to those obtained using equational specifications and methods. In this work we improve our approach by taking into account determinism of (part of) the considered programs. This results in significant shortenings of proofs when we put in practice our methods using standard systems supporting equational reasoning like, e.g., Isabelle.     

Verifying a logic-synthesis algorithm and implementation: a casestudy in software verification

We describe the verification of a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof development system to reason about functional programs. The approach hides implementation details and uses higher order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher order proof system, and can aid in the future verification of large software implementations     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

Inter-process buffers in separation logic with rely-guarantee

Separation logic allows simple proofs of concurrent algorithms which use blocking mechanisms such as semaphores. It can even deal with non-blocking algorithms. With the addition of mechanisms borrowed from rely-guarantee, we can make reasonably simple proofs of some simple non-blocking algorithms. We show that it extends to proofs of some intricate algorithms, including Simpson’s famous asynchronous four-slot buffer and Harris’s novel three-slot algorithm, in a manner that is arguably simpler than earlier treatments, though we cannot claim that we have yet found proofs that are as simple as we would wish. Our example proofs show functional correctness but do not deal with questions of liveness.     

Control Structure Abstractions of the Backtracking Programming Technique

Backtracking is a well-known technique for solving combinatorial problems. It is of interest to programming methodologists because 1) correctness of backtracking programs may be difficult to ascertain experimentally and 2) efficiency is often of paramount importance. This paper applies a programming methodology, which we call control structure abstraction, to the backtracking technique. The value of control structure abstraction in the context of correctness is that proofs of general properties of a class of programs with similar control structures are separated from proofs of specific properties of individual programs of the class. In the context of efficiency, it provides sufficient conditions for correctness of an initial program which may subsequently be improved for efficiency while preserving correctness.     

A shared-variable concurrency analysis of multi-threaded object-oriented programs

In this paper a proof outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. The main contribution is a generalization of the Owicki& Gries proof method for shared-variable concurrency to dynamic thread creation. This paper also provides a formal justification of this generalization in terms of soundness and completeness proofs.     

RGITL: A temporal logic framework for compositional reasoning about interleaved programs

This paper gives a self-contained presentation of the temporal logic Rely-Guarantee Interval Temporal Logic (RGITL). The logic is based on interval temporal logic (ITL) and higher-order logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles of symbolic execution and induction, known from the verification of sequential programs, which are transferred to a concurrent setting with temporal logic. We include an interleaving operator with compositional semantics. As a consequence, the calculus permits proving decomposition theorems which reduce reasoning about an interleaved program to reasoning about individual threads. A central instance of such theorems are rely-guarantee (RG) rules, which decompose global safety properties. We show how the correctness of such rules can be formally derived in the calculus. Decomposition theorems for other global properties are also derivable, as we show for the important progress property of lock-freedom. RGITL is implemented in the interactive verification environment KIV. It has been used to mechanize various proofs of concurrent algorithms, mainly in the area oflinearizable and lock-free algorithms.     

On the use of history variables

Summary This paper is a response to a suggestion that the use of history variables in proofs of the correctness of programs is unnecessary. It is argued that the use of history or ghost variables can be of benefit in improving the clarity of some proofs; that without their use some proofs require programming techniques which are at variance with the widely-accepted tenets of structured programming and that for some proofs of correctness their use is unavoidable.     

Proving the Correctness of Multiprocess Programs

The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.     

Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm

We describe a proof method that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This method provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This method makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate it with parts of a substantial example—the synthesis of a unification algorithm.     

Studies of a Theory of Specifications with Built-in Program Extraction

We present a Theory of Specifications based on Martin-Löf's type theory, with rules for simultaneously constructing programs and their correctness proofs. The theory contains types for representing specifications whose corresponding notion of implementation is that of a pair formed by a program and a correctness proof. The rules of the theory are such that in implementations the program parts appear mixed together with the proof parts. A confluent and normalizing computational relation performs the task of separating programs from proofs. As a consequence, every implementation computes to a pair composed of a program and a proof of its correctness, and so the program extraction procedure is immediate.     

概率拟Hoare逻辑

基于Hoare逻辑,给出了概率拟Hoare逻辑,用于刻画程序执行的正确度,定量地描述理论与程序(或软件)实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性,以及解释正确度很高的两个程序串行复合之后的整体正确度可能并不高等问题。     

Normalising the associative law: An experiment with Martin-Löf's type theory

Martin-Löf's type theory contains a logic, a specification language and a programming language, so it is a tool with different uses. Although it is traditionally used as anintegrated programming logic, it may well be used as anexternal logic, which is necessary if one wants to use the formalism of type theory to verify the correctness of an external program. Different tools, such as well founded recursion, measure functions, or the separation of correctness into termination and partial correctness, may be used to obtain a correct type theory program. Type theory is viewed as anopen system with respect toinductively defined types and predicates, which makes it easy to represent an external program as agraph. Formal proofs have been edited using Larry Paulson's ISABELLE.     

Termination of Nested and Mutually Recursive Algorithms

This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion.We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthys f_91 function).     

A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions

A typed program logic LMF for recursive specification and verification is presented. It comprises a strict functional programming language with polymorphic and recursively defined partial functions and polymorphic data types. The logic is two-valued with the equality symbol as only predicate. Quantifiers range over the values, which permits inductive proofs of properties. The semantics is based on a contextual (observational) semantics, which gives a consistent presentation of higher-order functions. Our analysis also sheds new light on the the role of partial functions and loose specifications. It is also an analysis of influence of extensions of programs on the tautologies. The main result is that universally quantified equations are conservative, which is also the base for several other conservative classes of formulas.