Proofs about Network Communication: For Humans and Machines

TL;DR

This paper introduces a method for creating machine-checked, human-understandable proofs of bisimilarity in network communication systems, enhancing assurance in safety-critical distributed systems.

Contribution

It presents a novel approach to conduct human-readable, machine-verified bisimilarity proofs specifically for network communication protocols.

Findings

Proofs are both machine-checked and understandable by humans.

The approach improves assurance in safety-critical distributed systems.

Facilitates verification of implementation adherence to specifications.

Abstract

Many concurrent and distributed systems are safety-critical and therefore have to provide a high degree of assurance. Important properties of such systems are frequently proved on the specification level, but implementations typically deviate from specifications for practical reasons. Machine-checked proofs of bisimilarity statements are often useful for guaranteeing that properties of specifications carry over to implementations. In this paper, we present a way of conducting such proofs with a focus on network communication. The proofs resulting from our approach are not just machine-checked but also intelligible for humans.