Login | Register

Early Dependability Analysis of FPGA-Based Space Applications Using Formal Verification


Early Dependability Analysis of FPGA-Based Space Applications Using Formal Verification

Hoque, Khaza Anuarul (2016) Early Dependability Analysis of FPGA-Based Space Applications Using Formal Verification. PhD thesis, Concordia University.

[thumbnail of Hoque_PhD_S2016.pdf]
Text (application/pdf)
Hoque_PhD_S2016.pdf - Accepted Version


SRAM-based FPGAs are increasingly attractive in the aerospace industry for their field programmability and low cost. Unfortunately, they suffer from cosmic radiation induced Single Event Effects (SEEs). In safety-critical applications, the dependability of the design is a prime concern since failures may have catastrophic consequences. Hence, an early analysis of dependability of such safety-critical applications will enable designers to develop systems that meet high dependability requirements, such as the DO-254 standard. In this thesis, we propose a high-level dependability and performability analysis methodology based on probabilistic model checking. Compared to the pen-and-pencil and discrete-event simulation approach, our methodology is more accurate due to the use of an automated formal verification technique. Moreover, compared to fault injection or beam testing, analysis at early design stages can guide designers to build more reliable designs reducing the overall cost and effort. The proposed methodology can perform three different types of analysis: evaluation of available design options, optimization of scrub intervals while satisfying its design assurance level requirements, and optimal partitioning of Triple-Modular Redundant (TMR) Systems. Such analysis can also guide designers to adopt proper mitigation technique(s), such as rescheduling, TMR, TMR with less frequent scrubs, or even can help to decide the number of TMR partitions for a given scrub intervals.

Starting from a high-level description of a system, based on the preferred analysis, a Markov model or Markov (reward) model is constructed from the extracted Control Data Flow Graph (CDFG) and the failure/mitigation parameters for the targeted FPGA. Such modeling and exhaustive analysis elaborated using a probabilistic model checking technique can capture all the failures and repairs possible (according to some general model) in the system within the radiation environment. To illustrate the applicability of the proposed approach, we present our quantitative analysis obtained from DSP benchmark circuits.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Hoque, Khaza Anuarul
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:3 February 2016
Thesis Supervisor(s):Ait Mohamed, Otmane and Savaria, Yvon
Keywords:Formal verification, Dependability, Reliability, Markov Chain, FPGA, Probabilistic analysis, DO-254, Design Optimization
ID Code:981023
Deposited On:16 Jun 2016 15:45
Last Modified:18 Jan 2018 17:52
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top