A calculus of quality for robustness against unreliable communication

A main challenge in the development of distributed systems is to ensure that the components continue to behave in a reasonable manner even when communication becomes unreliable. We propose a process calculus, the Quality Calculus, for programming software components where it becomes natural to plan for default behaviour in case the ideal behaviour fails due to unreliable communication and thereby to increase the quality of service offered by the system. The development is facilitated by a SAT-based robustness analysis to determine whether or not the code is vulnerable to unreliable communication. The framework is illustrated on the design of a fragment of a wireless sensor network, and is substantiated by formal proofs of correctness of the analysis, which relate the original reduction semantics of the calculus to a new semantics with explicit substitutions.