We report on our efforts to formally specify and verify a new protocol of the E-2C Hawkeye Early Warning Aircraft. The protocol, which is currently in test at Northrop Grumman, supports communication between a mission computer (MC) and three or more tactical workstations (TWSs), connected by a single-segment LAN. We modeled the protocol in the PROMELA specification language of the SPIN verification tool, and used SPIN to analyze a number of properties of the protocol. Our investigation revealed a race condition that can lead to a disconnect of an MC/TWS connection when there is one lost UDP datagram and significant timing delays. Such delays are virtually impossible under normal E-2C operating conditions, but could be due to noise on the MC/TWS LAN. A simple modification was proposed that avoids the disconnect in many situations. Practical considerations, however, mandated that the protocol be left as it is: shutting down a noisy connection and reinitializing the TWS, with minimal delay and loss of information to the operator was deemed preferable to operating in a degraded mode.

Probabilistic I/O automata (PIOA) constitute a model for distributed or concurrent systems that incorporates a notion of probabilistic choice. The PIOA model provides a notion of composition, for constructing a PIOA for a composite system from a collection of PIOAs representing the components. We present a method for computing completion probability and expected completion time for PIOAs. Our method is compositional, in the sense that it can be applied to a system of PIOAs, one component at a time, without ever calculating the global state space of the system (i.e. the composite PIOA). The method is based on symbolic calculations with vectors and matrices of rational functions, and it draws upon a theory of observables, which are mappings from delayed traces to real numbers that generalize the classical "formal power series" from algebra and combinatorics. Central to the theory is a notion of representation for an observable, which generalizes the classical notion "linear representation" for formal power series. As in the classical case, the representable observables coincide with an abstractly defined class of "rational" observables; this fact forms the foundation of our method.

This paper describes an algebraic framework for the study of dataflow networks, which form a paradigm for concurrent computation in which a collection of concurrently and asynchronously executing processes communicate by sending messages between port

A CCS-style calculus of dataflow networks with a standard structural operational semantics is defined. A version of weak bisimulation equivalence, called buffer bisimilarity, is defined for this calculus, and its equational theory is investigated. The main result is a completeness theorem for proving equations valid under buffer bisimilarity. The axioms have a familiar, category-theoretic flavor, in which a dataflow process with m input ports and n output ports is represented by an arrow from m to n in a category whose objects are the finite ordinals.>

We consider monotone input/output automata, which model a usefully large class of dataflow networks of indeterminate (or nonfunctional) processes. We obtain a characterization of the relations computable by these automata, which states that a relation R : X ! 2 Y (viewed as a "nondeterministic function") is the input /output relation of an automaton iff there exists a certain kind of Scott domain D, a continuous function F : X ! [D ! Y ] and a continuous function G : X ! P(D), such that R(x) = F (x) y (G(x)) for all inputs x 2 X. Here P denotes a certain powerdomain operator, and y denotes the pointwise extension to the powerdomain of a function on the underlying domain. An attractive feature of this result is that it specializes to two subclasses of automata, determinate automata, for which G is single-valued, and semi-determinate automata, for which G is a constant function. A corollary of the latter result is the impossibility of implementing "angelic merge" by a network of de...

Using concurrent transition systems [Sta86], we establish connections between three models of concurrent process networks, Kahn functions, input/output automata, and labeled processes. For each model, we define three kinds of algebraic operations on processes: the product operation, abstraction operations, and connection operations. We obtain homomorphic mappings, from input/output automata to labeled processes, and from a subalgebra (called “input/output processes”) of labeled processes to Kahn functions. The proof that the latter mapping preserves connection operations amounts to a new proof of the “Kahn Principle.” Our approach yields: (1) extremely simple definitions of the process operations; (2) a simple and natural proof of the Kahn Principle that does not require the use of “strategies” or “scheduling arguments”; (3) a semantic characterization of a large class of labeled processes for which the Kahn Principle is valid, (4) a convenient operational semantics for nondeterminate process networks.

This paper considers a variant of the Byzantine Generals problem, in which processes start with arbitrary real values rather than Boolean values or values from some bounded range, and in which approximate, rather than exact, agreement is the desired goal. Algorithms are presented to reach approximate agreement in asynchronous, as well as synchronous systems. The asynchronous agreement algorithm is an interesting contrast to a result of Fischer et al, who show that exact agreement with guaranteed termination is not attainable in an asynchronous system with as few as one faulty process. The algorithms work by successive approximation, with a provable convergence rate that depends on the ratio between the number of faulty processes and the total number of processes. Lower bounds on the convergence rate for algorithms of this form are proved, and the algorithms presented are shown to be optimal.

Most discussions of semaphore primitives m the literature provide only an informal description of their behavtor, rather than a more prectse definition.These informal descriptions may be incorrect, incomplete, or subject to m~smterpretation.As a result, the literature actually contains several different defimtlons of the semaphore primmves.The differences are important, since the particular choice of definition can affect whether a soluuon to the mutual exclusion problem using semaphore primitives allows the possibility of process starvation.An attempt is made to alleviate some of the confusion by gtving precise defmittons of two varteties of semaphore prtmtttves, here called weak and blocked-set primitives.It is then shown that under certain natural condttious, although it is possible to implement starvation-free mutual exclusion with blocked-set semaphores, it is not possible to do so with weak semaphores.Thus weak semaphores are strictly less "powerful" than blocked-set semaphores.