A temporal logic approach to object certification

A brief overview is made of the use of temporal logic formalisms for specifying and verifying concurrent systems in general and information systems in particular. The requirements imposed by object-orientation on such formalisms are examined. A logic is proposed fulfilling those requirements (except concerning non-monotonic features), allowing the uniform treatment of both local and global properties of systems with concurrent, interacting components organized in classes, and supporting specialization. A semantics and a calculus (following an axiomatic, Hilbert style) are presented in detail. The calculus includes rules for the sound inheritance and reflection of theorems between classes. Practical aspects of the usage of such a logic for both specification and verification are considered. To this end a set of metatheorems is provided for expediting the proof of invariants. Finally, the need and availability of automatic theorem proving for systems querying is briefly discussed.     

A verification system for concurrent programs based on the Boyer-Moore prover

We describe a mechanical proof system for concurrent programs, based on a formalization of the temporal framework of Manna and Pnueli as an extension of the computational logic of Boyer and Moore. The system provides a natural representation of specifications of concurrent programs as temporal logic formulas, which are automatically translated into terms that are subject to verification by the Boyer-Moore prover. Several specialized derived rules of inference are introduced to the prover in order to facilitate the verification of invariance (safety) and eventuality (liveness) properties. The utility of the system is illustrated by a correctness proof for a two-process program that computes binomial coefficients.     

Compositional reasoning using intervals and time reversal

Interval Temporal Logic (ITL) is an established formalism for reasoning about time periods. We investigate some simple kinds of ITL formulas which have application to compositional reasoning and furthermore are closed under conjunction and the conventional temporal operator known both as “box” and “always”. Such closures help us modularly construct formulas from simple building blocks in a way which preserves useful compositional properties. The most important class considered here is called the 2-to-1 formulas. They offer an attractive framework for analysing sequential composition in ITL and provide the formal basis for most of the subsequent presentation. A key contribution of this work concerns a useful and apparently new and quite elementary mathematical theorem that 2-to-1 formulas are closed under “box”. We also use a natural form of time symmetry with 2-to-1 formulas. This extends known facts about such formulas by looking at them in reverse. An important example involves showing that 2-to-1 formulas are also closed under a variant of “box” for prefix subintervals rather than suffix ones. We then apply the compositional formulas obtained with time symmetry to analyse concurrent behaviour involving mutual exclusion in both Peterson’s algorithm and a new and more abstract one. At present, our study of mutual exclusion mainly serves as a kind of experimental “proof of concept” and research tool to develop and illustrate some of the logical framework’s promising features. We also discuss how time symmetry sometimes assists in reducing reasoning in ITL to conventional linear-time temporal logic.     

Reasoning about plan revision in BDI agent programs

Facilities for handling plan execution failures are essential for agents which must cope with the effects of nondeterministic actions, and some form of failure handling can be found in most mature agent programming languages and platforms. While such features simplify the development of more robust agents, they make it hard to reason about the execution of agent programs, e.g., to verify their correctness. In this paper, we present an approach to the verification of agent programs which admit exceptional executions. We consider executions of the BDI-based agent programming language 3APL in which plans containing non-executable actions can be revised using plan revision rules, and present a logic for reasoning about normal and exceptional executions of 3APL programs. We provide a complete axiomatization for the logic and, using a simple example, show how to express properties of 3APL programs as formulas of the logic.     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

Distributed reasoning with ontologies and rules in order-sorted logic programming

Integrating ontologies and rules on the Semantic Web enables software agents to interoperate between them; however, this leads to two problems. First, reasoning services in SWRL (a combination of OWL and RuleML) are not decidable. Second, no studies have focused on distributed reasoning services for integrating ontologies and rules in multiple knowledge bases. In order to address these problems, we consider distributed reasoning services for ontologies and rules with decidable and effective computation. In this paper, we describe multiple order-sorted logic programming that transfers rigid properties from knowledge bases. Our order-sorted logic contains types (rigid sorts), non-rigid sorts, and unary predicates that distinctly express essential sorts, non-essential sorts, and non-sortal properties. We formalize the order-sorted Horn-clause calculus for such properties in a single knowledge base. This calculus is extended by embedding rigid-property derivation for multiple knowledge bases, each of which can transfer rigid-property information from other knowledge bases. In order to enable the reasoning to be effective and decidable, we design a query-answering system that combines order-sorted linear resolution and rigid-property resolution as top-down algorithms.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

良基归纳法在时序逻辑程序不变式验证中的应用

并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义.以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证.提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式,尤其是循环结构的不变量性质.     

LORETO: a tool for reducing state explosion in verification of LOTOS programs

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value‐passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu‐calculus. The reduced system with respect to ρ preserves the truth value of all selective mu‐calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non‐standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms. This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

A Branching Time Temporal Framework for Quantitative Reasoning

Temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) have become popular for specifying temporal properties over a wide variety of planning and verification problems. In this paper we work towards building a generalized framework for automated reasoning based on temporal logics. We present a powerful extension of CTL with first-order quantification over the set of reachable states for reasoning about extremal properties of weighted labeled transition systems in general. The proposed logic, which we call Weighted Quantified Computation Tree Logic (WQCTL), captures the essential elements common to the domain of planning and verification problems and can thereby be used as an effective specification language in both domains. We show that in spite of the rich, expressive power of the logic, we are able to evaluate WQCTL formulas in time polynomial in the size of the state space times the length of the formula. Wepresent experimental results on the WQCTL verifier.     

Reasoning about memory layouts

Verification methods for memory-manipulating C programs need to address not only well-typed programs that respect invariants such as the split-heap memory model, but also programs that access through pointers arbitrary memory objects such as local variables, single struct fields, or array slices. We present a logic for memory layouts that covers these applications and show how proof obligations arising during the verification can be discharged automatically using the layouts. The framework developed in this way is also suitable for reasoning about data structures manipulated by algorithms, which we demonstrate by verifying the Schorr-Waite graph marking algorithm.     

Proofs of randomized algorithms in Coq

Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of programs. Thus, providing tools for the mechanization of reasoning is an important issue. This paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distributions (Giry, Ramsey and Pfeffer). It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory. Instead it uses functional and algebraic properties of unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy specified properties. This approach addresses only discrete distributions and gives rules for analyzing general recursive functions.We apply this theory to the formal proof of a program implementing a Bernoulli distribution from a coin flip and to the (partial) termination of several programs. All the theories and results presented in this paper have been fully formalized and proved in the Coq proof assistant.     

Completeness of the Accumulation Calculus

The accumulation calculs(AC for short)is an interval based temporal logic to specify and reason about hybrid real-time systems.This paper presents a formal proof system for AC,and proves that the system is complete relative to that of Interval Temporal Logic(ITL for short)on real domain.     

Properties of Concurrent Programs

A program property is a predicate on programs. In this paper we explore program properties for safety, progress and parallel composition, of the form U ? V where U and V are either predicates on states of a program or program properties, and ? satisfies three rules that are also enjoyed by implication. We show how such properties can be used to reason about concurrent programs. Our motivation is to explore methods of reasoning based on a very small number of widely-known rules.     

Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.     

A unified formal basis for the CASE tools system

XYZ system is a CASE tools system based on a temporal logic language XYZ/E which can represent every essential feature of conventional HLL's (sequential or concurrent), specifications of different levels, production rules, operational semantics of graphic languages in a uniform framework. With this formal language as the common basis, all the CASE tools including various kinds of graphic tools for distributed process, concurrent programs with phased memory and sequential programs, tools for verification, rapid-prototyping, language transformation, and module management can be connected freely to form more sophisticated and integrated systems.     

Beyond contracts for concurrency

SCOOP is a concurrent programming language with a new semantics for contracts that applies equally well in concurrent and sequential contexts. SCOOP eliminates race conditions and atomicity violations by construction. However, it is still vulnerable to deadlocks. In this paper we describe how far contracts can take us in verifying interesting properties of concurrent systems using modular Hoare rules and show how theorem proving methods developed for sequential Eiffel can be extended to the concurrent case. However, some safety and liveness properties depend upon the environment and cannot be proved using the Hoare rules. To deal with such system properties, we outline a SCOOP Virtual Machine (SVM) as a fair transition system. The SVM makes it feasible to use model-checking and theorem proving methods for checking global temporal logic properties of SCOOP programs. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation. P. J. Brooke, R. F. Paige and Dong Jin Song This work was conducted under an NSERC Discovery grant.