автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Алгоритмы вычисления отношений подобия в задачах верификации и реструктуризации программ

004616956

Московский государственный университет имени М.В. Ломоносова Факультет вычислительной математики и кибернетики

На правах рукописи

Булычёв Пётр Евгеньевич

АЛГОРИТМЫ ВЫЧИСЛЕНИЯ ОТНОШЕНИЙ ПОДОБИЯ ЗАДАЧАХ ВЕРИФИКАЦИИ И РЕСТРУКТУРИЗАЦИИ ПРОГРАММ

Специальность 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации па соискание ученой степени кандидата физико-математических наук

- 9 ДЕК 2010

МОСКВА 2010

004616956

Работа выполнена на кафедре автоматизации систем вычислительных комплексов факультета вычислительной математики и кибернетики Московского государственного университета имени М.В. Ломоносова.

Научные руководители: доктор физико-математических наук,

профессор, академик РАЕН Смелянский Руслан Леонидович; кандидат физико-математических наук, доцент Захаров Владимир Анатольевич.

Официальные оппоненты: доктор физико-математических наук,

профессор Ломазова Ирина Александровна;

кандидат физико-математических наук, Ромапенко Сергей Анатольевич.

Ведущая организация: Вычислительный центр им. А. А. Дородницына

РАН.

Защита состоится «10» декабря 2010 г. в 11:00 на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В. Ломоносова по адресу: 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-ой учебный корпус, факультет вычислительной математики и кибернетики, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ имени М.В. Ломоносова, с текстом автореферата — на официальном сайте ВМиК МГУ имени М.В. Ломоносова: http://www.cs.msu.su в разделе «Наука» — «Работа диссертационных советов» — «Д 501.001.44».

Автореферат разослан « $ » ноября 2010 г.

Ученый секретарь

диссертационного совета Д 501.001.44 профессор

Н.П. Трифонов

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Введение.

Отношения подобия и различные их проявления играют большую роль как в математике, естествознании, так и в обыденной практике.

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

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

Во второй части рассмотрен особый вид отношений подобия — симуляции, часто возникающие в задачах верификации программ. Отношение симуляции ^ — это бинарное отношение, заданное на множестве моделей вычисления (автоматов, сетей Петри, программ). Справедливость Л ^ В означает то, что структура дерева вычислений модели В оказывается сходной структуре дерева вычислений модели А. Как следствие, многие отношения симуляции сохраняют выполнимость спецификаций, заданных формулами темпоральных логик. Благодаря этому качеству отношения симуляции часто используются в методах формальной верификации программ, позволяя сводить проверку корректности программ к анализу их абстрактных моделей, сохраняющих исследуемые свойства программ. В данной работе рассматривается задача проверки отношений симуляции для случая, когда модели программ задаются структурами Крипке и временными автоматами.

Актуальность задачи поиска клонов. Клопом называются фрагменты, имеющие незначительные синтаксические отличия друг от друга. Суще-

ствует ряд факторов, приводящих к появлению клонов, и наиболее распространённой причиной является использование операции "копирование и вставка" (сору&ра81е). Результаты многочисленных статистических исследований свидетельствуют о том, что суммарный объём клонов в больших проектах обычно составляет 7-20%.

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

Существуют и другие применения детекторов клонов. Например, они могут использоваться для выделения библиотек часто используемых функций. Найденные клоны могут использоваться для нахождения шаблонов использования классов, и таким образом, для добавления новых методов в эти классы. При добавлении новой функции можно проверять с помощью детектора клопов, не существует ли уже функции, которая имеет ту же функциональность. Относительное количество кода, покрытого клонами, может использоваться в качестве одной из метрик качества кода. Ещё одной областью применимости детекторов клонов является выявление случаев нарушения авторских прав.

Актуальность задачи проверки симуляции между моделями программ. Одним из наиболее распространенных методов проверки правильности программ является верификация моделей программ. В этом методе прове-

ряется не сама программа, а её модель, которая, с одной стороны, сохраняет исследуемые свойства программы, а с другой стороны, является достаточно простой для автоматического анализа.

Важным этапом метода является построение моделей программы. Модели могут отражать поведение программы с разной степенью подробности, они могут строиться как вручную, так и автоматически. Чрезмерно упрощённая модель может давать слишком грубое приближение реальной программы, и па ней не будут проявляться те свойства вычислений, которые присущи программе. С другой стороны, при верификации чрезмерно подробных моделей приходится преодолевать эффект "комбинаторного взрыва": анализ модели становится практически неосуществим из-за слишком большого числа возможных состояний.

Поэтому для применения метода верификации моделей удобно иметь средство, позволяющее сравнивать структуру модели со структурой исходной программы, а также сравнивать структуру моделей между собой. Данное средство в своей работе может опираться на отношения симуляции, т. е. бинарные отношения, заданные на множестве моделей вычисления и сохраняющие структуру их деревьев вычислений. Замечательной особенностью отношений симуляции является то, что они сохраняют выполнимость спецификаций, заданных формулами темпоральных логик. Поэтому для того, чтобы проверить, что все формулы некоторой темпоральной логики, выполнимые на модели Л, выполняются и на другой модели (или программе) В, достаточно проверить выполнимость подходящего отношения симуляции ^ между А и В (т. е. проверить выполнимость А В).

Отношения симуляции также используются для вычисления инвариантов бесконечных параметризованных семейств моделей, для нахождения симметрии в моделях, для автоматического уменьшения размеров моделей, для проверки свойств конфиденциальности многопоточных программ.

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

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

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

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

Цель работы. Цель диссертационной работы — разработка математических методов и алгоритмов проверки различных отношений подобия, которые возникают в анализе и преобразовании программ. В частности, для решения задачи реструктуризации программ необходимо разработать и реализовать алгоритм обнаружения клонов, совместимых с существующими методами ре-факторинга. Для решения задачи верификации программ дискретного времени необходимо разработать платформу, которая могла бы быть использована для проверки целого ряда отношений симуляции между структурами Крипке. Для решения задачи верификации программ реального времени необходимо разработать подходящее отношение симуляции, сохраняющее выполнимость темпоральных спецификаций на временных игровых автоматах, и алгоритм проверки этого отношения.

Методы исследования. При получении основных результатов работы диссертации использовались методы математической логики, теории графов, теории автоматов и теории формальных языков.

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

определено отношение симуляции, сохраняющее выполнимость формул логики ATCTL на множестве временных игровых автоматов; приведён алгоритм проверки выполнимости данного отношения.

Практическая ценность. Разработанное средство обнаружения клопов может использоваться разработчиками программного обеспечения в процессе реструктуризации программ. Разработанное средство проверки симуляций между структурами Крипке может служить дополнением к средству верификации моделей NuSMV. Разработанное средство проверки симуляций между временными автоматами было использовано в задаче синтеза контроллера для системы автоматического управления реального времени.

Апробация работы. Результаты, представленные в работе, докладывались на научном семинаре лаборатории вычислительных комплексов кафедры АСВК факультета ВМиК МГУ имени М.В. Ломоносова под руководством профессора P.JT. Смелянекого; на семинаре кафедры АСВК под руководством заведующего кафедрой член-корр. РАН JI.H. Королева; на научном семинаре "Теоретические проблемы программирования" под руководством профессора Р.И. Подловченко и доцента В.А. Захарова; на научном семинаре "Дискрет-пая математика и математическая кибернетика" под руководством профессора В.Б. Алексеева, профессора A.A. Сапоженко и профессора С.А. Ложкина; на рабочих совещаниях группы проекта INTAS 05-1000008-8144 «Practical Formal Verification Using Automated Reasoning and Model Checking», а также на следующих конференциях:

• Международная конференция «Дискретные модели в теории управляющих систем» (Москва, март 2006 г.);

• Всероссийская научная конференция студентов, аспирантов и молодых учёных «Технологии Microsoft в теории и практике программирования», секция «Теоретическое программирование» (Москва, апрель 2008 г.);

• Весенний коллоквиум молодых ученых в области программной инженерии (SYRCoSE) (Санкт-Петербург, май 2008 г.);

• Научно-техническая общеевропейская конференция «ЕвроПайтон» (EuroPython) (Литва, Вильнюс, июль 2008 г.);

• Международный научный семинар «Программные клоны» (Workshop on Software Clones) (Германия, Кайзерслаутерн, март 2009 г.);

• Международная конференция памяти академика А. П. Ершова «Перспективы систем информатики» (Новосибирск, июнь 2009 г.);

• Международный научный семинар «Теория игр в приложениях к проектированию и верификации» (Workshop on Games for Design and Verification) (Италия, Удине, сентябрь 2009 г.);

• Международная конференция «Формальное моделирование и анализ временных систем» (Conference on Formal Modelling and Analysis of Timed Systems) (Венгрия, Будапешт, сентябрь 2009 г.);

• Всероссийская конференция «Методы и средства обработки информации» (Москва, октябрь 2009 г.);

• Международная научная конференция студентов, аспирантов и молодых учёных «Ломоносов» (Москва, апрель 2010 г.).

Работа была выполнена при поддержке грантов INTAS и РФФИ.

Публикации. По теме диссертации имеется 10 публикаций (включая 2 в изданиях из перечня ВАК), список которых приводится в конце автореферата.

Структура и объем диссертации. Диссертация состоит из введения, трёх глав, заключения, списка литературы и приложения. Объём работы —

169 страниц (включая 2 страницы приложения). Список литературы содержит 122 наименований.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

Работа состоит из введения, трёх глав и заключения.

Во введении обоснована актуальность диссертационной работы и сформулирована цель исследований.

В первой главе решается задача разработки математической модели программных клонов, совместимой с существующими методами рефакторин-га, и разработки алгоритма поиска клонов, удовлетворяющих этой модели.

В разделе 1.1 рассмотрены операции рефакторинга, при помощи которых можно избавиться от клонов, а именно: "Выделение метода" (процедурная абстракция, Extract Method), "Подъём метода" (Pull Up Method) и "Выделение родительского класса" (Extract Superclass). Для применения этих операций в общем случае необходимо, чтобы фрагменты, составляющие клон, являлись линейными последовательностями операторов (последовательности могут состоять из одного элемента, а операторы могут быть составными). Кроме того, наиболее простыми для рефакторинга являются клопы, один фрагмент которых может быть получен из другого фрагмента путём замены одних подвыражений на другие подвыражения. Для выделения операторов и их подвыражений необходимо провести синтаксический разбор программы, т. е. построить её абстрактное синтаксическое дерево (АСД). Произвольное подвыражение некоторого оператора программы соответствует некоторому поддереву АСД этой программы.

Отсюда мы приходим к следующему определению:

Определение 1.1 (Клон кода). Две последовательности операторов Е\ и Е2 формируют (р1,р2)-клон, если абстрактное синтаксическое дерево после-

10

довательности Е\ можно получить из абстрактного синтаксического дерева последовательности Е? путём замены некоторых поддеревьев на другие поддеревья, и справедливы неравенства min(|£/i|, l^l) > í>i и p(Ei, Ег) < рг-

В качестве функций размера | • | и расстояния р используются следующие две функции. Размером |Т| дерева Т считается равным количеству всех его листьев, а размером оператора — размер его АСД. Размер оператора, определённый таким образом, инвариантен относительно способа построения АСД, поскольку он равен количеству вхождений всех имён и констант в фрагмент кода. Если АСД оператора Е\ получается из АСД оператора Е2 заменой поддерева T\¿ на Т2Д, Ti.2 на Тг,2 . • • Ti.n на Т2,,,, то будем считать расстояние p(Ei,E2) равным значению + 1^2.¡I) — п- Показано, что функция

р является семи-метрикой.

В разделе 1.2 представлен обзор средств автоматического обнаружения клонов. На основании обзора делается вывод о том, что ни одно из существующих средств не позволяет находить клоны, удовлетворяющие определению 1.1. Однако два средства находят клоны, похожие на те, которые удовлетворяют этому определению. Это средство Asta1, разработанное в Microsoft Research, и средство CloneDR.2, разработанное компанией Semantic Designs. Asta находит клоны, которые могут отличаться в произвольных подвыражениях, но сами фрагменты, составляющие клон, являются отдельными операторами. CloneDR находит клоны, состоящие из последовательностей операторов, однако эти фрагменты могут отличаться только в именах функций и переменных и значениях констант.

Таким образом, определение 1.1 не рассматривалось ранее в литературе

1 Evans W. S., Eraser С. W., Ma F. Clone detection via structural abstraction // Reverse Engineering,

2007.

2 Clone detection using abstract syntax trees / I. D. Baxter, A. Yahin, L. Moura et al. // Proceedings of the International Conference on Software Maintenance, 1998.

и, вместе с тем, оно является обобщением существующих определений.

В разделе 1.3 вводится ряд определений, которые будут использованы при описании разработанного алгоритма обнаружения клонов. Шаблоном называется дерево, в котором часть листьев помечена специальными метками-заполнителями. Дерево Т называется примером шаблона 17, если Т получается из II заменой всех меток-заполнителей на некоторые поддеревья. Наиболее специальный шаблон (НСШ) двух деревьев Т\ и Т2 — это такой шаблон максимального размера, что и Т\, и Тг являются его примерами.

В разделе 1.4 приводится алгоритм поиска клонов, удовлетворяющих определению 1.1. Этот алгоритм состоит из трёх процедур.

На первом этапе все операторы разбиваются на группы похожих операторов (кластеры). Используется простой однопроходный алгоритм кластеризации. Каждый новый оператор сравнивается с существующими кластерами; в зависимости от результата сравнения он либо добавляется в подходящий кластер, либо формирует новый. В целях эффективности каждый новый оператор сравнивается не со всеми операторами некоторого кластера, а только с их общим НСШ. По окончании первого этапа все операторы будут помечены номерами кластеров, которым они принадлежат.

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

На последнем этапе все выявленные одинаково помеченные последовательности операторов сравниваются попарно для окончательного выделения клопов.

Разработанный алгоритм является эвристическим, т. е. в некоторых слу-

чаях он может находить не все клоны, удовлетворяющие определению 1.1. Поэтому в разделе 1-4-4 приведено и доказано достаточное условие полноты алгоритма, т. е. способ получения по заданной программе таких параметров алгоритма, что при их использовании описанный алгоритм найдёт все клоны, удовлетворяющие определению 1.1.

В разделе 1.5 проводится теоретическое сравнение возможностей разработанного и существующих алгоритмов.

В разделе 1.6 описывается реализация разработанного алгоритма в программно-инструментальном средстве Clone Digger. Это средство распространяется под лицензией GNU General Public License (GPL) и может быть загружено с сайта http://clonedigger.sourceforge.net. Clone Digger написано на языке Python и поэтому является кроссплатформенным. В качестве языков программирования, на которых могут быть написаны анализируемые программы, в настоящее время поддерживаются Python версий 2.Х, Java 1.5, Javascript, Lúa. Найденные клопы записываются в HTML-отчёт в двухколо-ночном формате с подсветкой отличий.

В разделе 1.7 приводятся результаты двух экспериментов, в которых разработанное средство Clone Digger сравнивалось с другими существующими средствами обнаружения клонов.

В первом эксперименте проводилось сравнение с средством CloneDR; как было указано в обзоре, это средство находит клоны, похожие на те, что находит разработаное средство Clone Digger. Было проверено, что все клоны, которые были выданы пробной версией CloneDR, могут быть обнаружены Clone Digger при некоторых значениях параметров-порогов. Кроме того, доказано, что некоторые клоны, найденные Clone Digger, не могут быть найдены CloneDR в принципе (при произвольных значениях порогов).

Во втором эксперименте проводилось сравнение с средствами Dup и CloneDR. Методика данного эксперимента является общепринятой при срав-

90 80 70

, , . 53

49 ,/ .;

Clone Digger

40 Clone DR

30 .I'M... - - Dup

20 " . ; B ^ . 18 .....И " '

10 ■ ■ ■ í\>~'Á .i-ríj

. я.. : . . Ú'A '^Ж

Булычёв Коваленко Шалимов Усреднённый

Рис. 1.1. Сравнение полноты обнаружения клонов

нении средств обнаружения клопов3.

В начале эксперимента был построен объединённый список из всех 31500 клонов, найденных хотя бы одним из трёх средств в проекте Eclipse JDT Core. Затем 2% от этих клопов были классифицированы каждым из трёх экспертов (аспирантов JIBK ВМиК МГУ), и было сформировано три эталонных множества, в которые попали только те клопы, от которых, по мнению эксперта, можно избавиться при помощи рефакторинга. Четвёртое эталонное множество было автоматически построено методом голосования.

Для каждого эталонного множества Е и каждого рассматриваемого средства t были вычислены две характеристики: полнота (recall) и точность (precision) обнаружения клопов. Полнота — это процент от числа клопов из эталонного множества Е, которые были обнаружены средством t. Точность — это процент от числа клопов, обнаруженных средством Í, которые попали в множество Е.

Полученные результаты представлены на диаграммах 1.1 и 1.2. Видно, что разработанное средство Clone Digger превосходит два других средства Dup и CloneDR как по точности, так и по полноте поиска клонов.

Во второй главе решается задача создания универсальной среды про-

3 Bellon S., Koschke R., Antoniol G., Krinke J., Merlo E.. Comparison and Evaluation of Clone Detection Tools // IEEE Transactions on Software Engineering, 200714

Clone Digger

CloneDR

Dup

Рис. 1.2. Сравнение точности обнаружения клонов

верки симуляций между моделями программ, заданными конечными структурами Крипке.

Определение 2.1. Структура Крипке задаётся пятёркой (5, ¿о, Л, Ь}, где 5 — конечное множество состояний, «о 6 5 — начальное состояние, И С 5 х Б — отношение переходов, £ — множество атомарных переменных, Ь : Б —>• 2е — функция разметки состояний.

Для задания спецификаций поведения программ наиболее часто используется темпоральная логика ветвящегося времени СТЬ* и её фрагменты ЬТЬ, АСТЬ*, СТЬ*Х и АСТЬ*Х. Эти логики имеют различные выразительные способности и области применения. Так, СТЬ* и АСТЬ* позволяют описывает свойства деревьев вычислений, а ЬТЬ — свойства отдельных вычислений. В логиках СТЬ*Х, АСТЬ*Х и ЬТЬх отсутствует оператор X. Данный оператор используется для задания свойств, которые должны выполняться в следующем состоянии вычисления. Поэтому оп не применяется для описания свойств параллельных асинхронных систем, поскольку порядок выполнения процессов в таких системах недетерменировап.

Будем говорить, что бинарное отношение ^ на множестве структур Крипке сохраняет выполнимость формул логики Л, если для любой формулы <р € А и любых структур Крипке М\ и Мг таких, что М\ М^, из М2 |= (р

15

100 ю 90 80 70

во

50 40

30 22

20 10

Булычёв

m

Шалимов Усреднённый

следует М\ (= <р.

Отношения симуляции — это специальная разновидность бинарных отношений на множестве моделей программ; говоря неформально, модель М2 симулирует модель М\, если дерево вычислений, порождённое моделью М\, подобно некоторому фрагменту дерева вычислений, порождённому моделью М2. Определяя по-разному подобие деревьев вычислений, можно получить большое разнообразие отношений симуляции (строгую симуляцию, прореженную симуляцию,...). Наибольший интерес представляют отношения симуляции, сохраняющие выполнимость формул различных темпоральных логик.

В разделе 2.1.3 даны определения строгой и прореженной симуляций (которые в дальнейшем будут использоваться в качестве сквозного примера) и вкратце описаны несколько других симуляций.

Определение 2.2 (Строгая симуляция). Пусть даны две структуры Крипке М\ и М2, где М,- = йг'о, Яп £,-, Ь^, г = 1,2, и £1 = Ег. Будем говорить, что между Мх и М2 выполняется строгая симуляция (обозначается М\ -< М2), если существует такое Я С 5х х 5г, что (вю,в2о) £ Я и для любой пары («1,52) 6 Я выполняется:

1. ¿1(51) = Ь2(з2) и

2. если (.91,.^) € то существует такое состояние в'2 € £2, что (зг,^) € Й2 И (я'ц 4) € Я.

Будем говорить, что между М\ и М2 выполняется строгая бисимуляция, если в определении 2.2 отношение Я является симметричным (т. е. Я = Я-1).

Определение прореженной симуляции отличается от определения строгой симуляции тем, что каждому переходу (э1, э^) € Я1 может соответствовать последовательность переходов (п > 0) в /?2, такая, что ¿о = й2, 6 Я и для всех I < п выполняется (£¿,£¿+1) Я2 и (^1, € Я.

Если добавить к этому определению требование симметричности, то мы придём к определению прореженной бисимуляции.

Строгая симуляция сохраняет выполнимость формул ACTL*, строгая биеимуляция — выполнимость формул CTL*, прореженная симуляция — выполнимость формул ACTL*X, прореженная биеимуляция — выполнимость формул CTL*X.

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

На основании обзора, проведённого в разделе 2.2, был сделан вывод о том, что в основу универсального средства описания и проверки симуляций целесообразно положить теоретико-игровой подход. Этот подход годится для проверки всех известных отношений симуляции, и более того, во многих случаях его использование даёт оптимальные по сложности алгоритмы проверки симуляций.

В теоретико-игровом подходе задача проверки симуляции сводится к задаче нахождения выигрышной стратегии в антагонистической игре двух игроков Spoiler и Duplicator (или для краткости S и D).

Формально такая игра задаётся пятёркой (Vs, Vd, Es, Ed, i'o), где Vs и Vd — множества состояний игроков Spoiler и Duplicator соответственно, Es С VsX-Vd и Ed С Vd x Vs — множества допустимых ходов, vq £ V5 — начальное состояние. История игры — это такая конечная или бесконечная последовательность игровых состояний (эд, i>i, t'2, • • •), что (г>;, t',+i) 6 E$\JEd для любого г > 0. Стратегией игрока Duplicator — это функция W : Vd —> Vs U {halt}.

История игры (vo,Vi,V2,...) удовлетворяет стратегии W игрока Duplicator, если для любого состояния v-t Е Vb из истории игры, за исключением, возможно, последнего, выполняется г>;+1 = W(vi), а для последнего состояния (если история игры конечна) выполняется W(vj) = halt. Игрок Duplicator выигрывает в игре, если у пего существует стратегия, для которой любая удовлетворяющая ей история игры либо является бесконечной, либо завершается состоянием игрока Spoiler. Игры проверки симуляции проектируются таким образом, что выполнимость отношения симуляции равносильна существованию выигрышной стратегии игрока Duplicator в соответствующей игре проверки симуляции.

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

Самый простой вид имеет определение правил игры проверки строгой симуляции. Предположим, что необходимо проверить симуляцию между Mi и Мг, где М; = {Si, s,-o, Ri, Lt). Состояния игроков Spoiler и Duplicator в этой игре представляются кортежами, состоящими из одного состояния из Si и одного состояния из S2, т. е. Vs — Vd = {(si, S2)lsi 6 Si As2 G S2)}. Если состояния игрока P описывается парой значений типизированных переменных Хр и х'р (хгР принимает значения из Si), то допустимые переходы игроков

описываются формулами

</5S(4,4,xk,4,) = (4 = x2d) Л i?i(4,4)

<pd(X]},X2d, 4,4) = (4 = Л л2(4,4) л (М4) = ¿2(4,))

Поэтому множества ходов будут иметь следующий вид: Es = {((s1,s2),(s'i,s2))|(si,si) £ Ri} и = {({sus2))(si,s'2))\(sus'2) e /?2 Л ¿(si) = Х(б'2)}- Начальное игровое состояние полагается равным но — (S10,S20)-

Всего на разработанном языке были записаны правила проверки следующий отношений: строгой симуляции и бисимуляции, прореженной симуляции и бисимуляции, слабой симуляции (сохраняющей выполнимость формул LTLx), к2 симуляции (сохраняющей выполнимость формул LTL). В диссертационной работе доказана корректность игр для проверки прореженной симуляции и бисимуляции, корректность игр для проверки остальных симуляций была доказана ранее в литературе.

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

В разделе 2.5 описывается разработанное универсальное программно-инструментальное средство проверки симуляций между парами структур Крип-ке. Данное средство реализовано па языке Python. В качестве языка задания

моделей используется язык широко используемого верификатора NuSMV1. Для представления формул в символьном алгоритме были использованы упорядоченные двоичные разрешающие диаграммы (OBDD). В равной мере для символьного представления моделей и игры могут быть использованы и другие математические конструкции: регулярные выражения, прямое формульное представление и др. OBDD были выбраны ввиду широкой распространённости библиотек для манипуляции с ними. В дайной диссертационной работе в качестве библиотеки работы с OBDD используется библиотека Cudd.

В разделе 2.6 приводится пример применения средства проверки симуляции при инкрементальном построении моделей программ. В инкрементальном методе последовательно строятся модели Mi,..., Мп так, что каждая следующая модель является уточнением предыдущей модели и содержит больше подробностей о конструируемой программе. Такой способ построения помогает избежать ошибок при построении моделей. Чтобы убедиться, что Mj+i уточняет Mi, достаточно проверить, что между этими моделями выполняется некоторое отношение симуляции (которое выбирается исходя из характера отличий между Mj+i и М;). Если же это отношение симуляции не выполняется, то контрпример, выданный средством проверки симуляций, поможет найти ошибку в модели М,;+\.

В диссертационной работе инкрементальный подход был применён для решения задачи справедливого разделения ресурсов в системе асинхронных взаимодействующих процессов (задача "обедающих философов"). Всего были построены 3 модели. В модели М\ не накладывалось никаких ограничений на действия процессов (философов). В модели Мг появляется маркер; каждый философ может получить маркер только когда вилки слева и справа от него лежат па столе. После того, как философ получил маркер, он может взять вилки и начать есть; после того как он закончил есть, он освобожда-

4 NuSMV model checker: http://nusmv.irst.itc.it

ет маркер. В окончательной модели М3 маркер движется строго по кругу, и каждый философ обязан закончить есть прежде, чем оп передаст маркер своему соседу.

Исходя из характера отличий между моделями был сделан вывод о том, что между М2 и М\ должно выполнятся отношение строгой симуляции, а между Мз и Л/2 — отношение прореженной симуляции. Справедливость этих отношений была проверена при помощи разработанного средства для систем с различным количеством обедающих философов.

В третьей главе решается задача разработки алгоритма проверки симуляции между временными игровыми автоматами.

В разделе 3.1 даются вводные определения. Будем использовать запись В(Х) для обозначения множества формул над множеством X, удовлетворяющих грамматике ц> v.— х ~ к \ (рЛр, где к £ Z>o, х £ X и ~ е {<, <,=,>, >}. Будем использовать запись XY для обозначения множества всех отображений из множества X в множество Y (это расходится с традиционной записью Yx). Оценка переменных из X — это элемент R>0. Пусть 5 £ К>о, тогда будем обозначать v + 5 такую оценку, что для всех х £ X выполняется (г> + 5)(ж) = u(:e) + <5. Пусть Y С X, тогда будем использовать запись v[Y] для обозначения оценки, сопоставляющей 0 всем х £ Y, и v(x) всем х £ X \ Y.

Определение 3.1. Временной автомат (timed automata, ТА) — это шестёрка (5, s0, X, £, R, Inv), где S — конечное множество дискретных состояни-яй, So £ S — начальное дискретное состояние, X — конечное множество вещественных переменных (таймеров), £ — множество пометок переходов (действий), включающее в себя так называемое невидимое действие г, R С S х В(Х) х £ х р(Х) х S — конечное множество переходов (р(Х) — множество всех подмножеств X), Inv : S —>• В{Х) — функция, сопоставляющая дискретным состояниям формулы (такие формулы называются инвариантами).

Семантика временного автомата определяется размеченной системой переходов (Q,<7o,->), где Q = S х Ж>0, go = (so, 0)- Из состояния qi существует дискретный переход по действию а в состояние q2 (обозначается q\ A q-z), если существует такой переход е = (s,g,a,Y,s') € R, что v\= g,v' = v[Y] и v' [= Inv(s'). Из состояния qi = (s,v) существует задержка по времени 6 в состояние qi = (s, v') (обозначается qi qi), если v' = v + 5 и v' |= Inv(s).

Для простоты будем полагать, что временные автоматы детерменирова-ны по действиям, т. е. для любой пары q € Q и а 6 £ существует не более одного такого q', что q A q'. Временной игровой автомат (timed game automata, TGA) — это временной автомат, в котором множество действий £ разбито на множество контролируемых (Ес) и множество неконтролируемых (£") переходов. Стратегия с нулевой памятью контроллера (соответственно, среды) — это функция /, определённая на множестве состояний Q, и возвращающая некоторый элемент множества (R>o х 72е) (соответственно, (М>о х 72")).

Определение 3.5. Пусть дан TGA (S, ¿0, 72, X, R, Inv), и пусть (6е, а,0) и (5й, аи) — некоторые стратегии контроллера и среды соответственно. Вычис-

5о an Si а 1 ^

ление до -> <72 —> Яз Qi —i> 9s • • • будем называть порожденным этими стратегиями, если для любого г G N выполняется 5,: = min(5c(g2/), ¿"(?2i)) и:

[ а»Ы если 5u(q2i) < 6'-(q2i) <4 = <

[ ас(Я2г) иначе

Аналогично определяются понятие стратегии для педетерменированных по действиям временных игровых автоматов, в этом случае стратегия будет возвращать не пометки, а переходы.

В разделе 3.1.4 определяется логика ATCTL, используемая для описания свойств временных игровых автоматов. Эта логика состоит из формул вида AaiUtfTo и AaiWta2, где t 6 Z>о U {+оо}, а о\ и ст2 — некоторые множества видимых действий. Будем говорить, что вычисление 7Г временного

автомата М удовлетворяет формуле o\Ut<J2, если существует такой префикс этого вычисления 7г', что все видимые действия 7г' лежат в множестве о\, последнее действие п' лежит в а^ и длительность 7г' не превышает t. Вычисление 7г временного автомата М удовлетворяет формуле U\Wt<J2, если это вычисление удовлетворяет формуле a\Utао, или все видимые действия 7Г принадлежат множеству о\. Будем говорить, что формула Aip логики ATCTL выполняется на TGA М, если существует такая стратегия контроллера /с, что для любой стратегии среды /„, формула ц) выполняется на вычислении, порождённом стратегиями fc и /„.

Задача, которая решается в данной главе, заключается в определении отношения сохраняющего выполнимость формул логики ATCTL, и разработке алгоритма проверки этого отношения. В разделе 3.2 приводится обзор существующих кандидатов на роль такого отношения. На основании обзора сделан вывод о том, что в качестве искомого отношения следует использовать "комбинацию" определений временной, игровой и ослабленной отношений симуляции, описанных ранее в литературе.

В разделе 3.3 даётся предложенное автором определение симуляции:

Определение 3.7 (twa-симуляция). Пусть даны два TGA М\ и М2 с множествами состояний Q1 и Q'2: где Mi = (Si, Sio, Xt, Е,-, Ri, Invi). Будем говорить, что между Mi и М2 выполняется отношение слабой альтернирующей временной (timed weak alternating, twa) симуляции, если существует такое отношение Н С Qi х Q2, что пара начальных состояний (910,520) находится в этом отношении и для любой пары (qi, дг) £ Я и для любых q\ е Q\, q'2 € Q2, 5 G M>o, a E E \ {г} выполняются следующие требования:

1. если (<72 —>с <72)1 т0 существует такое п > 1 и такая последовательность состояний q'Ll, q'12l ■ ■ ■, q[.„ автомата М\, что q[д = <71, q'l n_г -2>с q[ 7l, (q[ n, q'2) € Н и при этом для всех г = 2..п — 1 выполняется (gj ■, 72) 6 Н

и 9'i.i-i ^С ч'и

2. если (gi Au gj), то существует такое п > 1 и такая последовательность состояний (?2,i,i2.21---.<?2,n автомата М2, что g^i = 92, -^u (<?i>92,n) 6 Я и при этом для всех г = 2..n— 1 выполняется q[ g'u

3. если g2 gi,, то (gi, gi,) G Я

4. если gj A,, gj, то (gi,g2) G Я

5. если g2 Л g.^, то существует такое g" G Qi, что gi A g" и (g", gi,) G Я

В теореме 3.1 доказано, что введённое отношение twa-симуляции сохраняет выполнимость формул логики ATCTL.

В разделе 3.4 приведён разработанный теоретико-игровой алгоритм проверки twa-симуляции и доказана его корректность. Поскольку в общем случае множество состояний временных автоматов бесконечно, то бесконечна и игра проверки симуляции. Поэтому в разработанном алгоритме ведётся работа не над отдельными игровыми состояниями, а над формулами, описывающими потенциально бесконечные множества состояний. Для операций над такими формулами используется аппарат матриц ограниченных разностей (difference bounded matrixes).

В разделе 3.5 описана реализация разработанного алгоритма в рамках среды анализа временных игровых автоматов UPPAAL Tiga.

В разделе 3.6 описано экспериментальное исследование реализации разработанного алгоритма twa-симуляции для решения задачи синтеза алгоритма алгоритма работы контроллера в системе автоматического управления. Рассмотрим следующий пример. Пусть имеется движущийся конвейер, на который ставится изделие. Затем изделие движется по конвейеру и последовательно проходит N этапов обработки, каждый этап занимает от 1 до 2 единиц времени. Задача контроллера — после завершения последнего этапа

pos <N-1.

X>1 Л

х<2 л Ready

- .__(¡«^l^ _ X22W2

\ , ~ ~х:=о" ~ ~ ~ pass n Jx< 2 next к.-о, —

pos" kick

Fail

kick

Win

x »2-N+2

pa"ss" "

Fail

Рис. 3.3. Временные автоматы, па которых проводилось экспериментальное исследование разработанного алгоритма

переместить готовое изделие с конвейера в коробку. Если этого не произойдёт в течение 2N + 2 единиц времени с начала работы конвейера, то изделие будет потеряно, и, таким образом, задача контроллера не будет выполнена. Данная система описывается TGA S, изображённом на рисунке 3.3 слева. Сплошными дугами обозначены контролируемые переходы, а прерывистыми — неконтролируемые.

Задача контроллера в автомате S — перевести автомат в дискретное состояние Win, т. е. обеспечить выполнимость формулы A{next}U{kick}. Одна из возможных выигрышных стратегий контроллера/с — подождать, пока автомат перейдёт в дискретное состояние Readxj, а затем выполнить переход в состояние Win. Предположим теперь, что в реальной ситуации контроллеру неизвестно текущее положение изделие на конвейере. Тогда стратегия /с не может использоваться в моделируемой (реальной) ситуации.

Поэтому была построена другая модель А, изображённая на рисунке 3.3 справа. Эта модель уже пе содержит невидимую контроллеру информацию, и для неё у контроллера существует выигрышная стратегия (её можно автоматически построить при помощи средства UPPAAL Tiga). Для того, чтобы проверить, что та же стратегия будет выигрышной и для исходной модели, достаточно проверить существование twa-симуляции между S и А. Коррект-

ность такого сведения была доказана в теореме 3.2. Существование twa-cимy-ляции между Б и А было проверено для нескольких значений N.

В приложении даются ииструкции по использованию разработанного средства обнаружения клонов и разработанного средства проверки симуляций между структурами Крипке.

Основные результаты работы.

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

2. Предложен формальный язык представления отношений симуляции между структурами Крипке, создан, реализован и испытан па практике универсальный (общий) алгоритм проверки симуляций, записанных на этом языке.

3. Дано определение отношения подобия между временными игровыми автоматами, сохраняющее выполнимость формул логики АТСТЬ. Разработан и испытан на практике алгоритм проверки этого отношения.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Булычев П.Е., Захаров В.А., Конпов И.В. Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов // Труды седьмой международной конференции "Дискретные модели в теории управляющих систем 2006.

2. Булычев П.Е., Булычёва О.Н., Захаров В.А. Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов с ограничениями справедливости. // Вестник МЭИ, т. 6, 2007. С. 5-9.

3. Bulychev Р.Е., Konnov I.V., Zakharov V.A. Computing (bi)siinulation relations preserving CTL*_X for ordinary and fair Kripke structures. // Сборник «Математические методы и алгоритмы», ИСПРАН. - 2007. - Том 12.

4. Bulychev P., Minea М. Duplicate code detection using anti-unification. Proceedings of the 1st Spring Young Researchers' Colloquium on Software Engineering SYRCoSE 2008, 2008. Pp. 51-54.

5. Bulychev P., Minea M. An evaluation of duplicate code detection using anti-unification. Proceedings of 3rd International Workshop on Software Clones, 2009, IESE-Report; 038.09/E. Pp. 22-27.

6. Bulychev P., Kostylev E., Zakharov V. Anti-unification algorithms and their applications in program analysis. Proceedings of Seventh International Andrei Ershov Memorial Conference, 2009, Lecture Notes in Computer Science vol. 5947, Pp. 413-423.

7. Bulychev P., Chatain Th., David A., Larsen K.G. Efficient on-the-fly algorithm for checking alternating timed simulation. Proceedings of Formal Modeling

and Analysis of Timed Systems, 2009, Lecture Notes in Computer Science vol. 5813. Pp. 73-87.

8. Булычев П.Е., Захаров В.А. О верификации конечных параметризованных моделей распределенных программ // Научные ведомости Белгородского государственного университета. — 2009. — JV«9. — С. 116-123.

9. Булычёв П.Е., Захаров В.А. Универсальный подход к проверке отношений симуляции моделей программ // Труды научной конференции Методы и Средства Обработки Информации. — 2009. С. 104-109.

10. Булычёв П.Е., Шалимов A.B., Коваленко Д.С. Экспериментальное сравнение средств обнаружения клонов // Труды молодёжной международной научной олимпиады "Ломоносов-2010". — 2010. С. 11-12.

Заказ № 25-а/11/10 Подписано в печать 02.11.2010 Тираж 80 экз. Усл. п.л. 1,3

¿■- ■СООО "Цифровичок", тел. (495) 649-83-30 ')) www.cfr.rti; е-таИ:irtfo@cfr.ru

Введение

1. Проблема обнаружения программных клонов.

2. Отношения симуляции между конечными автоматами (структурами Крипке).

3. Отношения симуляций между временными автоматами.

Глава 1. Обнаружение подобных фрагментов в исходных кодах программ.

1.1. Постановка задачи.

1.2. Обзор методов и средств автоматического обнаружения клонов

1.3. Основные определения.

1.4. Алгоритм поиска клонов.

1.5. Теоретическое сравнение возможностей разработанного и существующих алгоритмов.

1.6. Описание практической реализации.

1.7. Результаты экспериментальных исследований.

1.8. Область применимости.

Отношения подобия и различные их проявления играют большую роль как в математике, естествознании, так и в обыденной практике.

Словарь Даля определяет понятие подобия как схожесть, близость, принадлежность к одному виду, образу или обладание одинаковыми качествами. Похожее определение приводится и в других словарях: Ожегова, Оксфордском, Лопатникова и др.

Подобие лежит в основе аналогии, т. е. виде умозаключения, при котором знания, полученные в ходе рассмотрения какого-либо объекта А, переносятся на другой подобный ему объект В, менее изученный и в данный момент изучаемый. Помимо использования в аналогии отношения подобия обладают и другим полезным свойством: в некоторых случаях они позволяют не только установить, в чём схожи два объекта, но и понять, в чём они отличаются.

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

Отношения подобия позволяют вводить новые сущности, объединяя новые объекты в один класс. Таким образом возникают онтологии и появляется возможность описывать свойства не только отдельных объектов, но и свойства целых классов объектов.

В данной работе исследуется применение отношений подобия в задачах автоматического анализа программ. Среди методов анализа программ можно выделить методы, работающие с исходными текстами программ, и методы, в которых проверяются динамические свойства (поведение) программ. Мы будем рассматривать применение отношений подобия к анализу программ в обоих этих ракурсах. Таким образом, мы будем исследовать схожесть в устройстве программ (синтаксическое подобие) и схожесть их поведения (семантическое подобие).

Во-первых, мы рассмотрим проблему обнаружения синтаксически похожих фрагментов (клонов, дубликатов кода) в исходных кодах программ. Результаты статистических исследований, о которых говорится в работах [8, 11, 83], свидетельствуют о том, что суммарный объём клонов в больших проектах обычно составляет 7-20%, а в некоторых случаях доходит и до 59% [33]. Наличие большого числа клонов приводит к увеличению стоимости поддержки кода [73, 96], к возрастанию ресурсов, необходимых для компиляции и хранения скомпилированной программы [59, 93]. Кроме того, сознательное дублирование кода (т. е. использование операции copy&paste) приводит к увеличению вероятности возникновения новых и распространения существующих ошибок [26, 31, 60]. Поэтому от избыточного дублирования кода целесообразно избавляться при помощи существующих методов реорганизации (рефакторинга) кода, например, при помощи процедурной абстракции, также называемой "Выделением метода" (Extract Method) в терминологии Фаулера [121]. В данной работе ставится задача разработи и реализации алгоритма нахождения клонов, от которых легко можно избавиться при помощи таких методов рефакторинга.

Не менее важное практическое значение имеют и отношения семантического подобия, проявляющиеся в схожести функциональных свойств вычислительных систем. Во второй части рассмотрены симуляции — отношения подобия специального вида, возникающие в задачах верификации программ. Отношения симуляции — это бинарные отношения, заданные на множестве моделей вычисления (автоматов, сетей Петри, программ), которые проявляются в том, что структура дерева вычислений одной модели оказывается сходной структуре дерева вычислений другой модели. Интересны эти отношения тем, что они сохраняют выполнимость спецификаций, заданных формулами темпоральных логик, т. е. если модели А и. В находятся в отношении симуляции (обозначается В ^ ./1), то любая спецификация, выполнимая для А, выполняется и для В. Благодаря этому качеству отношения симуляции часто используются в методах формальной верификации программ, позволяя сводить проверку программ к анализу их абстрактных моделей, сохраняющих исследуемые свойства программ.

Начиная с основополагающей статьи Миллнера [74] отношения симуляции хорошо исследованы для случая, когда модели задаются структурами Крипке. По мере возникновения новых задач и методов верификации моделей программ появляются новые отношения. Библиография статей, посвященных отношениям симуляции, вероятно, обширна. Наиболее распространённые отношения симуляции и способы их проверки описаны в работах [15, 17, 35, 43, 47, 50, 54, 65, 89, 95, 105]. Более того, постоянно появляются новые отношения, поэтому существует необходимость в создании универсальной системы проверки симуляции, которая могла бы быть использована как единая платформа для проверки различных отношений, в зависимости от потребностей пользователя. С научной точки зрения разработка данного средства интересно тем, что оно позволит дать ответ на вопрос о том, можно ли сконструировать универсальный алгоритм проверки симуляций, не уступающий по эффективности существующим индивидуальным алгоритмам. С практической точки зрения это средство будет полезно тем, что оно может быть приспособлено к разным системам верификации и для проверки различных (в т. ч. новых) отношений симуляции. В данной работе ставится задача разработки такой системы.

Помимо конечных автоматов в верификации программ на моделях используются и более выразительные формализмы описания программ, в частности, временные автоматы [5]. По существу, временные автоматы — это конечные автоматы, снабжённые конечным множеством таймеров и ограничениями на значения таймеров, при которых допустимы те или иные переходы. Пока автомат находится в одном состоянии, значения всех таймеров растут с одинаковой скоростью, при переходе из состояния в состояние значения некоторых таймеров могут сбрасываться в 0. Временные автоматы могут использоваться в задаче синтеза контроллера (устройства управления). В этом случае автомат, фактически, описывает взаимодействие двух игроков: контроллера и среды. Сложность временных автоматов настолько велика, что практическое применение этих методов невозможно без применения абстракции. Поэтому разработка подходящего отношения симуляции и алгоритма его проверки — ключевая задача в разработке любой инструментальной системы верификации временных автоматов. Однако, отношения симуляции между временными автоматами не так хорошо исследованы, как отношения симуляции между конечными автоматами. В данной работе ставится задача разработки формального определения временной симуляции между игровыми времеными автоматами и построение алгоритма проверки этой симуляции.

Таким образом, в данной работе рассматриваются три задачи, связанные с исследованием подобия, возникающим в анализе программ:

1. задача обнаружения клонов, в которой задействована идея синтаксического подобия,

2. задача построения универсального алгоритма проверки отношений симуляции (семантического подобия) между моделями дискретных программ,

3. задача разработки отношения симуляции для временных игровых автоматов и построения алгоритма проверки этого отношения.

Опишем каждую из трёх поставленных задач более подробно.

Заключение

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

Работа состоит из двух частей. В первой части исследована задача проверки схожести в устройстве программ (синтаксического подобия), а именно, рассмотрена проблема обнаружения похожих фрагментов кода (клонов, дубликатов кода). Во второй части исследуется схожесть поведения программ (семантическое подобие): рассмотрены отношения симуляции — отношения подобия между моделями программ, сохраняющие выполнимость формул темпоральных логик. В качестве формализма задания моделей программ использовались структуры Крипке и временные автоматы.

В диссертационной работе получены следующие основные результаты:

1. Разработан новый алгоритм обнаружения подобных фрагментов в исходных кодах программ (программных клонов), позволяющий находить клоны, от которых можно избавиться при помощи реорганизации кода. Данный алгоритм был реализован в средстве, распространяемом под открытой лицензией. Проведено экспериментальное сравнение результатов работы Clone Digger и двух других средств Asta и CloneDR на основе методики, общепринятой при изучении эффективности средств выявления клонов. Эксперименты показали, что разработанное нами средство превосходит два другие средства как по полноте так и по точности поиска.

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

3. Впервые было разработано отношение симуляции, сохраняющее выполнимость формул логики АТСТЪ на множестве временных игровых автоматов; приведён алгоритм проверки выполнимости данного отношения. Проведено практическое испытание реализации данного алгоритма в задаче синтеза контроллера для системы автоматического управления, модель которой содержит невидимую контроллеру информацию.

Приношу глубокую благодарность своим научным руководителям проф. Р.Л. Смелянскому и доценту В.А. Захарову за постановку задачи и обсуждения в процессе её решения.

1. The algorithmic analysis of hybrid systems / R. Alur, C. Courcoubetis, N. Halbwachs et al. // Theoretical Computer Science. — 1995. — Vol. 138. — Pp. 3-34.

2. Algorithms for omega-regular games with imperfect information / J.-F. Raskin, K. Chatterjee, L. Doyen, Th. A. Henzinger // Logical Methods in Computer Science. — 2007. — Vol. 3, no. 3.

3. Alternating refinement relations / R. Alur, Th. A. Henzinger, O. Kupfer-man, M. Y. Vardi // CONCUR. Vol. 1466 of LNCS. - Springer, 1998. -Pp. 163-178.

4. Alur R., Courcoubetis C., Dill D. L. Model-checking in dense real-time // Inf. Comput. 1993. - Vol. 104, no. 1. - Pp. 2-34.

5. Alur R., Dill D. A theory of timed automata // Theoretical Computer Science. 1994. - Vol. 126, no. 2. - Pp. 183-235.

6. Alur R., Henzinger Th. A., Kupferman 0. Alternating-time temporal logic // FOCS. 1997. - Pp. 100-109.

7. Andersen H. R. Model checking and boolean graphs // Theoretical Computer Science. — 1994. — Vol. 126, no. 1. Pp. 3-30.

8. Baader F., Snyder W. Unification theory // Handbook of Automated Reasoning / Ed. by J.A. Robinson, A. Voronkov. — Elsevier Science Publishers, 2001. Vol. I. - Pp. 447-533.

9. Baker B. S. A program for identifying duplicated code // Computer Science and Statistics: Proc. Symp. on the Interface. — 1992. — March. — Pp. 49-57.

10. Baker B. S. On finding duplication and near-duplication in large software systems // WCRE '95: Proceedings of the Second Working Conference on Reverse Engineering. — Washington, DC, USA: IEEE Computer Society, 1995. Pp. 86-95.

11. Bellman R. Dynamic Programming. — Princeton University Press, 1957.

12. Bengtsson J., Yi W. Timed automata: Semantics, algorithms and tools // Lecture Notes in Computer Science. — New York, NY, USA: Springer, 2004. Pp. 87-124.

13. Bille P. A survey on tree edit distance and related problems // Theor. Comput. Sci. 2005. - Vol. 337, no. 1-3. - Pp. 217-239.

14. Browne M. C., Clarke E. M., Griimberg O. Characterizing finite kripke structures in propositional temporal logic // Theoretical Computer Science. 1988. - Vol. 59, no. 1-2. - Pp. 115-131.

15. Bryant Randal E. Graph-based algorithms for boolean function manipulation // IEEE Transactions on Computers. — 1986. — Vol. 35, no. 8. — Pp. 677-691.

16. Bulychev P.E., Konnov I. V., Zakharov V.A. Computing (bi) simulation relations preserving ctlx logic for ordinary and fair kripke structures // Tpyды Института системного программирования РАН — 2007. — Т. 12. — С. 59-76.

17. Bulychev P., Kostylev Е., Zakharov V. Anti-unification algorithms and their applications in program analysis // PSI. — 2009.

18. Burd EMunro M. Investigating the maintenance implications of the replication of code //in the Proceeedings of the International Conference on Software Maintenance; ICSM'97. IEEE Press, 1997. — Pp. 1-3.

19. Bustan D., Grumberg O. Simulation-based minimization // ACM Transactions on Computational Logic. — 2003. — Vol. 4, no. 2. — Pp. 181-206.

20. Butler M. Incremental design of distributed systems with event-b // Engineering Methods and Tools for Software Safety and Security Marktoberdorf Summer School. - IOS Press, 2008. - Pp. 131-160.

21. Cerans K. Decidability of bisimulation equivalences for parallel timer processes. // CAV. Vol. 663 of LNCS. - Springer, 1992. - Pp. 302-315.

22. Cerans K., Godskesen J. C., Larsen K. G. Timed modal specification theory and tools. // CAV. - Vol. 697 of LNCS. - Springer, 1993. - Pp. 253-267.

23. Chockler II., Kupferman O., Vardi M. Y. Coverage metrics for temporal logic model checking // Formal Methods in System Design. — 2006. — Vol. 28, no. 3. Pp. 189-212.

24. Clarke E. M., Emerson E. A., Sistla A. P. Automatic verification of finite-state concurrent systems using temporal logic specifications // ACM Trans. Program. Lang. Syst.— 1986.- Vol. 8, no. 2,- Pp. 244-263.

25. Clone detection using abstract syntax trees / I. D. Baxter, A. Yahin, L. Moura et al. // ICSM '98: Proceedings of the International Conference on Software Maintenance. — Washington, DC, USA: IEEE Computer Society, 1998. P. 368.

26. Comparison and evaluation of clone detection tools / S. Bellon, R. Koschke, G. Antoniol et al. // IEEE Transactions on Software Engineering. — 2007. Vol. 33, no. 9. - Pp. 577-591.

27. Cooper K. D., Mcintosh N. Enhanced code compression for embedded rise processors 11 PLDI '99: Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation. — ACM, 1999. — Pp. 139-149.

28. Cordy James R. Comprehending reality practical barriers to industrial adoption of software maintenance automation // IWPC. — 2003. — Pp. 196-206.

29. Counterexample-guided abstraction refinement for symbolic model checking / E. Clarke, O. Grumberg, S. Jha et al. // Journal of the ACM.— 2003. September. - Vol. 50, no. 5. - Pp. 752-794.

30. Cp-miner: Finding copy-paste and related bugs in large-scale software code / Z. Li, S. Lu, S. Myagmar, Y. Zhou // IEEE Transactions on Software Engineering. 2006. - Vol. 32, no. 3. — Pp. 176-192.

31. Cudd: Colorado university bdd package. — http://vlsi.colorado.edu/ "fabio/CUDD.

32. D. Stéphane, R. Matthias, D. Serge, A language independent approach fordetecting duplicated code // International Conference on Software Maintenance. IEEE, 1999. - Pp. 109-118.

33. David A. Merging DBMs efficiently // 17th Nordic Workshop on Programming Theory. — DIKU, University of Copenhagen, 2005. — October. — Pp. 54-56.

34. De Nicola R., Vaandrager F. Three logics for branching bisimulation // Journal of the ACM. 1995. - Vol. 42, no. 2. - Pp. 458-487.

35. Detection of software clones: Tool comparison experiment. —http: //www. bauhaus- Stuttgart. de/clones/index. html.

36. Dijkstra E. W. Hierarchical ordering of sequential processes // Acta Informática. 1971. - Vol. 1. - Pp. 115-138.

37. Ducasse S., Rieger M., Demeyer S. A language independent approach for detecting duplicated code. IEEE, 1999. - Pp. 109-118.

38. Edelkamp S. Symbolic exploration in two-player games: Preliminary results //In Proceedings of the Sixth International Conference on AI Planning and Scheduling (AIPS-02) Workshop on Model Checking. — 2002. — Pp. 40-48.

39. Efficient on-the-fly algorithm for checking alternating timed simulation / P. Bulychev, T. Chatain, A. David, K. G. Larsen // 7th International Conference on Formal Modelling and Analysis of Timed Systems. — 2009.

40. Efficient on-the-fly algorithms for the analysis of timed games / F. Cassez, A. David, E. Fleury et al. // CONCUR. Vol. 3653 of LNCS. - 2005. -Pp. 66-80.

41. An empirical study of operating systems errors / A. Chou, J. Yang, B. Chelf et al. // SOSP '01: Proceedings of the eighteenth ACM symposium on Operating systems principles. New York, NY, USA: ACM, 2001. - Pp. 73-88.

42. Etessami K. A hierarchy of polynomial-time computable simulations for automata // CONCUR 2002.— 2002. citeseer.ist.psu.edu/ etessami02hierarchy. html.

43. Etessami K., Wilke T., Schuller R. A. Fair simulation relations, parity games, and state space reduction for biichi automata // SI AM Journal on Computing. 2005. - Vol. 34, no. 5. - Pp. 1159-1175.

44. Evans W. S., Fraser C. W., Ma F. Clone detection via structural abstraction // Reverse Engineering. — 2007.— Vol. 0. — Pp. 150-159.

45. F. Jeanne, O. Karl J., W. Joe D. The program dependence graph and its use in optimization // ACM Transactions on Programming Languages and Systems. 1987. - Vol. 9. - Pp. 319-349.

46. Fernandez J.-C. An implementation of an efficient algorithm for bisimulation equivalence // Science of Computer Programming. — 1989. — Vol. 13. — Pp. 13-219.

47. Graphviz open source graph drawing tools / J. Ellson, E. R. Gansner, E. Koutsofios et al. // Graph Drawing. — 2001. — Pp. 483-484.

48. Groote J. F., Vaandrager F. W. An efficient algorithm for branching bisimulation and stuttering equivalence // Automata, Languages and Programming. — 1990. — Pp. 626-638.

49. Guiding and cost-optimality in uppaal / Gerd Behrmann, Ansgar Fehnker, Thomas Hune et al. // AAAI Spring Symposium Model-Based Validation of Intelligence. — 2001.

50. Gusfield D. Algorithms on strings, trees, and sequences : computer science and computational biology. — Cambridge Univ. Press, 2007. — January.

51. Henzinger M. R., Henzinger Th. A., Kopke P. W. Computing simulations on finite and infinite graphs // 36th IEEE Symp. on Foundations of Comp. Sci. IEEE Computer Society Press, 1996. - Pp. 453-462.

52. Henzinger Th. A. The theory of hybrid automata. — IEEE Computer Society Press, 1996. Pp. 278-292.

53. Henzinger Th. A., Kupferman O., Rajamani S. K. Fair simulation // Information and Computation. — 2002. — Vol. 173, no. 1.— Pp. 64-81.

54. Holzmann G. J. The model checker spin // Software Engineering. — 1997. — Vol. 23, no. 5. Pp. 279-295.

55. Jensen H. E., Larsen K. G., Skou A. Scaling up Uppaal automatic verification of real-time systems using compositionality and abstraction. // FTRTFTS. Vol. 1926 of LNCS. - Springer, 2000. - Pp. 19-30.

56. Johnson J.H. Substring matching for clone detection and change tracking. — 1994.

57. Johnson J. H. Identifying redundancy in source code using fingerprints // Proc. Conf. Centre for Advanced Studies on Collaborative research (CAS-CON).- IBM Press, 1993. Pp. 171-183.

58. Jones N. D. Blindfold games are harder than games with perfect information. 1978. - Vol. 6:4-7.

59. Kamiya T., Kusumoto S., Inoue K. Ccfinder: A multilinguistic token-based code clone detection system for large scale source code // IEEE Transactions on Software Engineering. — 2002. — Vol. 28, no. 7. — Pp. 654-670.

60. Kapser C., Godfrey M. W. "cloning considered harmful "considered harmful // WCRE '06: Proceedings of the 13th Working Conference on Reverse Engineering. — IEEE Computer Society, 2006. — Pp. 19-28.

61. Komondoor R., Horwitz S. Using slicing to identify duplication in source code //In Proceedings of the 8th International Symposium on Static Analysis.— Springer-Verlag, 2001,— Pp. 40-56.

62. Konnov I., Zakharov .V. An invariant-based approach to the verification of asynchronous parameterized networks // Journal of Symbolic Computation. 2009.

63. Koschke R., Falke R., Frenzel P. Clone detection using abstract syntax suffix trees // WCRE '06: Proceedings of the 13th Working Conference on Reverse Engineering. — Washington, DC, USA: IEEE Computer Society, 2006. Pp. 253-262.

64. Krinke J., Softwaresysteme L. Identifying similar code with program dependence graphs. 2001. - Pp. 301-309.

65. Kupferman O., Vardi M. Y. Module checking // Eighth International Conference on Computer Aided Verification CAV. — Vol. 1102. — Springer Verlag, 1996. Pp. 75-86.

66. Lamport L. What good is temporal logic? // IFIP 83.— 1983.— Pp. 657-668.

67. Lanubile F., Mallardo T. Finding function clones in web applications // Software Maintenance and Reengineering, European Conference on — 2003. — Vol. 0. P. 379.

68. Maler O., Pnueli A., Sifakis J. On the synthesis of discrete controllers for timed systems // STACS. Vol. 900. - Springer, 1995. - Pp. 229-242.

69. Marcus A., Maletic J. I. Identification of high-level concept clones in source code. 2001.

70. Mayrand J., Leblanc C., Merlo E. M. Experiment on the automatic detection of function clones in a software system using metrics // Software Maintenance, IEEE International Conference on. — 1996. — Vol. 0. — P. 244.

71. Milner R. An algebraic definition of simulation between programs: Tech. rep. Stanford, CA, USA: 1971.

72. Milner R. A Calculus of Communicating Systems. — Springer-Verlag New York, Inc., 1980.

73. Nielsen M., Clausen C. Bisimulation, games and logic // Dep. of Computer Science, University of Aarhus. — Springer-Verlag, 1994. — Pp. 289-306.

74. Nusmv: a new symbolic model checker / A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri // International Journal on Software Tools for Technology Transfer. — 2000. — Vol. 2.

75. Oancea C., So C., Watt S. M. Generalization in maple. — 2005.

76. Olson D. L., Delen D. Advanced Data Mining Techniques. — Springer, 2008.

77. Paige R., Tarjan R. E. Three partition refinement algorithms // SI AM Journal on Computing. — 1987. — Vol. 16, no. 6. — Pp. 973-989.

78. Park D. Concurrency and automata on infinite sequences // Proceedings of the 5th GI-Conference on Theoretical Computer Science. — London, UK: Springer-Verlag, 1981. Pp. 167-183.

79. Parr T. J., Quong R. W. Antlr: A predicated-ll(k) parser generator // Software Practice and Experience. — 1994. — Vol. 25. — Pp. 789-810.

80. Pattern matching for clone and concept detection / K. A. Kontogiannis, R. Demori, E. Merlo et al. // Journal of Automated Software Engineering. — 1996. Vol. 3. - P. 108.

81. Plotkin G.D. A note on inductive generalization // Machine Intelligence. — Edinburgh University Près, 1970. Vol. 5. — Pp. 153-163.

82. Pnueli A. A temporal logic of concurrent programs // Theoretical computer science. — Vol. 13. — Pp. 45-60.

83. Pycudd: an enhanced python interface to the Colorado university bdd package. — http: / / www. ece. ucsb. edu/bears/pycudd. html.

84. Ramadge P. J. G., Wonham W. M. The control of discrete event systems // Proceedings of the IEEE. 1989. - Vol. 77, no. 1. - Pp. 81-98.

85. Ranzato F., Tapparo F. Computing stuttering simulations // CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory. — Berlin, Heidelberg: Springer-Verlag, 2009. — Pp. 542-556.

86. Raza A., Vogel G., Plodereder E. Bauhaus a tool suite for program analysis and reverse engineering // Ada-Europe. — 2006. — Pp. 71-82.

87. Reif John H. The complexity of two-player games of incomplete information // J. Comput. Syst. Sci. — 1984. Vol. 29, no. 2. - Pp. 274-301.

88. Reynolds J. C. Transformational systems and the algebraic structure of atomic formulas // Machine Intelligence.— Edinburgh University Pres, 1970. Vol. 5. - Pp. 135-151.

89. Roy C. K., Cordy J. R. A survey on software clone detection research // SCHOOL OF COMPUTING TR 2007-541, QUEEN'S UNIVERSITY.-2007. Vol. 115.

90. Sabelfeld A. Confidentiality for multithreaded programs via bisimulation // Andrei Ershov International Conference on Perspectives of System Informatics. — Springer-Verlag, 2003. Pp. 260-273.

91. S0rensen M. H., Gluck R. An algorithm of generalization in positive supercompilation // ILPS. 1995. - Pp. 465^79.

92. Stirling C. Modal and temporal logics for processes // Summer School in Logic Methods in Concurrency. — 1993.

93. Tarski A. A lattice-theoretical fixpoint theorem and its applications. — 1955.

94. Turing Alan M. Computing machinery and intelligence // Mind. — 1950. — Vol. LIX. Pp. 433-460.

95. Vardi M. Y. Alternating automata and program verification //In Computer Science Today. LNCS 1000. Springer-Verlag, 1995. - Pp. 471-485.

96. Weise C., Lenzkes D. Efficient scaling-invariant checking of timed bisimulation // STACS. Vol. 1200 of LNCS. - 1997. - Pp. 177-188.

97. Wettel R., Marinescu R. Archeology of code duplication: Recovering duplication chains from small duplication fragments // Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on — 2005. — Vol. 0. Pp. 63-70.

98. Wulf M. D., Doyen L., Raskin J.-F. A lattice theory for solving games of imperfect information // HSCC, LNCS 3927. Springer, 2006. - Pp. 153-168.

99. Yang W. Identifying syntactic differences between two programs // Software Practice and Experience.— 1991. — Vol. 21.— Pp. 739-755.

100. A. Ахо P. Сети Д. Ульман. Компиляторы. Принципы, технологии, инструменты. — Вильяме, 2003.

101. Даль В.И. Толковый словарь живого великорусского языка. — С.-Петербург Москва: Издание книгопродавца-типографа М. О. Вольфа, 1882.

102. Дж. Ту, Р. Гонсалес. Принципы распознавания образов. — Мир, 1978.

103. Ершов А. П. Современное состояние теории схем программ // Проблемы кибернетики. — 1973. — Vol. 27. — Pp. 87-110.

104. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. МЦНМО, 2002.

105. Костылев Е. Алгоритмы антиунификации и их применение для вычисления инвариантов программ: Ph.D. thesis / Моск. гос. ун-т им. М.В. Ломоносова. — 2008.

106. Котов В.Е., Сабельфелъд В.К. Теория схем программ. — Наука, 1991. — Р. 248.

107. Фаулер М. Рефакторинг. Улучшение существующего кода. — Символ-Плюс, 2008.