FORMATION OF THE REVERSE EXAMPLE AT VERIFICATION OF THE ALGORITHMS USING THE METHODS OF LOGICAL INFERENCE
Authors:
1.
Vyatka State University
Type:
Article
Pages:
from 50
to 57
Status:
Published
Received:
05.07.2014
Accepted:
25.07.2014
Published:
25.07.2014
Subject area:
VAC 05.12.2013 Системы, сети и устройства телекоммуникаций
VAC 05.13.01 Системный анализ, управление и обработка информации (по отраслям)
VAC 05.13.06 Автоматизация и управление технологическими процессами и производствами (по отраслям)
VAC 05.13.10 Управление в социальных и экономических системах
VAC 05.13.18 Математическое моделирование, численные методы и комплексы программ
VAC 05.13.19 Методы и системы защиты информации, информационная безопасность
UDK 004.052.42
GRNTI 20.01 Общие вопросы информатики
GRNTI 28.01 Общие вопросы кибернетики
GRNTI 49.01 Общие вопросы связи
GRNTI 50.01 Общие вопросы автоматики и вычислительной техники
GRNTI 82.01 Общие вопросы организации и управления
VAC 05.13.01 Системный анализ, управление и обработка информации (по отраслям)
VAC 05.13.06 Автоматизация и управление технологическими процессами и производствами (по отраслям)
VAC 05.13.10 Управление в социальных и экономических системах
VAC 05.13.18 Математическое моделирование, численные методы и комплексы программ
VAC 05.13.19 Методы и системы защиты информации, информационная безопасность
UDK 004.052.42
GRNTI 20.01 Общие вопросы информатики
GRNTI 28.01 Общие вопросы кибернетики
GRNTI 49.01 Общие вопросы связи
GRNTI 50.01 Общие вопросы автоматики и вычислительной техники
GRNTI 82.01 Общие вопросы организации и управления
Language:
Russian
Keywords:
formal verification, logical inference, clause division, inference process scheme
Abstract (English):
This paper proposes a modification of the inference method by clause division based on the defining element. The method is one of the basic components of the software complex for parallel algorithms formal verification using the technique of model checking and mathematical apparatus of the theory of inference. The considered modification can not only detect the presence or absence of an error in the object of the analysis, but also, in case of error detection, restore the course of events leading to the occurrence of abnormal situation. The obtained information facilitates the process of error localization and contributes to its effective elimination. The study also introduces the concept of inference process scheme in relation to the problem of formal verification and proposes a set of graphic primitives for its description.
This paper proposes a modification of the inference method by clause division based on the defining element. The method is one of the basic components of the software complex for parallel algorithms formal verification using the technique of model checking and mathematical apparatus of the theory of inference. The considered modification can not only detect the presence or absence of an error in the object of the analysis, but also, in case of error detection, restore the course of events leading to the occurrence of abnormal situation. The obtained information facilitates the process of error localization and contributes to its effective elimination. The study also introduces the concept of inference process scheme in relation to the problem of formal verification and proposes a set of graphic primitives for its description.
Keywords:
formal verification, logical inference, clause division, inference process scheme
formal verification, logical inference, clause division, inference process scheme
Введение Одной из наиболее важных проблем современной информатики является проблема проверки корректности (верификации) программного обеспечения. Ошибка в программном обеспечении, не обнаруженная на этапе разработки, способна привести к самым непредсказуемым и нежелательным последствиям. Примеры подобных ситуаций представлены в [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. Karpov Yu. G. Model Checking. Verifikaciya parallel'nyh i raspredelennyh programmnyh sistem / Yu. G. Karpov. SPb.: BHV-Peterburg, 2009. 552 s.
2. Baier C. Principles of Model Checking / S. Baier, J.-P. Katoen. Cambridge: The MIT Press, 2008. 994 p.
3. Kulyamin V. V. Metody verifikacii programmnogo obespecheniya / V. V. Kulyamin. Vseros. konkurs. otbor obzor.-analit. statey po prioritetnomu napravleniyu «Informacionno-telekommunikacionnye sistemy», 2008. 117 s. // URL: http://window.edu.ru/window/library?p_rid=56168.
4. Mel'cov V. Yu. Formal'naya verifikaciya parallel'nyh algoritmov s pomosch'yu tehniki proverki modeley i metodov logicheskogo vyvoda / V. Yu. Mel'cov, G. A. Chistyakov / Vyat. gos. un-t. Kirov, 2013. 140 s. Dep. v VINITI RAN 10.12.2013, № 358-V2013.
5. Mel'cov V. Yu. Formirovanie bazy znaniy na osnove struktury Kripke i formul temporal'noy logiki / V. Yu. Mel'cov, G. A. Chistyakov. Fundamental'nye issledovaniya. 2013. № 8, ch. 4. S. 847-852.
6. Strabykin D. A. Logicheskiy vyvod v sistemah obrabotki znaniy / D. A. Strabykin. SPb.: Izd-vo SPbGETU, 1998. 164 s.
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.
