Formal Verification of Distributed System Using an Executable C Model

Abstract

Formal verification means to rigorously explore the correctness of system designs expressed as mathematical models, most likely with the assistance of modern computers. Original approaches were to model and express a distributed system using existing theoretical tools such as Petri Nets. Nevertheless the main problems of such approaches are the restrictions imposed by formal tools and the human factor of simplify and model a distributed system. We propose a way to do formal verification of a distributed system by modeling the communication of the system as a concurrent program, instantiating the distributed system using threads and atomic queues and testing/verifying directly to the source code with specialized verifiers for concurrent programs. As an example, we show the verification of a distributed threshold signer using CBMC verifying properties such as memory leaks, index out of bounds, and data races.