Provably correct implementation of the AbC calculus

摘要

Building open, distributed systems while guaranteeing a specific behaviour is difficult because of the dynamicity of the operating environments and the complexity of the interactions of their components. The AbC calculus provides a novel communication mechanism to select interacting partners based on their runtime capabilities, making it naturally to model complex interactions and adaptive behaviour in such systems. The formal account of this calculus has enabled constructing formally verifiable models and proving their properties. In this paper, we ⅰ) propose an implementation of AbC using the Erlang language ⅱ) formalize the operational semantics of our implementation; ⅲ) propose a set of rules that given an AbC specification, automatically generate Erlang executable code; and ⅳ) prove that the proposed translation is correct by establishing a simulation relation between source and target specifications. This enables us to guarantee that any property proved for a given AbC specification is preserved by the corresponding implementation.