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

• Автор: Царьков, Дмитрий Викторович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2002
• Место защиты: Москва
• Количество страниц: 185 с. : ил

Оглавление
Введение б

Идея формальных методов.

Принципы формальной верификации.

Цель работы

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

Структура работы.

1 Современные средства формальной верификации

1.1 Классификация моделей программ и языков спецификации.

1.2 Верификация моделей программ.

1.2.1 Методы верификации

1.2.2 Обзор современных систем верификации моделей программ.
1.2.3 Тенденции развития средств верификации программ.
1.3 Формальная постановка задачи.
. 1.3.1 Распределенные программы
1.3.2 Модели распределенных программ
1.3.3 Логика ветвящегося времени СТЬ
1.3.4 Формальная постановка задачи
Общая схема алгоритмов верификации программ
2.1 Теоретикомножественная схема верификации программ методом проверки на
модели.
2.2 Поиск подтверждающего вычисления.
2.2.1 Линейные трассы
2.2.2 Циклические трассы
2.3 Алгоритмы верификации справедливых моделей программ
2.3.1 Формальное определение справедливости .
2.3.2 Верификация слабо справедливых моделей программ
ОГЛАВЛЕНИЕ
2.3.3 Верификация сильно справедливых моделей программ.
2.3.4 Модификация алгоритма восстановления трасс.
3 Построение моделей распределенных программ
3.1 язык описания распределенных программ
3.1.1 Основные конструкции языка ММ .
3.1.2 Понятие временного автомата
3.1.3 Временные автоматы контекста.
3.1.4 Семантика языка ММ.
3.2 Язык спецификаций
3.3 Язык представления моделей .
3.3.1 Основные конструкции языка .
3.3.2 Семантика языка
3.3.3 Композиционная семантика программ
3.4 Построение модели распределенной программы.
3.4.1 Абстракция ММпрограмм.
3.4.2 Трансляция элементарных конструкций языка ММ.
3.4.3 Моделирование взаимодействия.
3.5 Корректность трансляции .
3.6 Извлечение контрпримера вычисления на ММ.
4 Графовая реализация алгоритмов верификации
4.1 Графовое представление модели.
4.2 Графовый алгоритм.
4.3 Алгоритм восстановления трасс.
4.4 Справедливая верификация.
4.4.1 Графовый алгоритм верификации в ограничениях слабой справедливости
4.4.2 Графовый алгоритм верификации в ограничениях сильной справедливости
5 Символьная реализация алгоритмов верификации
5.1 Представления булевых функций
5.1.1 Базовые сведения о .
5.1.2 Операции над .
5.2 Символьное представление модели .
5.3 Алгоритм символьной верификации.
5.3.1 Методы повышения эффективности символьной верификации
ОГЛАВЛЕНИЕ
5.4 Алгоритм восстановления трасс
5.5 Справедливая верификация
5.5.1 Алгоритм символьной верификации в ограничениях слабой справедливости
5.5.2 Алгоритм символьной верификации в ограничениях сильной справедливости .
6 Система верификации в среде ДИАНА
6.1 Устройство системы верификации в среде ДИАНА.
6.2 Практические результаты применения системы верификации.
Литература


В этой главе описывается конкретная реализация теоретико-множественных алгоритмов из главы 2 для использования применительно к моделям Крипке, представленным графом переходов. Пятая глава посвящена алгоритмам символьной верификации программ методом проверки на модели. Особенность символьных методов заключается в том, что модель не строится целиком, а описывается в виде формул, с которыми и происходит работа. В этой главе описана конкретная реализация теоретико-множественных алгоритмов из главы 2 применительно к моделям Крипке, представленным в символьном виде. Шестая глава описывает реализацию разработанных алгоритмов в среде ДИАНА. Можно выделить несколько основных признаков, по которым удается провести достаточно содержательную классификацию всего многообразия моделей программ и соответствующих им языков спецификации. К таким признакам относятся парадигмы параллелизма и времени, уровень абстракции, типы моделей вычислений и ряд других более частных характеристик. Парадигмы параллелизма. В соответствии с известными представлениями о различных типах параллельных вычислений [] модели распределенных программ можно классифицировать по следующим основным характеристикам: интенсиональные — экстенсиональные синхронные - асинхронные чередование - истинный параллелизм. Интенсиональные и экстенсиональные модели. Интенсиональные модели описывают поведение системы в терминах действий, происходящих внутри системы, в то время как экстенсиональные модели описывают поведение на основе последовательностей событий, происходящих в системе и доступных для наблюдений извне. Интенсиональные модели обычно используются, если мы имеем описание функционирования системы, и желаем что-нибудь узнать о ее поведении. Примерами таких моделей являются размеченные системы переходов [], различные алгебраические формализмы [5, , ], автоматы [6, ,5] и сети Петри [9,]. ГЛАВА 1. Основное доступное нам наблюдение — трасса вычисления модели как последовательность элементарных состояний []. На базе трасс вычислений основываются допускающие деревья [], синхронизационные деревья [4], трассы Мазуркиевича [2], запрещающие множества [], истории [8] и ряд других формализмов. Поскольку при верификации распределенных программ мы располагаем текстом программы и нам полностью известна ее структура, далее мы будем рассматривать интен-сиональные модели. Синхронные и асинхронные модели. При построении синхронных моделей параллельных вычислений распределенной системы подразумевается, что все компоненты системы функционируют согласованно в едином масштабе времени. Вычисление всей системы разбивается на отдельные такты, и на каждом такте каждый компонент системы выполняет свое очередное действие []. Обычно такое разбиение вычисления системы на такты достигается за счет прохождения по всей системе тактовых импульсов, общих для всех ее компонентов. Поэтому синхронные модели параллельных вычислений применяются для описания аппаратуры (процессоров, контроллеров и т. В асинхронных моделях параллельных вычислений, напротив, подразумевается, что каждый компонент распределенной системы функционирует в своем собственном масштабе времени независимо от других компонентов. Это означает, в частности, что временные отрезки, на протяжении которых выполняются отдельные действия двух разных процессов, могут располагаться весьма произвольно друг относительно друга, в том числе перекрываться, совпадать, не пересекаться. Единственное ограничение, которое должно быть соблюдено — это сохранение причинно-следственной зависимости между отдельными действиями различных процессов. Асинхронные модели применяются для описания распределенных программ (сетевых протоколов, операционных и управляющих систем, И т. Истинный параллелизм и чередование. Семантика истинного параллелизма определяется отношением причинно-следственной зависимости между отдельными базовыми действиями компонентов распределенной системы. Предполагается, что на каждом шаге вычисления может исполниться любое множество попарно независимых действий. Семантика истинного параллелизма свойственна таким моделям, как сети Петри, трассы Мазуркиевича, некоторым разновидностям алгебраических моделей.