A probabilistic model for estimation of software robustness to short-term hardware failures

The paper shows the possibility of using a two-dimensional Markov model defined on direct product of state spaces of two finite-state machines (FSM), one of which is a program finite automaton model that is running under normal conditions and the other one is the same FSM in which at some point in time, there was a short-term failure (e. g., within the time of a single operation or one machine cycle), for estimation of software robustness to short-term hardware failures. Previously, this model was proposed for probabilistic verification of hardware systems. The robustness of a program is estimated by probability of the faulty FSM return on the path of transitions of the source machine after termination of the failure. At the same time, the authors assume that a change in the FSM transitions trajectory in a low-level (instruction-by-instruction) program model will be significant only if it corresponds to some corruption in the branching of said block-diagram. The model is analyzed in detail by the example of the block-diagram of a specific program.