TY - GEN

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

AU - Jobredeaux, Romain

AU - Herencia-Zapana, Heber

AU - Neogi, Natasha

AU - Feron, Eric

N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18

PY - 2012/12/1

Y1 - 2012/12/1

N2 - 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.

AB - 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.

UR - http://ieeexplore.ieee.org/document/6425966/

UR - http://www.scopus.com/inward/record.url?scp=84874282893&partnerID=8YFLogxK

U2 - 10.1109/CDC.2012.6425966

DO - 10.1109/CDC.2012.6425966

M3 - Conference contribution

SP - 1816

EP - 1821

BT - Proceedings of the IEEE Conference on Decision and Control

ER -