Компьютерное обеспечение и вычислительная техника УДК 004.052.42 Г. А. Чистяков ФОРМИРОВАНИЕ КОНТРПРИМЕРА ПРИ ВЕРИФИКАЦИИ АЛГОРИТМОВ С ПОМОЩЬЮ МЕТОДОВ ЛОГИЧЕСКОГО ВЫВОДА Предлагается модификация метода логического вывода делением дизъюнктов на основе определяющего элемента. <...> Метод является одной из базовых составляющих программного комплекса для формальной верификации параллельных алгоритмов с помощью техники проверки моделей и математического аппарата теории логического вывода. <...> Рассматриваемая модификация позволяет не только определять наличие или отсутствие ошибки в объекте анализа, но и, в случае ее обнаружения, восстанавливать цепочку событий, приводящих к возникновению некорректной ситуации. <...> Вводится также понятие схемы процесса логического вывода применительно к решению задачи формальной верификации и предлагается набор графических примитивов для ее описания. <...> Ключевые слова: формальная верификация, логический вывод, деление дизъюнктов, схема процесса логического вывода. <...> Обзор основных формальных методов верификации содержится в [3]. <...> Метод логического вывода делением дизъюнктов на основе определяющего элемента В [4] предлагается метод формальной верификации параллельных алгоритмов на основе ной базы знаний KB D i KB |}, элементами которой являются секвенции, состоящие из { , 1. | i 50 техники проверки моделей и математического аппарата теории логического вывода. <...> Рассматриваемый там же метод логического вывода делением дизъюнктов на основе определяющего элемента (МЛВДДОЭ) в логике предикатов первого порядка хорошо зарекомендовал себя при анализе программ и алгоритмов, модели которых не могут быть эффективно верифицированы символьными средствами. <...> Литералами являются предикатные константы определенного вида, возможно с символом отрицания. <...> Элементы KB f определяют свойства модели объекта анализа, а элементы KB r – требования, предъявляемые к объекту. <...> KB r имеют вид 2,P2 D D| |,1 i | |,D <...>