Developing proof carrying code to formally assure termination in fault tolerant distributed controls systems

We address the semantic gap between the model and the implementation of control algorithms for distributed systems in a formal fashion: we provide an interactive (partially automated) method by which to translate the global, model level theoretical properties, such as stability and convergence, into code level assertions and invariants which assure termination of the relevant implementations and validity of the result. We outline a simple flight control system example for altitude holding, and describe a fault-tolerant distributed agreement protocol among n processor nodes, in the presence of a varying network topology. We develop a Lyapunov-like function for the distributed algorithm, and attain a polynomial time theoretical bound on the convergence time T_conv ∝ n³. We then exploit the Lyapunov function and convergence proof, in order to derive requisite ANSI-C Specification Language (ACSL) annotations for the C code distributed implementation, in order to guarantee termination. The ACSL annotations can then be used to automatically generate formal proof obligations via the Frama-C tool. These proof obligations also encompass assertions relating to timing, memory allocation, type checking and processor specific issues. The proof obligations can then be automatically discharged using a theorem prover, and their success guarantees that the behavior of the corresponding distributed code will evince the global properties proven for the model. Thus, the verification process spans efforts from the high-level control theory to the low-level implementation as a C program.