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

Please wait, while we are loading the content...

Keynote talk I: Security and privacy in implantable medical devices: An ongoing concern

An abstraction-refinement framework for priority-driven scheduling of static dataflow graphs

Unified dataflow model for the analysis of data and pipeline parallelism, and buffer sizing

A new synthesis procedure for atomic rules containing multi-cycle function blocks

From clock-driven to data-driven models

Optimized distribution of synchronous programs via a polychronous model

Three-valued asynchronous distributed runtime verification

A multi-core version of FreeRTOS verified for datarace and deadlock freedom

A framework for high-assurance quasi-synchronous systems

Structure-aware CNF obfuscation for privacy-preserving SAT solving

Performance analysis of the Disrupted Static Priority scheduling for AFDX

Are interface theories equivalent to contract theories?

TESL: A language for reconciling heterogeneous execution traces

An architecturally-integrated, systems-based hazard analysis for medical applications

Refinement-based synthesis of correct contract model decompositions

Keynote talk IIP: Proving (and revisiting) what programs do not

Assertion-based flow monitoring of SystemC models

Formal property verification in a conformance testing framework

From visual to logical formalisms for SoC validation

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

MEMOCODE 2014 software design contest: Space Invaders emulator

Cycle-accurate 8080 emulation using an ARM11 processor with dynamic binary translation

A fast emulator for ARM-based embedded systems

Profiling and optimizations for embedded systems

MEMOCODE 2014 design contest: k-Nearest Neighbors with Mahalanobis distance metric

A high performance systolic architecture for k-NN classification

Cost-efficient implementation of k-NN algorithm on multi-core processors

Building faithful high-level models and performance evaluation of manycore embedded systems

Symbolic inner loop parallelisation for massively parallel processor arrays

Keynote talk III: A framework for modeling architectures and their properties

Tutorial I: Efficient symbolic execution for software testing

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

Content Provider	ACM Digital Library
Abstract	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.
Starting Page	175
Ending Page	184
Page Count	10
File Format	PDF
ISBN	9781479953387
DOI	10.1109/MEMCOD.2014.6961856
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-10-01
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

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

SEU Mitigation and Validation of the LEON3 Soft Processor Using Triple Modular Redundancy for Space Processing

Scheduling Considerations for Voter Checking in FPGA-based TMR Systems

Probabilistic model checking of perturbed MDPs with applications to cloud computing

Reliability analysis in component-based development via probabilistic model checking

Improving fpga design robustness with partial tmr.

Effectiveness of internal vs. external SEU scrubbing mitigation strategies in a Xilinx FPGA: Design, test, and analysis

Probabilistic model checking for energy analysis in software product lines

Implementation of Symbolic Model Checking for Probabilistic Systems (2002)

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

Similar Documents

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

SEU Mitigation and Validation of the LEON3 Soft Processor Using Triple Modular Redundancy for Space Processing

Scheduling Considerations for Voter Checking in FPGA-based TMR Systems

Probabilistic model checking of perturbed MDPs with applications to cloud computing

Reliability analysis in component-based development via probabilistic model checking

Improving fpga design robustness with partial tmr.

Effectiveness of internal vs. external SEU scrubbing mitigation strategies in a Xilinx FPGA: Design, test, and analysis

Probabilistic model checking for energy analysis in software product lines

Implementation of Symbolic Model Checking for Probabilistic Systems (2002)

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