Narrow Results

A theory of representation of semiautomata by canonical words and equivalences was developed in [7]. That work was motivated by trace-assertion specifications of software modules, but its focus was entirely on the underlying mathematical model. In the present paper we extend that theory to automata with Moore and Mealy outputs, and show how to apply the extended theory to the specification of modules. In particular, we present a unified view of the trace-assertion methodology, as guided by our theory. We illustrate this approach, and some specific issues, using several nontrivial examples. We include a discussion of finite versus infinite modules, methods of error handling, some awkward features of the trace-assertion method, and a comparison to specifications by automata. While specifications by trace assertions and automata are equivalent in power, there are cases where one approach appears to be more natural than the other. We conclude that, for certain types of system modules, formal specification by automata, as opposed to informal state machines, is not only possible, but practical.

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. The proposed method has some notable features. Among them are as follow:

(1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and

(2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite.

Crème is a tool based on the proposed method. We also report on two case studies in which

(1) Crème proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and

(2) Crème finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property.

Proof scores are documents of comprehensible plans to prove theorems. The proof score approach to systems analysis is a method in which proof scores are used to verify that systems enjoy properties (or analyze systems). In this paper, we describe a way to analyze electronic commerce protocols with the proof score approach, which has been developed and refined through several case studies conducted.

In this paper we introduce a complete rewriting system on any large-type Artin monoid. The rewriting system stems from a well-ordering defined by Burckel on the related class of braid monoids. As a consequence of our rewriting system's existence we will recover the fact that certain large-type monoids are well-orderable, and we will discern finer detail regarding the structure of this associated ordering.