A framework for early stage quality-fault tolerance analysis of embedded control systems

This work presents a static-analysis based method for analyzing the robustness of a given embedded control system design, in the presence of quality-faults in sensors, software components, and inter-connections. The method characterizes the individual components of the system by storing the relations between the precision of inputs and the precision of outputs in what we call, lookup tables (LUTs). A network of LUTs thus formed which represent the given control system is converted into a satisfiability modulo theory (SMT) instance, such that a satisfying assignment corresponds to a potential counterexample (the set of quality-faults which violate the given fault-tolerance requirements) or hot-spot in the design. Hot-spots obtained in this manner are counter-verified through simulation to filter the false-positives. Experimental results on the fault-tolerant fuel controller from Simulink automotive library demonstrate the efficacy of the proposed approach.