This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework
Nov. 2013 (vol. 62 no. 11)
pp. 2292-2307
Karthik Pattabiraman, University of British Columbia, Vancouver
Nithin M. Nakka, Nexstest Systems, San Jose
Zbigniew T. Kalbarczyk, University of Illinois at Urbana-Champaign, Urbana
Ravishankar K. Iyer, University of Illinois at Urbana-Champaign, Urbana
This paper introduces SymPLFIED, a program-level framework that allows specification of arbitrary error detectors and the verification of their efficacy against hardware errors. SymPLFIED comprehensively enumerates all transient hardware errors in registers, memory, and computation (expressed symbolically as value errors) that potentially evade detection and cause program failure. The framework uses symbolic execution to abstract the state of erroneous values in the program and model checking to comprehensively find all errors that evade detection. We demonstrate the use of SymPLFIED on a widely deployed aircraft collision avoidance application, tcas. Our results show that the SymPLFIED framework can be used to uncover hard-to-detect catastrophic cases caused by transient errors in programs that may not be exposed by random fault injection-based validation. Further, the errors exposed by the framework help us formulate a set of error detectors for the application to avoid the catastrophic case and other incorrect outcomes.
Index Terms:
Registers,Detectors,Hardware,Assembly,Computational modeling,Transient analysis,error detection,Fault injection,model checking
Citation:
Karthik Pattabiraman, Nithin M. Nakka, Zbigniew T. Kalbarczyk, Ravishankar K. Iyer, "SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework," IEEE Transactions on Computers, vol. 62, no. 11, pp. 2292-2307, Nov. 2013, doi:10.1109/TC.2012.219
Usage of this product signifies your acceptance of the Terms of Use.