Lineage-driven fault injection

Lineage

核心观点：fault-tolerance is redundancy

从一个正确的结果出发，反推为了这个正确的结果有哪些可能的情况。比如A和B都是保证C成功执行的冗余，所以C的正确执行依赖于A或者B。

上面的方式直接解不了，因为状态空间是\(2^E\)的（E是相关的组件）。

采用以下的方法：算出使每条路径失效的条件，然后如果要让整个都失效，就把每条路径失效的条件and起来，用布尔表达式计算。

\(\and\)(\(\or\)每条路径上的元素)

一个容错程序在出现部件故障和消息丢失等故障时，应该试图通过其他方式实现其预期结果。因此，上述公式的解并不一定表明是一个错误，而是一个必须通过故障注入来测试的假设。通过注入与布尔公式的解相对应的一组故障，故障注入框架将产生两种结果之一。

系统不能产生预期的结果，表明有一个容错错误。执行终止，用户会看到一个可视化的脉络图。
系统成功地产生了预期的结果。这表明它已经揭示了获得该结果的替代策略。这次执行的线代图应该与当前的线代图合并，并提取和解决一个新的公式。就这样，LDFI在具体执行和符号求解之间交替进行。

后面是介绍故障的框架的了。