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

Romain Jobredeaux, Heber Herencia-Zapana, Natasha Neogi, Eric Feron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

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 ∝ n3. 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. © 2012 IEEE.
Original languageEnglish (US)
Title of host publicationProceedings of the IEEE Conference on Decision and Control
Pages1816-1821
Number of pages6
DOIs
StatePublished - Dec 1 2012
Externally publishedYes

Fingerprint

Dive into the research topics of 'Developing proof carrying code to formally assure termination in fault tolerant distributed controls systems'. Together they form a unique fingerprint.

Cite this