Linearizability and progress properties are key correctness notions for concurrent objects. This paper presents novel verification techniques for both property classes. The key of our techniques is based on the branching bisimulation equivalence. We first show that it suffices to check linearizability on the quotient object program under branching bisimulation. This is appealing, as it does not rely on linearization points. Further, by exploiting divergence-sensitive branching bisimilarity, our approach proves progress properties (e.g., lock-, wait-freedom) by comparing the concurrent to-be-verified object program against an abstract program consisting of atomic blocks. Our work thus enables the usage of well-known proof techniques for branching bisimulation to check the correctness of concurrent objects. The potential of our approach is illustrated by verifying linearizability and lock-freedom of 14 benchmark algorithms from the literature. Our experiments confirm one known bug and reveals one new bug.

Metamorphic testing is a technique for the verification of software output without a complete testing oracle. Mathematical optimization, implemented in software, is a problem for which verification can often be challenging. In this paper, we apply metamorphic testing to one such optimization problem, the quadratic assignment problem (QAP). From simple observations of the properties of the QAP, we describe how to derive a number of metamorphic relations useful for verifying the correctness of a QAP solver. We then compare the effectiveness of these metamorphic relations, in "killing" mutant versions of an exact QAP solver, to a simulated oracle. We show that metamorphic testing can be as effective as the simulated oracle for killing mutants. We examine the relative effectiveness of different metamorphic relations, both singly and in combination, and conclude that combining metamorphic relations can be significantly more effective than using a single relation.

Environment abstraction enriches predicate abstraction by idea from counter abstraction to develop a framework for verification of parameterized systems. However, despite various effects, the constructed abstractions still go beyond the capability of the usual model checkers for many realistic systems. In this paper, a new technique, called state clustering, is proposed to group local states into a small number of clusters, by purely syntactic analysis. The size of array variables in the resulting abstractions are further reduced using parameter abstraction technique. By combining different abstraction techniques, real-life cache coherence protocols such as FLASH have been successfully verified.

We propose a modal logic for modular pi calculus: a logic to specify both temporal and spatial properties for processes in modular pi calculus. Characterization of process equivalence the logic induce is investigated, and it is shown that the distinguishing power of the logic falls between bisimilarity and structural congruence. Then a model checking algorithm for the logic over the finite-control subset of modular pi calculus is presented, and its correctness proved.

A new approach to combining invariants computing and guard strengthening methods is presented in the context of parameter abstraction for parameterized model checking of cache coherence protocols. The approach uses a small instance of a parameterized protocol as a "reference model" to compute candidate invariants. References to a specific node in these candidate invariants are then abstracted away, and the resulting formulas are used to strengthen guards of the transition rules in the abstract node. The correctness of the approach is guaranteed by symmetry which exists in many parameterized systems. A number of case studies have been carried out to illustrate the effectiveness of the approach. During the process a data consistency error was identified and fixed in the German 2004 cache coherence protocol.

A predicate sequencing constraint logic (PSCL) is proposed to represent test purpose for concurrent program testing. The logic is capable of expressing not only sequencing relationships among input and output events, but also data dependencies between event parameters. A PSCL-based symbolic test generation method is developed to automatically derive symbolic test cases that incorporate given data dependency constraints as verdict conditions. The method works in a syntactic way without referring to concrete program states and the derived test cases allow dynamic test data selection according to the response from the software under test. The advantage of the approach is demonstrated with a case study.

An extension of symbolic transition graphs with assignment is proposed which combines the advantages of both the assignment-before-action and the assignment-after-action approaches: like the former it allows a simple set of rules to be designed for generating finite symbolic graphs from regular value-passing process descriptions; like the later it avoids creating multiple copies in the graph for a recursive process definition. Experiences show that, in most cases, considerable reductions in verification time and space can be achieved using the new approach.

Summary form only given. Mobile computing provides a new paradigm for organizing and implementing computation over the Internet. There are two computational phenomena that involve mobility: code mobility and computation mobility. The former happens when pieces of code (such as Applets) move between computing devices, while the later concerns computation carried out in computing device (such as laptops) which change locations. Mobile computing has posed serious challenges to the safety and security of Internet-based systems. Theories and techniques are needed to decide if code coming from outside can be trusted, or to determine if a computation movement is safe, and so on. This work first reviews some formal methods that have recently been proposed for such purposes. These methods are based on either theorem proving or model checking, and each emphasizes on certain aspects of trustworthy computing. Then it focuses on a model checking approach to mobile computing. Traditionally model checking is based on modal logics which are appropriate for describing the temporal behaviors of systems. Since in mobile computing processes may evolve not only in time but also in space, efforts have recently been made to extend these logics with spatial modalities (to describe location changes), and to design model checking algorithms for them. However, so far there still lacks a satisfactory approach to introducing recursion into such spatial logics, due to subtle interplay between recursion and first-order quantification. We take the challenging task to extend a spatial ambient logic with fixpoints, yielding a predicate-based mu-calculus in which fixpoint formulas are formed using predicate variables. We also develop an algorithm for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for an ambient logic with recursion.

An algorithm for model checking value-passing processes is presented. Processes are modeled as symbolic transition graphs with assignments. To specify properties for such processes a graphical predicate mu-calculus is introduced. It allows arbitrary nesting of the least and greatest fixpoints, and contains the propositional mu-calculus as a proper subset. The algorithm instantiates input variables on-the-fly and states are only generated when they are needed for the computation. To handle alternating fix-points properly, a multi-stack is employed and the controlling strategy is such that a state is evaluated without depending on the default values for more deeply nested states. The algorithm is shown correct with respect to the semantics of the predicate mu-calculus. Its complexity is also analysed.

Abstract We give sound and complete proof systems for a variety of bisimulation based equivalences over a message-passing process algebra. The process algebra is a generalisation of pure CCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operator a.p is replaced by the two operators c?x.p and c!e.p and in addition messages can be tested by a conditional construct. The various proof systems are parameterised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.

An implementation of an algebraic specification in an imperative programming language consists of a representation type, together with an invariant and an equivalence relation over it, and a procedure for each operator in the specification. A formal technique is developed to check the correctness of an implementation with respect to its specification. Here “correctness” means that the implementation satisfies the axioms and preserves the behavior of the specification. Within legal representing value space, a correct implementation behaves like a desirable model of the specification. A notion of implementation refinement is also proposed, and it is shown that the correctness relation between implementations and specifications is preserved by implementation refinement. In the extreme case the procedures in an implementation may be pre-post-condition pairs. Such abstract implementations can be refined into executable code by refining the abstract procedures in it. In this way a formal link between the algebraic and the pre- post-condition specification techniques is established.

Abstract A categorical semantics of multiple inheritance is presented, in which the inheritance relations between program entities are represented as commutative diagrams in a suitable category, and multiple inheritance is then modelled with colimits of such diagrams. It is shown that the informal semantics of multiple inheritance used in existing object-oriented programming languages conforms to, or is consistent with, this model.