Skip to Main content Skip to Navigation
Journal articles

Automating the Addition of Fault Tolerance with Discrete Controller Synthesis

Alain Girault 1 Eric Rutten 2, * 
* Corresponding author
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 SARDES - System architecture for reflective distributed computing environments
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Discrete controller synthesis (DCS) is a formal approach, based on the same state-space exploration algorithms as model-checking. Its interest lies in the ability to obtain automatically systems satisfying by construction formal properties specified a priori. In this paper, our aim is to demonstrate the feasibility of this approach for fault tolerance. We start with a fault intolerant program, modeled as the synchronous parallel composition of finite labeled transition systems; we specify formally a fault hypothesis; we state some fault tolerance requirements; and we use DCS to obtain automatically a program, having the same behavior as the initial fault intolerant one in the absence of faults, and satisfying the fault tolerance requirements under the fault hypothesis. Our original contribution resides in the demonstration that DCS can be elegantly used to design fault tolerant systems, with guarantees on key properties of the obtained system, such as the fault tolerance level, the satisfaction of quantitative constraints, and so on. We show with numerous examples taken from case studies that our method can address different kinds of failures (crash, value, or Byzantine) affecting different kinds of hardware components (processors, communication links, actuators, or sensors). Besides, we show that our method also offers an optimality criterion very useful to synthesize fault tolerant systems compliant to the constraints of embedded systems, like power consumption.
Document type :
Journal articles
Complete list of metadata

Cited literature [54 references]  Display  Hide  Download
Contributor : Alain Girault Connect in order to contact the contributor
Submitted on : Monday, November 5, 2012 - 6:39:14 PM
Last modification on : Wednesday, July 6, 2022 - 4:15:43 AM
Long-term archiving on: : Wednesday, February 6, 2013 - 3:56:41 AM


Files produced by the author(s)




Alain Girault, Eric Rutten. Automating the Addition of Fault Tolerance with Discrete Controller Synthesis. Formal Methods in System Design, Springer Verlag, 2009, 35, pp.190--225. ⟨10.1007/s10703-009-0084-y⟩. ⟨hal-00748687⟩



Record views


Files downloads