ФОРМИРОВАНИЕ КОНТРПРИМЕРА ПРИ ВЕРИФИКАЦИИ АЛГОРИТМОВ С ПОМОЩЬЮ МЕТОДОВ ЛОГИЧЕСКОГО ВЫВОДА
Авторы:
1.
Вятский государственный университет
Тип:
Статья
Страницы:
с 50
по 57
Статус:
Опубликован
Получено:
05.07.2014
Одобрено:
25.07.2014
Опубликовано:
25.07.2014
Классификаторы:
ВАК 05.12.2013 Системы, сети и устройства телекоммуникаций
ВАК 05.13.01 Системный анализ, управление и обработка информации (по отраслям)
ВАК 05.13.06 Автоматизация и управление технологическими процессами и производствами (по отраслям)
ВАК 05.13.10 Управление в социальных и экономических системах
ВАК 05.13.18 Математическое моделирование, численные методы и комплексы программ
ВАК 05.13.19 Методы и системы защиты информации, информационная безопасность
УДК 004.052.42
ГРНТИ 20.01 Общие вопросы информатики
ГРНТИ 28.01 Общие вопросы кибернетики
ГРНТИ 49.01 Общие вопросы связи
ГРНТИ 50.01 Общие вопросы автоматики и вычислительной техники
ГРНТИ 82.01 Общие вопросы организации и управления
ВАК 05.13.01 Системный анализ, управление и обработка информации (по отраслям)
ВАК 05.13.06 Автоматизация и управление технологическими процессами и производствами (по отраслям)
ВАК 05.13.10 Управление в социальных и экономических системах
ВАК 05.13.18 Математическое моделирование, численные методы и комплексы программ
ВАК 05.13.19 Методы и системы защиты информации, информационная безопасность
УДК 004.052.42
ГРНТИ 20.01 Общие вопросы информатики
ГРНТИ 28.01 Общие вопросы кибернетики
ГРНТИ 49.01 Общие вопросы связи
ГРНТИ 50.01 Общие вопросы автоматики и вычислительной техники
ГРНТИ 82.01 Общие вопросы организации и управления
Язык материала:
русский
Ключевые слова:
формальная верификация, логический вывод, деление дизъюнктов, схема процесса логического вывода
Аннотация (русский):
Предлагается модификация метода логического вывода делением дизъюнктов на основе определяющего элемента. Метод является одной из базовых составляющих программного комплекса для формальной верификации параллельных алгоритмов с помощью техники проверки моделей и математического аппарата теории логического вывода. Рассматриваемая модификация позволяет не только определять наличие или отсутствие ошибки в объекте анализа, но и, в случае ее обнаружения, восстанавливать цепочку событий, приводящих к возникновению некорректной ситуации. Полученная информация облегчает процесс локализации ошибки и способствует ее эффективному устранению. Вводится также понятие схемы процесса логического вывода применительно к решению задачи формальной верификации и предлагается набор графических примитивов для ее описания.
Предлагается модификация метода логического вывода делением дизъюнктов на основе определяющего элемента. Метод является одной из базовых составляющих программного комплекса для формальной верификации параллельных алгоритмов с помощью техники проверки моделей и математического аппарата теории логического вывода. Рассматриваемая модификация позволяет не только определять наличие или отсутствие ошибки в объекте анализа, но и, в случае ее обнаружения, восстанавливать цепочку событий, приводящих к возникновению некорректной ситуации. Полученная информация облегчает процесс локализации ошибки и способствует ее эффективному устранению. Вводится также понятие схемы процесса логического вывода применительно к решению задачи формальной верификации и предлагается набор графических примитивов для ее описания.
Ключевые слова:
формальная верификация, логический вывод, деление дизъюнктов, схема процесса логического вывода
формальная верификация, логический вывод, деление дизъюнктов, схема процесса логического вывода
Введение Одной из наиболее важных проблем современной информатики является проблема проверки корректности (верификации) программного обеспечения. Ошибка в программном обеспечении, не обнаруженная на этапе разработки, способна привести к самым непредсказуемым и нежелательным последствиям. Примеры подобных ситуаций представлены в [1, 2]. В течение двух последних десятилетий активно развивался формальный подход к верификации [3]. Этот аппарат, в отличие от привычного тестирования или экспертиз различного рода, позволяет дать однозначный ответ на вопрос о корректности объекта проверки (программы или алгоритма). Такие результаты обеспечиваются благодаря применению строгих математических техник, суть которых состоит в анализе модели, эквивалентной исследуемому объекту и отражающей свойства, значимые с точки зрения его дальнейшей эксплуатации, на предмет соответствия заданной спецификации. Обзор основных формальных методов верификации содержится в [3]. Основным недостатком формального подхода, препятствующим его повсеместному применению и полному отказу от тестирования, является отсутствие универсальных методов, способных эффективно верифицировать программы и алгоритмы различной структуры. Как правило, каждый из известных методов хорошо показывает себя при проверке объектов только ограниченного числа классов. Например, символьные методы способны проверять программы и алгоритмы, модели которых насчитывают 10100-10200 состояний. Однако в ряде ситуаций сложность таких методов начинает возрастать экспоненциально, что приводит к нецелесообразности их применения вследствие высоких накладных расходов [3]. Таким образом, в настоящее время, в поисках путей устранения этого недостатка, формальный подход к верификации продолжает развиваться в направлении появления новых, эффективных для широкого спектра случаев, методов проверки корректности программ и алгоритмов. Метод логического вывода делением дизъюнктов на основе определяющего элемента В [4] предлагается метод формальной верификации параллельных алгоритмов на основе техники проверки моделей и математического аппарата теории логического вывода. Рассматриваемый там же метод логического вывода делением дизъюнктов на основе определяющего элемента (МЛВДДОЭ) в логике предикатов первого порядка хорошо зарекомендовал себя при анализе программ и алгоритмов, модели которых не могут быть эффективно верифицированы символьными средствами. Задача, решаемая МЛВДДОЭ, может быть поставлена следующим образом. Для известной базы знаний , элементами которой являются секвенции, состоящие из литералов, требуется определить, выводима ли цель , представленная однолитеральной секвенцией. Литералами являются предикатные константы определенного вида, возможно с символом отрицания. При этом база знаний может быть описана как , , где - множество фактов (однолитеральных секвенций), а - множество утверждений. Элементы определяют свойства модели объекта анализа, а элементы - требования, предъявляемые к объекту. Секвенции множества имеют вид . В [5] показано, каким образом классическая задача верификации с использованием техники проверки моделей может быть сведена к задаче логического вывода в форме, подходящей для решения с помощью МЛВДДОЭ. Суть МЛВДДОЭ заключается в последовательном применении операции деления дизъюнктов и порождении вспомогательных целей до тех пор, пока не будет доказана истинность или ложность первоначально выводимой секвенции. Кроме того, в ряде ситуаций используется операция разбиения дизъюнкта, заключающаяся в разделении текущей цели на несколько, с инверсией некоторых из них. Данная операция позволяет обеспечить полноту метода относительно задачи верификации. Формальное описание метода с доказательством его корректности изложено в [4]. Полезными могут оказаться также работы [6, 7], содержащие описание обобщенного метода логического вывода делением дизъюнктов. МЛВДДОЭ может быть рассмотрен как группа взаимосвязанных процедур: шаг логического вывода (процедура вывода), деление дизъюнкта, полное образование остатков и ограниченное образование остатков. Взаимодействие между этими процедурами представлено на рис. 1. Рис. 1. Взаимодействие между процедурами МЛВДДОЭ Основным недостатком верификации с использованием МЛВДДОЭ в базовом варианте является отсутствие возможности локализации ошибки в случае ее обнаружения. Задача получения этих сведений может быть решена путем модификации МЛВДДОЭ таким образом, чтобы вместе с формированием результата верификации выполнялось также построение схемы процесса вывода, отражающей цепочку событий, приводящих к некорректной ситуации. В терминах техники проверки моделей данная схема будет представлять собой контрпример - последовательность состояний модели, поочередное пребывание в которых приводит к нарушению спецификации. Локализация ошибки может быть выполнена путем анализа предметных констант, содержащихся в выводимых дизъюнктах. Формирование схемы процесса логического вывода Определим схему процесса логического вывода как ориентированное направленное дерево , состоящее из множества взвешенных вершин и множества взвешенных дуг. Вершины графа соответствуют шагам вывода, а дуги отражают связи между шагами. Каждой вершине графа сопоставляется следующая информация: - множество номеров секвенций базы знаний, при делении на которые были получены какие-либо непустые остатки; - промежуточный признак завершения вывода, полученный в результате выполнения данного шага; - уникальный числовой идентификатор, используемый для ссылки на конкретный шаг. Каждой дуге графа, соединяющей вершины с числовыми идентификаторами и , сопоставляется следующая информация: - выводимый дизъюнкт, являющийся целью для шага ; - признак инверсии, показывающий, является ли выводимая на шаге цель результатом, полученным в ходе выполнения операции разбиения дизъюнкта инверсным литералом; - окончательный признак завершения вывода, принимающий значение «0» (вывод завершен успешно) или «1» (вывод завершен неудачно) и передаваемый с шага на шаг для вынесения заключения о выводимости цели шага . Таким образом, произвольная вершина графа может быть представлена как кортеж , где - множество номеров секвенций - делимых, давших непустые остатки; - промежуточный признак завершения вывода; - уникальный идентификатор шага вывода. Произвольная дуга представляет собой кортеж , где и - идентификаторы инцидентных вершин (дуга направлена от к ); - целевой дизъюнкт для шага ; - признак инверсии; - окончательный признак завершения вывода. Указанной информации оказывается достаточно для восстановления хода процесса логического вывода. Для возможности формирования графа требуется модифицировать МЛВДДОЭ и в ходе выполнения процедур метода осуществлять следующие дополнительные действия. 1. Перед выполнением процедуры вывода для первоначальной цели требуется инициализировать пустое множество вершин и множество дуг , состоящее из единственного элемента с , и . Кроме того, следует обнулить счетчик идентификаторов . 2. В начале выполнения процедуры вывода для некоторого дизъюнкта (позиция (1) на рис. 1) следует увеличить значение счетчика идентификаторов , добавить к множеству вершин графа новый элемент , задав для него и , и установить значение элемента входящей в вершину дуги в . 3. После завершения процедуры деления дизъюнктов (позиция (2) на рис. 1) следует проанализировать полученные результаты и установить признак окончания вывода вершины в одно из четырех возможных значений . Кроме того, если , необходимо поместить в множество соответствующей вершины номера тех секвенций базы знаний, при деление которых на текущую цель были получены непустые остатки. 4. В ходе порождения новых выводимых целей (позиция (3) на рис. 1) необходимо добавить к множеству дуг требуемое количество элементов. При этом для каждой добавляемой дуги : - в следует занести идентификатор соответствующей вершины ; - признак необходимо установить в «1», если цель шага, для которого данная дуга будет являться входной, представляет собой инверсию литерала, полученного в ходе выполнения операции разбиения дизъюнкта, и в «0» в противном случае; - в следует занести порожденную вспомогательную цель. 5. После вынесения заключения о выводимости некоторого дизъюнкта (позиция (4) на рис. 1) следует установить окончательный признак завершения вывода входной для соответствующей вершины дуги в одно из двух возможных значений . Для визуализации и последующего анализа графа предлагается воспользоваться специальными графическими примитивами. Примеры использования этих примитивов изображены на рис. 2. Рис. 2. Примеры использования графических примитивов для изображения схемы процесса логического вывода Шаг вывода изображается в виде окружности, разделенной горизонтальной чертой на две половины. В верхней части вершины (над горизонтальной чертой) перечисляются номера секвенций базы знаний, при делении на которые были получены какие-либо непустые остатки (множество ). Нижняя часть вершины (под горизонтальной чертой) содержит информацию о значении промежуточного признака завершения вывода, полученного в результате выполнения данного шага (признак ). В левой верхней области символа указывается уникальный идентификатор шага (). Выражение, расположенное рядом с входящей дугой, соответствует целевому дизъюнкту , выводимость которого устанавливается на данном шаге. Выражения, расположенные рядом с выходящими дугами, определяют новые выводимые дизъюнкты (вспомогательные цели), полученные в ходе выполнения шага. Обратная стрелка с символом «0» или «1», находящаяся рядом с каждой дугой, соответствует окончательному признаку завершения вывода. Пунктирная дуга показывает ситуацию анализа выводимости однолитеральной секвенции, полученной в результате выполнения операции разбиения дизъюнкта (признак инверсии ). Для сокращения размера схемы предлагается использовать два специальных примитива - символ шага со штриховкой и двойную выходную дугу. Символ шага со штриховкой означает, что результат данного шага не влияет на процесс вывода. В таком случае обратная стрелка с возвращаемым значением опускается. Данный символ может быть применен в тех ситуациях, когда результат шага не сказывается на выносимом в родительской вершине заключении вследствие получения решения в параллельной ветви вывода. Двойная выходная дуга означает, что полученная вспомогательная цель имеет существенное значение в контексте решаемой задачи, однако процесс ее вывода по каким-либо причинам не представлен на схеме. Пример схемы процесса логического вывода Рассмотрим схему процесса логического вывода на примере. Пусть требуется верифицировать алгоритм, модель которого описывается следующими секвенциями (фактами). 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. Здесь предикатная константа означает, что в модели алгоритма существует переход из состояния в состояние ; - из состояния не существует ни одного перехода; - в состоянии происходит событие . Предикаты, предваренные символом инверсии, имеют прямо противоположное значение. Кроме того, база знаний содержит следующие утверждения, отражающие предъявляемые к объекту верификации требования. 17. 18. 19. 20. 21. 22. 23. 24. Целью вывода является доказательство истинности выражения . Схема процесса вывода, полученная в результате применения модифицированного МЛВДДОЭ, представлена на рис. 3. Первый шаг вывода завершен с промежуточным признаком , т. к. исходная цель не может быть выведена из имеющихся утверждений. В результате применения операции разбиения дизъюнкта задача была преобразована к задаче проверки истинности отрицания цели. Второй шаг привел к получению остатка , что свело решаемую задачу к независимой проверке выводимости утверждений и . При этом анализ истинности первого из них был произведен через проверку выводимости инверсии единственного литерала. В процессе вывода утверждения на третьем шаге была получена новая секвенция . Далее дизъюнкт был разделен на два выражения и . Из-за получения отрицательного результата в ходе вывода обработка вспомогательной цели не потребовалась, и дизъюнкт был исключен из рассмотрения. Рис. 3. Схема процесса логического вывода На девятом шаге вывода были сформированы два множества остатков - и . В соответствии с алгоритмом выполнения процедуры деления дизъюнктов [4], единственный остаток множества был исключен на основании того, что в базе знаний имеется факт . В результате построения конъюнкции остатков из множества были получены два новых утверждения, вывод которых, ввиду получения признаков для вспомогательных целей (шаг не представлен на схеме) и (шаг 17), завершился с положительным результатом. Восьмой шаг вывода завершился с отрицательным результатом. Таким образом, вывод первоначального утверждения завершен успешно. Результатом верификации будет заключение о выводимости исходной посылки и, следовательно, несоответствии модели анализируемого алгоритма сформулированной спецификации. Анализ схемы процесса логического вывода позволяет локализовать ошибку. Положительный результат обусловлен получением на восьмом шаге окончательного признака , которое объясняется успешным выводом обеих вспомогательных целей на шаге девять. Те, в свою очередь, были выведены через на шагах 11 и 17, на шаге 14 и неотраженный на схеме успешный вывод () вспомогательной цели . Таким образом, доказано, что одной из некорректных ситуаций будет являться, например, нарушение моделью требования в состоянии (шаг 17), переход в которое возможен с помощью перемещений через состояния и . Заключение Представленная в работе модификация метода логического вывода делением дизъюнктов на основе определяющего элемента позволяет не только отвечать на вопрос о соответствии модели объекта верификации сформулированным требованиям, но и выполнять построение схемы процесса логического вывода. Данная схема, в случае нарушения моделью спецификации, может быть использована для эффективной локализации места ошибки и ее последующего устранения. Модифицированный метод нашел применение в прототипе программного комплекса для верификации параллельных алгоритмов DDVerifier.
1. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем / Ю. Г. Карпов. СПб.: БХВ-Петербург, 2009. 552 с.
2. Baier C. Principles of Model Checking / С. Baier, J.-P. Katoen. Cambridge: The MIT Press, 2008. 994 p.
3. Кулямин В. В. Методы верификации программного обеспечения / В. В. Кулямин. Всерос. конкурс. отбор обзор.-аналит. статей по приоритетному направлению «Информационно-телекоммуникационные системы», 2008. 117 с. // URL: http://window.edu.ru/window/library?p_rid=56168.
4. Мельцов В. Ю. Формальная верификация параллельных алгоритмов с помощью техники проверки моделей и методов логического вывода / В. Ю. Мельцов, Г. А. Чистяков / Вят. гос. ун-т. Киров, 2013. 140 с. Деп. в ВИНИТИ РАН 10.12.2013, № 358-В2013.
5. Мельцов В. Ю. Формирование базы знаний на основе структуры Крипке и формул темпоральной логики / В. Ю. Мельцов, Г. А. Чистяков. Фундаментальные исследования. 2013. № 8, ч. 4. С. 847-852.
6. Страбыкин Д. А. Логический вывод в системах обработки знаний / Д. А. Страбыкин. СПб.: Изд-во СПбГЭТУ, 1998. 164 с.
7. Strabykin D. A. Logical method for predicting situation development based on abductive inference / D. A. Strabykin // Journal of Computer and Systems Sciences International. 2013. Vol. 52, iss. 5. P. 759-763.
