A formal approach for the synthesis and implementation of fault-tolerant industrial embedded systems

Wei-Tsun Sun (1) , Alain Girault (1) , Gwenaël Delaval (2)

1 SPADES - Sound Programming of Adaptive Dependable Embedded Systems
2 LIG - Laboratoire d'Informatique de Grenoble

We demonstrate the feasibility of a complete workflow to synthesize and implement correct-by-construction fault tolerant distributed embedded systems consisting of real-time periodic tasks. Correct-by-construction is provided by the use of discrete controller synthesis (DCS), a formal method thanks to which we are able to guarantee that the synthesized controlled system guarantees the functionality of its tasks even in the presence of processor failures. For this step, our workflow uses the Heptagon domain specific language and the Sigali DCS tool. The correct implementation of the resulting distributed system is a challenge, all the more since the controller itself must be tolerant to the processor failures. We achieve this step thanks to the libDGALS real-time library (1) to generate the glue code that will migrate the tasks upon processor failures, maintaining their internal state through migration, and (2) to make the synthesized controller itself fault-tolerant.

Domaines: Langage de programmation [cs.PL]

Wei-Tsun Sun, Alain Girault, Gwenaël Delaval. A formal approach for the synthesis and implementation of fault-tolerant industrial embedded systems. SIES'2015: 10th IEEE International Symposium on Industrial Embedded Systems, Jun 2015, Siegen, Germany. ⟨hal-01165686⟩