Формирование контрпримера при верификации алгоритмов с помощью методов логического вывода

Предлагается модификация метода логического вывода делением дизъюнктов на основе определяющего элемента. Метод является одной из базовых составляющих программного комплекса для формальной верификации параллельных алгоритмов с помощью техники проверки моделей и математического аппарата теории логического вывода. Рассматриваемая модификация позволяет не только определять наличие или отсутствие ошибки в объекте анализа, но и, в случае ее обнаружения, восстанавливать цепочку событий, приводящих к возникновению некорректной ситуации. Полученная информация облегчает процесс локализации ошибки и способствует ее эффективному устранению. Вводится также понятие схемы процесса логического вывода применительно к решению задачи формальной верификации и предлагается набор графических примитивов для ее описания.