A theory of slicing non-deterministic programs and systems is developed. Non-deterministic programs and systems are represented as non-deterministic program graphs (NDPGs) that allow arbitrary non-deterministic branching to be expressed. Structural and ...

We propose an extension to ATL (alternating-time temporal logic), called BSIL (basic strategy-interaction logic), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL⁺ but incomparable ...

We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with refinement types for ...

Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, ...

We present a method for specification and verification of distributed systems that communicate via asynchronous message passing. The method handles both safety and liveness properties. It is compositional, i.e., a specification of a composite system can ...

The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including equivalence ...

A stepwise refinement heuristic to construct distributed systems is presented. The heuristic is based on a conditional refinement relation between system specifications, and a “Marking”. It is applied to construct four sliding window protocols that ...

Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly ...

Leslie Lamport presented a set of axioms in 1979 that capture the essential properties of the temporal relationships between complex and perhaps unspecified activities within any system, and proceeded to use this axiom system to prove the correctness of ...

A self-stabilizing system has the property that, no matter how it is perturbed, it eventually returns to a legitimate configuration. Dijkstra originally introduced the self-stabilization problem and gave several solutions for a ring of processors in his ...

An issue of current interest in the Open Systems Interconnection (OSI) field is the choice of a language well suited to specification and verification. For this purpose, two languages based on Milner's communication calculi are proposed, respectively ...

Consider a network of communicating finite state machines that exchange messages over unbounded FIFO channels. Each machine in the network can be defined by a directed graph whose nodes represent the machine states and whose edges represent its ...

Generative communication is the basis of a new distributed programming langauge that is intended for systems programming in distributed settings generally and on integrated network computers in particular. It differs from previous interprocess ...