Symplified: Symbolic program-level fault injection and error detection framework

TitleSymplified: Symbolic program-level fault injection and error detection framework
Publication TypeConference Paper
Year of Publication2008
AuthorsPattabiraman, K., N. Nakka, Z. Kalbarczyk, and R. Iyer
Conference NameDependable Systems and Networks With FTCS and DCC, 2008. DSN 2008. IEEE International Conference on
Pagination472 -481
Date Publishedjun.
Keywordsarbitrary error detectors, error detection, error detection framework, fault diagnosis, hard-to-detect corner cases, model checking, program verification, program-level framework, random fault-injection, symbolic execution, symbolic program-level fault injection, SymPLFIED, transient hardware errors

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 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 corner cases caused by transient errors in programs that may not be exposed by random fault-injection based validation.


a place of mind, The University of British Columbia

Electrical and Computer Engineering
2332 Main Mall
Vancouver, BC Canada V6T 1Z4
Tel +1.604.822.2872
Fax +1.604.822.5949

Emergency Procedures | Accessibility | Contact UBC | © Copyright 2021 The University of British Columbia