Исследование и разработка семантических методов анализа распределенных программ Шипов Андрей Александрович

Содержание к диссертации

Введение

Глава 1. Исследование проблемы 12

1.1. Задача верификации 12

1.1.1. Экспертиза 15

1.1.2. Статический анализ 17

1.1.3. Динамические методы верификации 18

1.1.4. Синтетические методы верификации 19

1.1.5. Формальные методы верификации 20

1.1.6. Классификация методов верификации программного обеспечения 21

1.1.7. Актуальность верификации 24

1.1.8. Международные стандарты верификации 26

1.2. Model Checking. Верификация больших распределенных программных систем 27

1.2.1. Возникновение больших распределенных программных систем 29

1.2.2. Возникновение метода Model Checking 32

1.2.3. Идея алгоритма Model Checking 32

1.2.4. Логика линейного времени LTL и алгоритм Model Checking 34

1.2.5. Инструменты верификации для метода Model Checking 36

1.2.6. Примеры верификации распределенных программных систем 37

1.3. Проблема избыточности верифицируемого множества вычислительных последовательностей, ускорение процесса верификации БРПС 38

1.3.1. Темпы роста сложности программных систем 38

1.3.2. Ускорение процесса верификации БРПС 40

1.3.3. Избыточность верифицируемых моделей 42

1.4. Выводы по главе 43

Глава 2. Вопросы повышения эффективности верификации больших распределенных программных систем 45

2.1. Метод ограничений верифицируемых моделей 45

2.1.1. Ограничение моделей программных систем 46

2.1.2. Ограничение моделей распределенных программных систем 51

2.1.3. Эффективность метода ограничения моделей 55

2.1.4. Расширение метода ограничений 58

2.2. Распределенный метод верификации моделей 60

2.2.1. Инструмент формальной верификации «Spin» 61

2.2.1.1. Распределенная верификация в Spin. 63

2.2.2. Распределенный алгоритм верификации автоматов Бюхи 66

2.2.2.1. Поиск допустимых состояний 67

2.2.2.2. Поиск циклов из допустимых состояний 68

2.2.2.3. Суперлинейное ускорение 69

2.2.2.4. Результаты 72

2.2.2.5. Сравнение со Spin 76

2.3. Выводы по главе 78

Глава 3. Эквациональная характеристика LTL 81

3.1. Расширение выразительности LTL 82

3.1.1. Эквациональная характеристика операторов LTL (RLTL) 84

3.1.2. Примеры описания свойств в RLTL-нотации 85

3.1.3. Верификация RLTL 88

3.1.4. Формальный вывод 91

3.2. Абстракция моделей на базе RLTL 92

3.3. Выводы по главе 94

Глава 4. Разработка и апробация программного комплекса верификации больших распределенных систем 96

4.1. Реализация системы анализа и метода верификации для больших распределенных программных систем 96

4.1.1. Спецификация системы 97

4.1.1.1. Диаграмма вариантов использования 97

4.1.1.2. Диаграмма классов 98

4.1.1.3. Диаграмма последовательности 101

4.1.1.4. Диаграмма взаимодействия 104

4.1.1.5. Диаграмма активности

4.1.2. Выбор языка программирования 106

4.1.3. Результаты разработки 108

4.2. Апробация комплекса 116

4.2.1. Работа с комплексом и тестирование примеров 116

4.2.1.1. Тестирование примера верификации микроволновой печи 117

4.2.1.2. Тестирование примера верификации большой системы 125

4.2.2. Внедрение комплекса 127

4.3. Выводы по главе 128

Заключение 130

Список сокращений и условных обозначений 133

Список литературы 134

• Синтетические методы верификации
• Ограничение моделей программных систем
• Примеры описания свойств в RLTL-нотации
• Диаграмма вариантов использования

Введение к работе

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

параллельного программирования, получивших широкое

распространение за последние два десятилетия, обязывают

программистов вырабатывать совершенно новые навыки и подходы
программирования. Эти проблемы касаются и программных

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

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

распределенных программных систем и формулирования

верифицируемых условий. Например, для программы, в рамках которой могут одновременно выполняться 20 потоков, каждый из которых может находиться в одном из 5 состояний, общее число состояний вычислительного процесса может достигать 5²⁰ = 95 367 431 640 625, это может стать непреодолимым препятствием при попытке верификации тех или иных свойств системы. Кроме того, в ней могут явно присутствовать те вычисления, переход в которые на практике никогда не встретится в реальных условиях.

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

Степень разработанности.

Вопросы верификации распределенных программных систем подробно рассмотрены в работах C. A. R. Hoare, D. Harel, С. Алагич, М. Арбиб, Ю. Г. Карпова, Ю. П. Кораблина, А. А. Шалыто, М. А. Лукина, С. Э. Вельдера, В. С. Гурова, Э. М. Кларка, О. Грамберга, Д. Пеледа, В. В. Кулямина, Р. Блэк, В.П. Котлярова, С. Канер, Дж. Фолк, Нгуен Енг Кек, И. В. Винниченко, Л. Тамре, Z. Manna, A. Pnueli, B. Brard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P.Schnoebelen, W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D.Notkin, J. D. Reese и других.

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

распределенных программных систем из-за так называемого

«комбинаторного взрыва» не решена в полной мере, и на сегодняшний день существуют лишь два основных подхода, позволяющих в той или иной степени преодолевать её:

1. Построение более абстрактной, менее детализированной модели на базе исходной (редукция по конусу влияния и абстракция данных)

2. Выполнение верификации модели на ее приведенном к некоторому сжатому виду представлении (символьные методы верификации)

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

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

Объектом диссертационного исследования являются модели больших распределенных программных систем.

Предметом диссертационного исследования является

верификация моделей больших распределенных программных систем.

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

верифицируемых свойств с целью повышения эффективности процесса верификации для метода проверки на моделях (Model Checking). Также в работе ставится цель разработки новых инструментальных средств повышения быстродействия при анализе больших распределенных систем.

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

3. Исследование современных средств и методов верификации больших распределенных программных систем.

4. Разработка новых средств и методов:

1. Исключения избыточных и невыполнимых на практике состояний из процесса верификации.

2. Оценки эффективности исключения избыточных и невыполнимых на практике состояний из процесса верификации.

3. Распределенного анализа свойств моделей.

4. Расширения описательной мощности логики LTL.

3. Разработка программного комплекса для анализа и верификации больших распределенных программных систем на базе предложенных методов.

4. Апробация разработанного комплекса методов на практике для реальных задач верификации больших распределенных программных систем.

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

1. Метод ограничения верифицируемых моделей для метода «Model Checking» и оценка его эффективности.

2. Метод распределенной верификации свойств моделей.

3. Средства расширения мощности логики LTL за счет приведения её к эквациональной форме (RLTL).

Достоверность полученных результатов. Прежде всего,

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

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

метод верификации на моделях «Model Checking» в качестве нового отдельного этапа.

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

Разработанные в рамках диссертационного исследования алгоритмы внедрены в следующих организациях, о чем имеются соответствующие акты:

4. В научно-исследовательском и производственном предприятии оборонного комплекса АО «Корпорация «Московский институт теплотехники» (МИТ).

5. В ведущей компании по производству полиэфирных смол России и стран СНГ «Дугалак».

6. В «Российском государственном социальном университете» на кафедре информационных систем, сетей и безопасности.

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

Теоретические основы математической логики

Теория конечных автоматов и автоматов Бюхи

Теория рекурсивных функций

Логика линейного времени (LTL)

Метод «Model Checking» для LTL

Для оценки сложности созданных методов использовались математический и понятийный аппараты оценки алгоритмической сложности. Разработка и реализация программного комплекса осуществлялись на базе теорий и методик объектно-ориентированного и параллельного программирования.

На публичную защиту выносятся следующие положения:

7. Метод ограничения верифицируемых моделей для метода «Model Checking» и оценки его эффективности.

8. Метод распределенной верификации свойств моделей.

9. Средства расширения мощности логики LTL за счет приведения её к эквациональной форме (RLTL).

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

Публикации и апробация работы. Основные положения диссертационной работы докладывались и обсуждались на следующих семинарах и конференциях:

11. XIII Международный социальный конгресс «Сплоченность общества и социальная справедливость: мировые тренды и российская реальность» РГСУ. 25-26 ноября 2013 года.

12. XV Студенческая международная научно-практическая конференция. Новосибирск, декабрь 2013.

13. Конференция в рамках IX Недели науки молодежи СВАО города Москвы. Апрель 2014 года.

14. Global science and innovation: III международная научная конференция. Чикаго, октябрь 2014.

15. Конференция аспирантов и молодых ученых-2015 «Памяти А.П.Починка». 12-18 марта 2015, РГСУ.

16. VIII Международная научно-практическая конференция. Научная публикация: Актуальные вопросы науки, технологии и производства. Санкт-Петербург, 17-18 апреля 2015.

17. II International Conference Engineering & Telecommunication En&T 2015. November 18-19, 2015.

18. Конференция аспирантов и молодых ученых-2016 «Памяти А.П.Починка». 16-18 марта 2016, РГСУ.

Основные результаты диссертационного исследования были опубликованы в 10 работах:

9 статей, из них 3 в изданиях, включенных в перечень ведущих рецензируемых журналов, рекомендованных ВАК, и 4 в изданиях, индексируемых РИНЦ

1 - тезисы конференций

Структура работы. Диссертационное исследование состоит из введения, 4 глав, заключения и списка использованной литературы. Общий объем работы составляет 140 страниц, в работе присутствуют:

62 рисунка, 10 таблиц, отдельный том из библиографический список из 87 наименований.

2 приложений

и

Синтетические методы верификации

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

Сегодня существует два основных типа методов динамической верификации, а именно:

1. Мониторинг - тип методов верификации, заключающейся в наблюдении, записи и оценки результатов работы программного обеспечения в его обычном режиме с целью выявления и обнаружения ошибок и неисправностей. 2. Тестирование – тип методов верификации, заключающейся в наблюдении, записи и оценки результатов работы программного обеспечения, выполняемого в рамках заранее подготовленных сценариев с целью выявления и обнаружения ошибок и неисправностей.

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

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

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

Более подробно вопросы динамических методов верификации и тестирования рассмотрены в [23–30].

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

1. Тестирование на основе моделей или «Model-based Testing» – процесс разработки и построения формальных моделей требований к проверяемой программной системе и последующей генерации тестов на их основе.

2. Мониторинг формальных свойств («Runtime Verification» и «Passive Testing») – процесс выявления формальных свойств программной системы, требующих проверки для их последующего включения в систему мониторинга и дальнейшего анализа.

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

4. Синтетическое структурное тестирование – процесс, при котором после первого случайно выбранного теста автоматически генерируются другие тесты таким образом, чтобы обеспечить покрытие ранее не покрытых элементов кода. Более подробно вопросы синтетических методов верификации рассмотрены в [23; 31; 34; 35].

Формальные методы верификации – методы верификации математической модели программной системы, реализованной на базе её программного кода. Требование к такой системе формулируется в виде некоторой формальной спецификации, после чего производится проверка его выполнимости относительно данной модели.

На сегодняшний день существует три основных типа формальных методов верификации: 1. Дедуктивный анализ - метод формальной верификации логико-алгебраических моделей при помощи дедуктивного анализа, который был предложен Флойдом и Хоаром.

2. Проверка моделей или «Model Checking» - метод формальной верификации распределенных программных систем с конечным числом состояний. Проверяет соответствие программной системы, представленной чаще всего в виде модели Крипке, заданной формальной спецификации, сформулированной на основе временной логики.

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

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

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

Более подробно вопросы формальных методов верификации рассмотрены в [2; 3; 13; 14; 19; 23; 36].

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

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

Ограничение моделей программных систем

В качестве результирующего автомата, удовлетворяющего заданному ограничению, для которого будет выполняться верификация проверяемых свойств, примем автомат Бюхи R(BmB), где R – функция редукции, исключающая сначала все «изолированные» и «недопускающие» состояния, а затем все «допускающие» состояния, из которых не существует ни одного перехода. «Изолированными» будем называть такие состояния, в которые не существует ни одного пути из начального состояния. На рис. 2.6 изображен данный автомат.

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

Теперь выполним проверку того, возможна ли работа печи с открытой дверцей. Для проверки данного свойства введем следующую формулу временной логики LTL: 1 = G(w c) – «Всегда, если печь работает, то значит, дверца закрыта». Возьмем отрицание данной формулы 1 = (G(w c)) = F(w c) и построим для нее соответствующий автомат Бюхи, который изображен на рис. 2.7.

Этот автомат переходит в допускающее состояние только в случае возникновении ошибки, то есть тогда, когда микроволновая печь будет работать с открытой дверцей. Таким образом, построив синхронную композицию данного автомата и проверяемого, мы можем установить, способна ли наша система перейти в ошибочное состояние и, если да, то в каком случае. Композиция автоматов R(BmB) и B( 1) представлена на рис. 2.8.

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

Рассмотрим работу данного метода и на примере распределенной программной системы, реализованной на основе модели «читатели-писатели». В нашем случае система будет состоять из трех потоков «писателей», осуществляющих запись в разделяемый ресурс, и двух потоков «читателей», имеющих возможность производить чтение из данного ресурса. Условимся, что производить запись одновременно всегда может лишь один из «писателей», и право на чтение имеет любой из «читателей», пока не осуществляется запись. Также введем следующее условие: как только какой-либо «писатель» хочет начать записывать, то процесс чтения для всех «читателей» автоматически прекращается. Данная модель может быть, например, задана структурой Крипке, представленной на рис. 2.9.

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

Введем для нашей системы следующее ограничение: «Всегда осуществляется запись» – с целью оставить лишь потоки «писателей», так как только они способны забрать ресурс в бессрочное пользование в рамках заданных нами условий. Представим это ограничение в виде формулы временной логики LTL: = G(W1 W2 W3) и построим для неё соответствующий автомат Бюхи (рис. 2.11). В данном случае входной алфавит S нашего автомата над множеством 2АР, примет следующий вид Е={0, {Wl}, {W2}, {W3}, {Rl}, {R2}, {Wl, W2}, ..., {Wl, W2, W3, Rl, R2}}, AP={W1, W2, W3, Rl, R2}.

Окончательный результат ограничения нашей модели, после применения функции редукции R к композиции BmB, приведен на рис. 2.13. Рис.2.13. Автомат Бюхи R(BmB)

Теперь на имеющейся ограниченной вычислительной последовательности нашей модели, выполним проверку на существование тупиков. Для этого введем следующую LTL формулу: 1 = GF( Wi) – «Всегда в будущем процесс записи для любого из потоков будет обязательно завершен». Возьмем отрицание этой формулы 1 = FG(Wi) и попытаемся доказать, что в будущем хотя бы раз встретиться такой «писатель», который никогда не освободит разделяемый ресурс. Автомат Бюхи для формулы 1 представлен на рис. 2.14.

Как видно из этого рисунка, данный автомат перейдет в допускающее состояние только в том случае, если существует переход, помеченный {Wi}, и допускающее состояние всегда будет переходить само в себя только по переходу, помеченному тем же {Wi}. Композиция автоматов R(BmB) и B( 1) представлена на рис. 2.15. Рис. 2.15. Автомат Бюхи R(BmB)B( 1)

В данной композиции существует переход в допускающее состояние (S1, 2), что свидетельствует о том, что формула 1 выполняется, и в нашей системе может возникнуть тупиковая ситуация в случае работы первого «писателя». Из состояний (S2, 1) и (S3, 1) нет переходов в допускающие, так как если бы, например, мы перешли из состояния (S2, 1) в (S2, 2) по переходу {W2}, то в соответствии с контрольным автоматом на рис. 2.7, мы имели бы возможность переходить дальше только по переходам, печенным {W2}. Однако, из состояния (S2, 2) существует переход, например, в состояние (S3, 2), из которого в свою очередь существует переход, помеченный {W3}, что явно противоречит нашему контрольному автомату.

Примеры описания свойств в RLTL-нотации

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

Как видно на рис. 2.22 суперлинейное ускорение может достигаться за счет того, что линейному алгоритму (а) может потребоваться больше шагов для нахождения допустимого состояния с циклом, чем параллельному (б). В данном случае, если условиться, что время на поиск цикла или его отсутствия для всех допустимых состояний будет равным, то двухпоточному алгоритму потребуется всего один шаг, а последовательному – три, что позволяет получить коэффициент ускорения на втором этапе больше, чем два. В табл. 2.4 показаны среднестатистические значения ускорения распределенного алгоритма верификации автоматов Бюхи относительно последовательного, для случая поиска всех контрпримеров на одном, двух, трех и четырех ядрах. А в табл. 2.5, для более полного представления работы алгоритма, представлены аналогичные данные, только для случая поиска алгоритмом не всех контрпримеров, а любого из них.

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

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

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

Сопоставление времен выполнения каждого из подходов показывает, что поиск всех контрпримеров длится в среднем в 6.5 раз дольше, чем поиск одного контрпримера при использовании того же числа потоков. Однако из рис. 2.24 видно, что существенные отличия в ускорениях между данными подходами возникают, лишь когда размеры модели крайне маленькие (меньше 256 состояний). Это можно обосновать тем, что в случае поиска только одного контрпримера второй этап алгоритма дает значительно меньший прирост скорости, чем в случае поиска всех контрпримеров, поскольку его работа прекращается сразу же после нахождения любым из потоков допустимого состояния с циклом. А, так как линейному алгоритму в случае с моделью небольшого размера на втором этапе нужно проверить лишь весьма малое число допустимых состояний на наличие циклов и не требуется тратить время на создание потоков, то он оказывается более эффективным.

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

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

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

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

Диаграмма вариантов использования

Для получения наиболее полного и точного представления о разрабатываемой системе задание её спецификации будет осуществляться с помощью унифицированного языка моделирования UML или «Unified Modeling Language», который применяется в процессе разработки программного обеспечения на этапе проектирования [78; 79; 80]. В работе используются диаграммы следующих видов:

Рассмотрим каждую из диаграмм и проведем их структурный анализ для комплекса верификации «LDS-Verifier». Сформулируем функциональные требования к программному комплексу, определив основные варианты использования системы пользователем. Пользователь должен иметь следующие возможности. Верификация свойств больших распределенных программных систем на базе линейного или распределенного алгоритма с возможностью ограничения вычислительных последовательностей верифицируемой модели. Загрузка автоматов моделей системы, верифицируемых и ограничивающих условий из файлов с различными структурами данных (Buchi, LTL, RLTL) или на базе алгоритма случайной генерации. Построение синхронной композиции автоматов любых сочетаний: модели и верифицируемого условия, модели и ограничивающего условия, верифицируемого и ограничивающего условий. Возможность сохранения в файл любого загруженного ранее или полученного в результате композиции автомата. Таким образом, исходя из представленных функциональных требований, была разработана следующая диаграмма вариантов использования или «Use case diagram» программного комплекса (рис. 4.1).

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

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

Четвертая группа классов предоставляет возможности работы с формулами RLTL. Данная группа отвечает за загрузку формул LTL и RLTL и последующую их конвертацию в автоматы Бюхи по описанному в главе 3 методу.

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

На рис. 4.2 изображена соответствующая диаграмма классов или «Class diagram», состоящая из двенадцати основных классов, без учета классов, реализующих программный интерфейс комплекса.

Для полного представления свойств разрабатываемой системы необходимо рассмотреть работу и взаимодействие её компонентов во времени. Выделим следующие основные этапы работы системы в их хронологическом порядке: 1. Запуск системы пользователем 2. Загрузка пользователем необходимого числа автоматов моделей, верифицируемых и ограничивающих условий 3. Выбор среди загруженных автоматов автомата модели, автомата ограничивающего условия (если требуется) и списка автоматов верифицируемых условий 4. Запуск пользователем процесса верификации 5. Выбор метода верификации 6. Усечение числа вычислительных последовательностей верифицируемой системы с помощью ограничивающего условия (если выбран автомат ограничивающего условия и оценка эффективности ограничения дает положительный результат)