Probabilistic model checking based DAL analysis to optimize a combined TMR-blind-scrubbing mitigation technique for FPGA-based aerospace applications

SRAM-based FPGAs are increasingly popular in the aerospace industry for their field programmability and low cost. However, they suffer from cosmic radiation induced Single Event Upsets (SEUs), commonly known as soft errors. In safety-critical applications, the dependability of the design is a prime concern since failures may have catastrophic consequences. An early analysis of dependability of such safety-critical applications will enable designers to develop a design that meets the high availability and reliability requirements of the DO-254 standard. This paper introduces a novel methodology based on probabilistic model checking, to analyze the dependability properties of safety-critical systems and to suggest required mitigation techniques, such as Triple Modular Redundancy (TMR) or TMR with less frequent scrubs for early design decisions. Starting from a high-level description of a system, a Markov model is constructed from the Control Data Flow Graph (CDFG) expressing the functionality and from failure/mitigation parameters for the targeted FPGAs. Such an exhaustive model captures all the failures and repairs possible in the system within the radiation environment. We present a case study on a benchmark circuit to illustrate the applicability of the proposed approach to demonstrate that a wide range of useful dependability properties can be analyzed using our proposed methodology.