Вероятностные модели оценки устойчивости программ к кратковременным аппаратным сбоям

Показана возможность использования двумерной марковской модели поведения конечного автомата при сбое на одном такте, предложенной ранее для вероятностной верификации аппаратных систем, для оценки устойчивости программ, представленных блок-схемами реализуемых алгоритмов, к кратковременным сбоям. Модель представляет собой произведение цепей Маркова (ЦМ), соответствующих конечно-автоматной модели программы, работающей в нормальных условиях, и автомата, в котором в некоторый момент времени произошел кратковременный (например, в пределах времени выполнения одной операции или одного машинного цикла) сбой. Устойчивость к сбоям оценивается вероятностью возвращения автомата после прекращения действия помехи на траекторию переходов исходного автомата. При этом считается, что изменения траектории при сбое в низкоуровневой (instruction-by-instruction) модели программы будут существенными только в том случае, если они соответствуют изменению ветвления в указанной блок-схеме. Модель подробно анализируется на примере конкретной блок-схемы программы.