Search

The possibility of partial failure occuring at any stage of computation complicates rigorous formal treatment of distributed algorithms. We propose a methodology for formalising and proving the correctness of distributed algorithms which alleviates this complexity. The methodology uses fault-tolerance bisimulation proof techniques to split the analysis into two phases, that is a failure-free phase and a failure phase, permitting separation of concerns. We design a minimal partial-failure calculus, develop a corresponding bisimulation theory for it and express a consensus algorithm in the calculus. We then use the consensus example and the calculus theory to demonstrate the benefits of our methodology. [ABSTRACT FROM AUTHOR]

In general, faults cannot be prevented; instead, they need to be tolerated to guarantee certain degrees of software dependability. We develop a theory for fault tolerance for a distributed pi-calculus, whereby locations act as units of failure and redundancy is distributed across independently failing locations. We give formal definitions for fault tolerant programs in our calculus, based on the well studied notion of contextual equivalence. We then develop bisimulation proof techniques to verify fault tolerance properties of distributed programs and show they are sound with respect to our definitions for fault tolerance. [ABSTRACT FROM AUTHOR]

We develop a behavioural theory of distributed programs in the presence of failures such as nodes crashing and links breaking. The framework we use is that of , a language in which located processes, or agents, may migrate between dynamically created locations. In our extended framework, these processes run on a distributed network, in which individual nodes may crash in fail-stop fashion or the links between these nodes may become permanently broken. The original language, , is also extended by a ping construct for detecting and reacting to these failures. We define a bisimulation equivalence between these systems, based on labelled actions which record, in addition to the effect actions have on the processes, the effect on the actual state of the underlying network and the view of this state known to observers. We prove that the equivalence is fully abstract, in the sense that two systems will be differentiated if and only if, in some sense, there is a computational context, consisting of a surrounding network and an observer, which can see the difference. [ABSTRACT FROM AUTHOR]

We focus on techniques for proving behavioural equivalence between systems in , a distributed version of the in which processes may migrate between dynamically created locations, and where resource access policies are implemented by means of capability types. We devise a tractable collection of auxiliary proof methods, relying mainly on the use of bisimulations up-to β-reductions, which considerably relieve the burden of exhibiting witness bisimulations. Using such methods we model simple distributed protocols, such as crossing a firewall, a server and its clients, metaservers installing memory services, and address their correctness in a relatively simple manner. [ABSTRACT FROM AUTHOR]

We study type-safety properties of open distributed systems of mobile agents, where not all sites are known to be well-typed. We adopt the underlying model of an anonymous network, allowing that code may be corrupted on transmission and that the source of incoming code is unknowable. Nonetheless, we are able to guarantee a weak form of type-safety at "good" sites using a mix of static and dynamic typing. [ABSTRACT FROM AUTHOR]

We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPP, Basic Parallel Processes, obtained by omitting the restriction operator from CCS. Decision procedures are given for both strong and weak versions of causal bisimulation, location equivalence and ST-bisimulation. [ABSTRACT FROM AUTHOR]