ФОРМИРОВАНИЕ КОНТРПРИМЕРА ПРИ ВЕРИФИКАЦИИ АЛГОРИТМОВ С ПОМОЩЬЮ МЕТОДОВ ЛОГИЧЕСКОГО ВЫВОДА

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

• Чистяков Г.А.

• Общий отдел

• Технические науки. Промышленность
• Физико-математические науки
• Социальные (общественные) науки