The current trend toward portable computing systems (e.g., cellular phones, laptop computers) brings with it the need for a new paradigm to facilitate thinking about and designing distributed applications. We use the term mobile to refer to distributed systems that include moving, autonomous agents which loosely cooperate to accomplish a task. The fluid nature of the interconnections among components of a mobile system provides new challenges and opportunities for the research community. While we do not claim to have fully grasped all the issues involved in specifying and modeling such systems, we believe that the notions of place, time, and action will play a central role in any model that is developed. We show that these concepts can be expressed and reasoned about in the UNITY logic with a minimal amount of additional notation. The formal derivation of a control system for a radio-dispatched elevator is used to show how considerations involving place, time, and actions impact the design process, be it formal or semiformal.

As critical computer systems continue to grow in complexity, the task of showing that they execute correctly becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e., rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used in the design of concurrent systems do not provide any mechanisms for specifying and reasoning about the mapping of software to hardware. As a result, architectural constraints, even though they play an important role in the design process, are left out of the formal framework. We show how to state architectural constraints in a formal notation, how to prove that programs are allocated correctly to the underlying architecture, and how to factor architectural considerations into a program derivation process which uses a mixture of specification and program refinements. The approach is illustrated by the derivation of two related programs that solve the same problem but are designed to work on distinct architectures.>

Synchrony continues to be an important concern in concurrent programming. Existing languages and models have introduced a great diversity of constructs for expressing and managing synchronization among sequential processes or atomic actions. The authors put forth a model in which synchrony is viewed as a relation among atomic actions, a relation which may evolve with time. The model is shown to be convenient for expressing formally the semantics of synchrony as it appears in many of the languages and models proposed to date. Among such models Swarm is singled out for its use of dynamic synchrony. The Swarm notation is briefly reviewed. A new concurrent algorithm for the leader election problem illustrates the use of dynamic synchrony in Swarm.>

A method for formal derivation of distributed programs is presented. The approach uses programwide assertions to formulate safety and progress properties of computations. Assertions are used to state functional requirements of the program as well as structural and behavioral constraints imposed by the choice of underlying architecture. The significance of this latter feature is that it offers a single, unified formal framework for integrating functional requirements and architectural constraints.>