SymPLFIED: Symbolic program-level fault injection and error detection framework
SymPLFIED: Symbolic program-level fault injection and error detection framework
复制标题
SymPLFIED：符号程序级故障注入和错误检测框架
DOI：
10.1109/dsn.2008.4630118
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
R. Iyer
中科院分区：
文献类型：
--
作者：
K. Pattabiraman;Nithin Nakka;Z. Kalbarczyk;R. Iyer
本文介绍了SymPLFIED，这是一个程序级框架，允许指定任意错误检测器并验证其对硬件错误的有效性。SymPLFIED全面列举寄存器、内存和计算中所有可能逃避检测并导致程序失败的瞬时硬件错误(表示为值错误)。该框架使用符号执行来抽象程序中错误值的状态，并使用模型检测来全面地发现所有逃避检测的错误。我们演示了在广泛部署的飞机防撞应用程序TCAS上使用SymPLFIED。我们的结果表明，SymPLFIED框架可以用来发现由于程序中的瞬时错误而导致的难以检测的角落情况，这些情况可能不会被基于随机错误注入的验证所暴露。
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.