«САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ С. Э. Вельдер, М. А. Лукин, А. А. Шалыто, Б. Р. Яминов ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ Санкт-Петербург Наука 2011 УДК 004 ББК ...»

1

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ

С. Э. Вельдер, М. А. Лукин,

А. А. Шалыто, Б. Р. Яминов

ВЕРИФИКАЦИЯ

АВТОМАТНЫХ ПРОГРАММ

Санкт-Петербург «Наука»

2011 УДК 004 ББК –018*32.973 В 31 Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.

ISBN 978-5-02-038160-5 В книге рассматриваются вопросы верификации программного обеспечения на основе проверки моделей с использованием различных языков спецификации.

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

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

Рецензенты:

докт. техн. наук, проф. В. И. ВОРОБЬЕВ (СПИИРАН), докт. техн. наук, проф. В. Ф. МЕЛЕХИН (СПбГПУ), докт. техн. наук, проф. М. Б. СЕРГЕЕВ (СПбГУАП) Санкт-Петербургский государственный университет информационных технологий, механики и оптики, Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р., Издательство «Наука», ISBN 978-5-02-038160- Оглавление Введение

Глава 1. Валидация систем

1.1. Задачи валидации систем

1.2. Симуляция

1.3. Тестирование

1.4. Формальная верификация

1.5. Проверка моделей

1.6. Автоматическое доказательство теорем

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

2.2. Проверка моделей для линейной темпоральной логики..... 2.2.1. Синтаксис LTL

2.2.2. Семантика LTL

2.2.3. Аксиоматизация

2.2.4. Расширения LTL

2.2.5. Спецификация свойств в LTL

2.2.6. Проверка моделей для LTL

2.2.7. Верификация LTL при помощи автоматов Бюхи

2.3. Проверка моделей для ветвящейся темпоральной логики. 2.3.1. Синтаксис CTL

2.3.2. Семантика CTL

2.3.3. Некоторые аксиомы CTL

2.3.4. Сравнение выразительной силы CTL, CTL* и LTL

2.3.5. Спецификация свойств в CTL

2.3.6. Условия справедливости в CTL

2.3.7. Проверка моделей для CTL и CTL*

2.4. Поиск справедливых путей

2.4.1. Двойной обход в глубину

2.4.2. Поиск сильно связных компонент

2.5. Проверка моделей для темпоральной логики реального времени

2.5.1. Временные автоматы

2.5.2. Семантика временных автоматов

2.5.3. Синтаксис TCTL

2.5.4. Семантика TCTL

2.5.5. Спецификация временных свойств в TCTL

2.5.6. Эквивалентность часовых оценок

2.5.7. Регионные автоматы

2.5.8. Проверка моделей для регионных автоматов

2.6. Сети Петри

Глава 3. Обзор верификаторов

3.1. SPIN

3.2. SMV

Глава 4. Верификация автоматных программ

4.1. Автоматные программы

4.2. Обзор существующих решений

4.3. Средства и объекты верификации

4.3.1. Модель банкомата

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

4.4. Инструменты, использующие готовые верификаторы..... 4.4.1. Converter

4.4.2. Unimod.Verifier

4.4.3. FSM Verifier

4.5. Автономные верификаторы

4.5.1. CTL Verifier

4.5.2. Automata Verificator

Заключение

Список источников

Алфавитный указатель

Понятие валидации В повседневной жизни явно (при использовании компьютеров и интернета) или неявно (при использовании телевизоров, микроволновых печей, мобильных телефонов, автомобилей, общественного транспорта и т. д.) все чаще используются информационные технологии. В 1995 г. было подсчитано, что человек в день взаимодействует с 25 устройствами, обрабатывающими информацию. Известно также, что 20 % стоимости разработки автомобилей, поездов и самолетов приходятся на компьютерные компоненты. Ввиду высокой интеграции информационных технологий во всех приложениях приходится все больше полагаться на надежность программных и аппаратных средств. Естественно полагать, что не должно быть ситуаций, когда телефон неисправен или когда видеомагнитофон непредсказуемо и неверно реагирует на команды, посылаемые с пульта управления. Тем не менее, эти ошибки в определенном смысле малозначимы. Однако ошибки в системах, критичных в отношении безопасности, таких как, например, атомные электростанции или системы управления полетами, неприемлемы.

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

Даже если отвлечься от аспектов безопасности, ошибки все равно могут быть очень дорогими, особенно если они проявляются в процессе работы системы – после того, как продукт выпущен на рынок. Известно несколько впечатляющих примеров таких негативных последствий. Например, ошибка в команде деления чисел с плавающей запятой в процессоре Intel Pentium причинила ущерб около 500 миллионов долларов. Крупный ущерб был причинен также крушением ракеты Ariane-5, которое, вероятно, произошло вследствие ошибки в программе управления полетом.

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

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

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

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

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

Формальная верификация, как противоположность тестированию, основана на математическом доказательстве корректности программ.

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

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

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

Предмет рассмотрения книги Книга посвящена концепциям, алгоритмам и инструментам для проверки моделей программ.

Идеи проверки моделей имеют такой математический фундамент как логика, теория автоматов, структуры данных, алгоритмы на графах.

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

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

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

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

Изложение общих вопросов валидации, математического аппарата и примеров верификации моделей в первых трех главах следует курсу лекций П. Катоена [1].

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

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

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

Содержание четвертой главы основано на результатах работ по государственному контракту «Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода», выполнявшемуся в рамках Федеральной целевой программы «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007–2012 годы» по мероприятию «Проведение проблемно-ориентированных поисковых исследований и создание научно-технического задела по перспективным технологиям в области информационно-телекоммуникационных систем». Работы выполнялись в Санкт-Петербургском государственном университете информационных технологий, механики и оптики (СПбГУ ИТМО).

Содержание книги подтверждает известное положение программной инженерии: «то, что не специфицировано формально, не может быть проверено, а то, что не может быть проверено, не может быть безошибочно».

Авторы благодарны В. Н. Васильеву и В. Г. Парфенову за многолетнюю поддержку и помощь.

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

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

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

Схематически стратегия валидации изображена на рис. 1.1 [1].

Рис. 1.1. Схематическое изображение апостериорной валидации систем Какова общая практика решения вопроса, когда проводить валидацию? Ясно, что проверка на ошибки только в конце разработки неприемлема: если ошибка найдена, требуется много усилий для того, чтобы ее исправить, так как весь процесс разработки должна быть пройден вновь, для того чтобы увидеть, где и как ошибка могла возникнуть. Подобные операции обычно являются затратными.

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

Рис. 1.2. Схематическое изображение валидации систем «на лету»

На практике для того, чтобы убедиться, что конечный результат выполняет то, что предписано, применяются два метода: экспертный анализ и тестирование. Исследования в области разработки программ показывают, что 80% всех проектов используют экспертный анализ – полностью ручную деятельность, в которой прототип или его часть исследуется командой специалистов, которые не были вовлечены в процесс разработки этой компоненты системы. Тестирование является важным методом валидации для проверки корректности полученных реализаций. Однако обычно тесты генерируются вручную, и инструментальной поддержке уделяется мало внимания.

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

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

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

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

симуляция;

тестирование;

формальная верификация;

проверка моделей (верификация на моделях).

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

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

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

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

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

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

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

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

Как отмечалось выше, широко используемым традиционным путем валидации корректности проекта является тестирование [6]. В тестировании система используется в том виде, в каком она реализована (программа, устройство или их комбинация). На ее вход подаются определенные значения входных данных, называемых тестами, и исследуется реакция системы. После этого проверяется, действительно ли реакция системы соответствует требуемому выходу.

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

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

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

когда корректную модель системы сложно построить;

когда части системы не могут быть формально промоделированы (например, физические устройства);

когда модель проприетарна.

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

Например, в области коммуникационных протоколов этот тип исследований привел к проекту международного стандарта «Формальные методы в тестировании пригодности» [7]. В нем процесс тестирования разделен на несколько фаз:

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

2. Выбор тестов. Выбирается множество образцов абстрактных описаний тестов.

3. Реализация тестов. Абстрактные описания тестов трансформируются в исполнимые тесты.

4. Исполнение тестов. Исполнимые тесты применяются к тестируемой реализации путем выполнения их на тестирующей системе. Рассматриваются и протоколируются результаты исполнения.

5. Тестовый анализ. Запротоколированные результаты анализируются с целью определения, удовлетворяют ли они ожидаемым результатам.

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

Тестирование – это метод, который может быть применен как к прототипам, в форме систематической симуляции, так и к конечным продуктам. Известны два базовых подхода: тестирование белого ящика, когда внутренняя структура реализации может наблюдаться и иногда частично управляться (стимулироваться), и тестирование черного ящика [8]. Во втором случае может быть проверена только коммуникация между тестируемой системой и окружением, а внутренняя структура «ящика» полностью скрыта от тестера. В практических обстоятельствах тестирование находится где-то между этими двумя крайними случаями и иногда называется тестированием серого ящика.

Перечислим основные виды тестов.

1. Модульные тесты (Unit tests). Тест пишется на класс, отдельный метод этого класса и т. д. Обычно проверяется один сценарий использования класса, метода или иного модуля.

2. Функциональные тесты. Тестируется не элемент кода, а функциональность. Такие тесты позволяют выявлять структурные ошибки.

3. Приемочные тесты. Проверяется, что программа делает именно то, что хотел заказчик.

4. Стресс-тесты. Тестируется работоспособность программы под сильной нагрузкой.

5. Тесты «на дурака» (monkey test). Программе подаются случайные входные данные, и проверяются ее работоспособность на таких данных и отказоустойчивость. Также проверяется наличие уязвимостей. Такие тесты особенно важны для серверных приложений.

6. Параллельные тесты. Проверяется, что новая версия работает так же, как старая.

7. Регрессионные тесты. Пишутся после сообщения об ошибке. Тест повторяет сценарий, при котором произошла ошибка.

Разработка через тестирование (Test-driven development) Одной из технологий разработки программного обеспечения является разработка через тестирование (test-driven development – TDD) [9].

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

1. Написание теста.

2. Компиляция теста. Тест не должен компилироваться. Если тест компилируется, то это означает, что создана сущность, которая уже присутствует.

3. Устранение ошибки компиляции.

4. Запуск теста. Тест не должен проходить.

5. Написание кода. Пишется максимально простой код, какой только возможен.

6. Прогон теста. На этот раз тест должен быть пройден.

7. Рефакторинг (если требуется).

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

Когда программа использует оборудование, доступ к которому затруднен, применяются мок-объекты или моки [9] (mocks). Моки – это автоматически сгенерированные заглушки. Также моки могут использоваться для программирования сверху вниз [10]. Для создания мок-объектов существуют специальные фреймворки (RhinoMock, NMock, JMock и др.).

Свойства разработки через тестирование:

подход заставляет разрабатывать программу с точки зрения пользователя;

он заставляет писать классы, независимые друг от друга;

тесты являются также и документацией к коду;

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

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

Для формальной верификации требуются:

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

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

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

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

Здесь p – базовое предложение (например, «x равно 2»), символ «» – отрицание, а символ «» – дизъюнкция. Другие логические связки могут быть определены следующим образом: = ( ), true =, false = true и =. Для простоты опустим кванторы существования и всеобщности.

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

Для построения доказательств используется формальная система – множество правил вывода. Эти правила обычно соответствуют построению программы (алгоритма). Они записываются следующим образом:

Здесь – предусловие, S – программный оператор, а – постусловие.

Тройка {} S {} известна как тройка Хоара [13] и названа в честь одного из пионеров в области формальной верификации компьютерных программ. Существуют две интерпретации троек Хоара в зависимости от того, частичная или тотальная корректность рассматривается.

Формула {} S {} называется частично корректной, если каждое останавливающееся вычисление S, стартующее в состоянии, в котором выполняется, финиширует в состоянии, в котором выполняется.

Формула {} S {} называется тотально корректной, если каждое вычисление S, стартующее в состоянии, в котором выполняется, останавливается и финиширует в состоянии, в котором выполняется.

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

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

Здесь skip – отсутствие операции, x := E – присваивание выражения E переменной x (предполагается, что x и E имеют одинаковый тип), S; S – композиция операторов. Последние два – альтернатива и итерация, соответственно (B – булево выражение).

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

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

В соответствии с аксиомой для присваивания, начинают с постусловия и определяют предусловие подстановкой [x := k]. Эта подстановка означает формулу, в которой во всех вхождениях x заменено на k. Например, Если процесс доказательства начинается с анализа постусловия, то его обычно применяют последовательно к частям программы таким образом, что в конце можно доказать предусловие для всей программы.

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

Правило альтернативы использует булево выражение B, значение которого определяет, что именно исполняется: S1 или S2.

Правило для итерации требует пояснения. Оно определяет, что предикат выполняется после окончания while B do S od, если справедливость может быть поддержана в течение каждого исполнения тела цикла S. Это объясняет, почему называется инвариантом. Одна из основных трудностей в доказательстве правильности программ с помощью рассматриваемого подхода состоит в нахождении подходящих инвариантов. В частности, это усложняет автоматизацию таких доказательств.

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

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

Правило следствия позволяет усиливать предусловия и ослаблять постусловия. При этом оно облегчает применение остальных правил.

В частности, это правило позволяет заменять пред- и постусловия эквивалентными. Тем не менее, следует отметить, что доказательство импликаций вида ' в общем случае неразрешимо.

Теперь обсудим тотальную корректность. Системы доказательств в табл. 1.1 недостаточно для доказательства того, что последовательная программа останавливается. Единственная синтаксическая останавливающимся) вычислениям, – это итерация. Для доказательства наличия останова можно усилить правило вывода для итерации следующим образом:

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

Формальная верификация параллельных систем Пусть для операторов S1 и S2 конструкция S1 || S2 обозначает параллельную композицию этих операторов. Основным для применения формальной верификации к параллельным программам является следующее правило вывода:

Это правило позволяет верифицировать параллельные системы тем же путем, что и последовательные, рассматривая части программ по отдельности. Ввиду взаимодействия между S1 и S2 хотя бы за счет доступа к разделяемым переменным или обмена сообщениями, это правило, к сожалению, в общем случае неверно. Много усилий было приложено к получению правил вывода описанной формы [14].

Существует несколько причин, почему достичь этого непросто.

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

Например, если S1 – это x := x + 2, S2 – это x := x + 1; x := x + 1 и S3 – это x := 0, значение x после выполнения S1 || S3 может быть 0 или 2, а значение x после выполнения S2 || S3 может быть 0, 1 или 2. Различные значения для x зависят от порядка выполнения операторов в S1 и S или S2 и S3. Более того, несмотря на то, что входное-выходное поведение S1 и S2 идентично (увеличение x на 2), нет никакой гарантии, что это будет верно в параллельном контексте.

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

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

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

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

не может быть сформулировано в терминах пред- и постусловий.

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

U (until) и G (globally) – это примеры операторов, которые относятся к последовательностям состояний (таким как, например, вычисления).

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

Иначе говоря, если сообщение m послано процессом P, то этот процесс не передаст следующее сообщение nxt(m), пока не получит подтверждение.

Логики, расширенные операторами, которые позволяют выражать свойства о вычислениях (в частности, которые могут выражать свойства о взаимном порядке между событиями), называются темпоральными логиками. Эти логики в информатику ввел А. Пнуэли [15, 16]. Темпоральные логики – это широко используемый метод спецификации для выражения свойств вычислений реактивных систем на довольно высоком уровне абстракции.

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

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

Основная идея метода, который называется проверкой моделей (model checking) [1, 17, 18], состоит в запуске алгоритмов, исполняемых компьютером, для проверки корректности систем.

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

Если ошибка найдена, инструментальное средство (верификатор) предоставляет контрпример, показывающий при каких обстоятельствах ошибка может быть обнаружена. Контрпример представляет собой сценарий, в котором модель ведет себя нежелательным образом. Он свидетельствует о том, что модель неверна и должна быть исправлена1. Это позволяет пользователю обнаружить ошибку и исправить спецификацию модели перед тем, как продолжить верификацию. Если ни одной ошибки не найдено, то верификация может быть закончена или пользователь может уточнить модель (приняв во внимание больше проектных решений, так что модель становится более конкретной и реалистичной) и повторить процесс верификации. Схема проверки моделей приведена на рис. 1.3.

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

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

Протоколы моделируются множествами конечных автоматов, которые взаимодействуют путем асинхронного обмена сообщениями [19].

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

Методы проверки моделей Известны два подхода в проверке моделей, которые различаются в отношении того, как описывается желаемое поведение – спецификация требований:

Логический или разнородный подход. В этом случае желаемое поведение системы описывается путем формулировки множества свойств в подходящей логике (темпоральной или модальной).

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

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

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

Система считается корректной, если желаемое и возможное поведение эквивалентны (или упорядочены) по отношению к исследуемой эквивалентности (или предпорядку).

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

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

В данной книге используется логический подход [20]. Так как по существу здесь проверяется, что описание системы является моделью формул темпоральной логики, этот логический подход первоначально и назывался проверкой моделей.

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

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

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

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

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

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

Надежный математический фундамент: моделирование, семантика, логика и теория автоматов, структуры данных, алгоритмы на графах.

Ограничения проверки моделей Главные ограничения проверки моделей:

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

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

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

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

Проверка моделей не позволяет проверять обобщения [21]. Если, например, протокол верифицирован для одного, двух и трех процессов с использованием проверки моделей, это не дает никакого результата для другого числа процессов – проверка моделей практична только для частных случаев. Проверка моделей может, однако, помочь сформулировать теоремы с произвольными параметрами, которые впоследствии могут быть доказаны с использованием формальной верификации.

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

Поскольку в проверке моделей основная идея состоит в описании поведения системы конечными автоматами, при определенных условиях число состояний может выйти за пределы размеров доступной памяти. Это, в частности, может быть для параллельных и распределенных систем, у которых много системных состояний – размер множества состояний таких систем в худшем случае пропорционален произведению размеров множеств состояний индивидуальных компонент. Проблема чрезмерного увеличения числа состояний называется проблемой комбинаторного взрыва [17]. Как будет показано ниже, использование автоматного программирования [2] позволяет взглянуть на указанную проблему с другой точки зрения.

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

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

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

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

Логика, используемая программами доказательства теорем и программами проверки доказательств, обычно является вариантом логики предикатов первого порядка. В этой логике имеется неограниченное множество переменных, множества функциональных и предикатных символов заданной арности. Арность означает число аргументов функционального или предикатного символа. Терм – это переменная или строка вида f(t1, …, tn), где f – функциональный символ арности n и ti – термы. Константы могут быть рассмотрены как функции арности 0. Предикат имеет форму P(t1, …, tn), где P – предикатный символ арности n, а ti – термы. Предложения в логике первого порядка – это предикаты, логические комбинации предложений или предложения, снабженные квантификацией существования или всеобщности. В типизированной логике существует также множество типов, и каждая переменная имеет тип (как программная переменная x имеет тип int). Каждый функциональный символ имеет множество типов аргументов и тип результата, а каждый предикатный символ имеет множество типов аргументов, однако не имеет типа результата. По этой причине в такой логике квантификации также типизированы.

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

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

Наконец, программы автоматического доказательства теорем не очень полезны на практике: проблема доказательства теорем экспоненциально сложна – предложение длины n может иметь доказательство экспоненциального размера от n. Поиск такого доказательства требует времени экспоненциального от его длины.

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

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

Перечислим различия между доказательством теорем и проверкой моделей:

Проверка моделей полностью автоматическая и быстрая.

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

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

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

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

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

При использовании проверки моделей, проект проверяется для фиксированного (и конечного) множества параметров. Применение программ доказательства теорем возможно для произвольных значений параметров.

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

Глава 2. Математический аппарат Как следует из названия, метод верификации моделей работает не напрямую с программой, а с ее моделью. В этом разделе описано, как строить такую модель.

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

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

Работу реактивной системы при этом можно представить в виде переходов между состояниями.

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

Сначала введем понятие множество атомарных предложений (элементарных высказываний) – предложений, внутренняя структура которых не может изменяться. Атомарные предложения – это базовые предложения, которые могут быть сделаны. Множество атомарных предложений обозначается AP. Примерами атомарных предложений являются предложения «x больше 0» или «x равно 1» для некоторой переменной x. Другими примерами таких предложений являются «идет дождь» или «в магазине нет покупателей». В принципе, атомарные предложения определяются над множеством переменных x, y, …, констант 0, 1, 2, …, функций max, gcd, … и предикатов x = 2, x mod 2 = 0, …; допускаются предложения вида max(x, y) 3 или x = y.

Не будем точно определять множество AP, а просто постулируем его существование.

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

Моделью Крипке (структурой Крипке) над множеством атомарных предложений AP называется тройка (S, R, Label), где S – непустое множество состояний;

R S S – тотальное отношение переходов на S, которое сопоставляет элементу s S его возможных потомков;

Label: S 2AP сопоставляет каждому состоянию s S атомарные предложения Label(s), которые верны в s.

Отношение R S S называется тотальным, если оно ставит в соответствие каждому состоянию s S как минимум одного потомка (s S: s' S: (s, s' ) R).

Иногда еще требуют, чтобы для модели Крипке был задан набор начальных состояний S0 S.

Путь в модели Крипке из состояния s0 – это бесконечная последовательность состояний = s0 s1 s2 …, такая что для всех i выполняется R(si, si +1).

Представления первого порядка Опишем, как можно представить модель Крипке при помощи логики предикатов первого порядка.

Пусть V = {v1, v2, …, vn} – это множество всех переменных рассматриваемой системы. Поскольку model checking не работает с системами с бесконечным числом состояний, предположим, что переменные системы принимают значения из некоего конечного множества D.

Оценкой для V назовем функцию, которая каждой переменной v из V сопоставляет значение из множества D. Состояние системы описывается мгновенными значениями всех ее переменных, и поэтому состояние является просто оценкой s: V D. Состояние можно описать в виде формулы, которая принимает истинное значение, когда значения переменных соответствуют этому состоянию.

Например, пусть V = {v1, v2, v3}, D = {1, 2, 3} и состояние s соответствует оценке (v1 = 1, v2 = 2, v3 = 3). Тогда это состояние можно описать в виде следующей формулы: (v1 = 1) (v2 = 2) (v3 = 3). При помощи оператора дизъюнкции можно соединить несколько формул для состояний и получить формулу, описывающую набор состояний:

такая формула будет принимать истинное значение только в том случае, если значения переменных соответствуют одному из выбранных состояний. Таким образом, набор начальных состояний может быть описан в виде формулы первого порядка S0(v1, v2, …, vn).

Опишем теперь переходы в виде формул первого порядка. Для этого понадобится дополнительное множество переменных V' = {v'1, v'2, …, v'n}. Будем называть переменные v – переменными текущего состояния, а переменные v' – переменными следующего состояния. Переходом назовем пару оценок V и V'. Тогда можно написать формулу первого порядка R(V, V' ), которая принимает истинные значения тогда и только тогда, когда оценки V и V' соответствуют существующему переходу в системе.

Атомарные высказывания о системе можно задавать как высказывания относительно значений переменных системы.

Высказывание v = d истинно в состоянии s системы, если s(v) = d.

Теперь можно описать модель Крипке в виде формул логики предикатов первого порядка.

1. Множество состояний модели Крипке – множество всех оценок 2. Множество начальных состояний модели Крипке – множество таких оценок s: V D, для которых формула первого порядка S0(s) принимает истинное значение.

3. Отношение переходов задается следующим образом. Переход между оценками s1 и s2 существует тогда и только тогда, когда формула первого порядка R(s1, s2) принимает истинное значение.

Для того чтобы обеспечить тотальность отношения, для всех состояний sk, из которых нет ни одного перехода в другое состояние, введем переход в само это состояние: R(sk, sk) = true.

4. Label: S 2AP определяется так, чтобы Label(s) принадлежали все атомарные предложения, выполняющиеся в состоянии s.

Например, если s(vk) = dk, то атомарное высказывание (vk = dk) Label(s).

Рассмотрим пример построения модели Крипке на основе формул логики предикатов первого порядка, который приведен в книге [17].

Пусть в системе имеются две переменные x и y, принимающие значения из множества D = {0, 1}, и пусть переход в системе задается формулой x := x + y (mod 2). В начальном состоянии значения этих переменных равны единице.

Тогда формула для начального состояния принимает вид:

а формула для переходов:

При этом модель Крипке описывается следующими формулами:

1. S = {0, 1} {0, 1};

2. S0 = {(1, 1)};

3. R = {((0, 0), (0, 0)); ((0, 1), (1, 1)); ((1, 0), (1, 0)); ((1, 1), (0, 1))};

4. L((0, 0)) = {x = 0, y = 0}, L((0, 1)) = {x = 0, y = 1}, L((1, 0)) = {x = 1, y = 0}, L((1, 1)) = {x = 1, y = 1}.

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

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

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

Для пояснения приведем пример из книги [17]. Рассматривается система с двумя переменными x, y и двумя переходами и, которые могут выполняться параллельно:

В начальном состоянии x = 1 y = 2. Рассмотрим более детальную реализацию переходов и, в которой используются команды ассемблера:

Если в программе выполняется сначала переход, а затем переход, то программа попадает в состояние x = 3 y = 5. Если переходы выполняются в обратном порядке, то программа попадает в состояние x = 4 y = 3. Если же переходы совмещаются в следующем порядке:

0, 0, 1, 1, 2, 2,, то в результате программа попадет в состояние Пусть состояние x = 3 y = 3 является ошибочным для системы, и требуется проверить, может ли система оказаться в этом состоянии.

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

Пусть теперь, программа реализована детально, и возможно выполнение последовательности 0, 0, 1, 1, 2, 2. Тогда программа неверна, поскольку может попасть в ошибочное состояние. Однако если построить модель Крипке с использованием лишь переходов и, то верификация покажет, что программа верна, но это будет неправильным результатом.

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

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

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

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

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

Несмотря на неформальность, эта классификация довольно полезна:

два типа свойств почти дизъюнктны, и большинство свойств может быть описано комбинацией свойств безопасности и живучести.

Впоследствии некоторые авторы расширили эту классификацию другими свойствами.

Для того чтобы точно описывать эти типы свойств, были определены логические формализмы. Наиболее широко известными являются темпоральные логики, которые описывают спецификации систем [15].

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

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

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

Изложение теоретических вопросов и примеров проверки моделей для темпоральных логик основано на курсе лекций П. Катоена [1].

Следующее определение устанавливает множество базовых формул, которые могут быть выражены в пропозициональной линейной темпоральной логике (LTL – linear temporal logic).

Пусть AP – множество атомарных предложений. Тогда:

1. p является формулой для всех p AP.

2. Если – формула, то – формула.

3. Если и – формулы, то – формула.

4. Если – формула, то X – формула.

5. Если и – формулы, то U – формула.

Множество формул, построенных в соответствии с этими правилами, называется формулами LTL.

Заметим, что множество формул, полученных на основе первых трех пунктов, определяет множество всех формул пропозициональной логики. Пропозициональная логика является, таким образом, собственным подмножеством LTL. Темпоральными операторами являются только X (neXt) и U (Until).

Синтаксис LTL может быть задан и в нотации Бэкуса-Наура. Для p AP множество LTL-формул определяется следующим образом:

Для логических операторов (конъюнкция), (импликация) и (эквиваленция) справедливы соотношения:

Формула true равна, а false – это true. Темпоральные операторы G (Globally, «всегда») и F (Future, «когда-нибудь») определяются следующим образом:

Так как true верно во всех состояниях, формула F в действительности означает, что выполняется в какой-то момент в будущем. Предположим, что нет момента в будущем, когда выполняется. Тогда выполняется все время. Это объясняет определение G. В литературе F иногда обозначается как, а G как В данной книге используется традиционная нотация F и G.

Итак, можно утверждать, что формула без темпорального оператора (X, F, G, U) на «верхнем уровне» относится к текущему состоянию, формула X – к следующему состоянию, G – ко всем будущим состояниям, F – к некоторому будущему состоянию, а U – ко всем будущим состояниям до тех пор, пока определенное условие не станет верным.

Для уменьшения числа скобок приоритет на темпоральных операторах вводится следующим образом. Как обычно, унарные операции имеют более высокий приоритет, чем бинарные. Например, пишется U F вместо () U (F ). Темпоральный оператор U имеет более высокий приоритет по сравнению с, и, а импликация имеет более низкий приоритет по сравнению с и.

Например, может быть записано следующим образом:

Пример. Пусть AP = {x = 1, x < 2, x 3} – множество атомарных предложений. Примерами LTL-формул являются X(x = 1), (x < 2), x < 2 x = 1, (x < 2) U (x 3), F(x < 2) и G(x = 1). Вторая и третья формула также являются пропозициональными формулами. Пример LTL-формулы с вложенными темпоральными операторами:

G[(x < 2) U (x 3)].

Приведенное выше определение дает способ построения LTL-формул, но не дает интерпретаций этим операторам. Формально LTL интерпретируется на последовательностях состояний. Интуитивно X означает, что верно в следующем состоянии, F – что становится верным впоследствии (сейчас или в какой-то момент в будущем).

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

LTL-модель – это тройка M = (S, R, Label), в которой:

S – непустое конечное множество состояний;

R: S S сопоставляет элементу s S единственный следующий за ним элемент R(s);

Label: S 2AP сопоставляет каждому состоянию s S атомарные предложения Label(s), которые верны в s.

Для состояния s S состояние R(s) – единственное состояние, следующее за s. Важной характеристикой функции R является то, что она работает как генератор бесконечных последовательностей s, R(s), R(R(s)), R(R(R(s))), … Последовательности состояний для семантики LTL являются краеугольным камнем. Можно с тем же успехом определить LTL-модель как структуру (S,, Label), где – бесконечная последовательность состояний, а S и Label определены, как это сделано выше.

Функция Label указывает, какие атомарные предложения верны для заданного состояния M. Если для состояния s имеем Label(s) =, то это означает, что ни одно атомарное предложение не верно в состоянии s. Состояние s, в котором предложение p верно (p Label(s)), иногда называется p-состоянием.

Пример. Пусть AP = {x = 0, x = 1, x 0} – множество атомарных предложений, S = {s0, …, s3} – множество состояний, R(si) = si +1 для 0 i < 3 и R(s3) = s3 – функция следования и Label(s0) = {x 0}, Label(s1) = Label(s2) = {x = 0}, Label(s3) = {x = 1, x 0} – функция, сопоставляющая атомарные предложения состояниям. В модели M = (S, R, Label) атомарное предложение «x = 0» верно в состояниях s1 и s2, «x 0» верно в s0 и s3, а «x = 1» верно только в состоянии s3.

Заметим, что атомарное предложение может либо выполняться, либо не выполняться в любом состоянии модели M. Дальнейшая интерпретация не дается. Например, если «x = 1» верно в состоянии s, это не означает, что «x 0» также верно в этом состоянии. Технически это следует из того факта, что на пометки состояний атомарными предложениями Label не накладывается никаких ограничений.

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

(M, s, ) обозначается в инфиксной нотации: M, s. Идея заключается в том, что M, s тогда и только тогда, когда верно в состоянии s модели M. Когда модель M ясна из контекста, будем опускать модель и писать s вместо M, s.

Семантика LTL определяется следующим образом. Пусть p AP – атомарное предложение, M = (S, R, Label) – LTL-модель, s S и, – LTL-формулы. Отношение выполняемости задается таким способом:

Здесь R0(s) = s и R n +1(s) = R(R n (s)) для любого n 0.

Если R(s) = s', то состояние s' называется прямым потомком s. Если R n (s) = s' для n 1, то состояние s' называется потомком s. Если M, s, то говорят, что модель M удовлетворяет формуле в состоянии s. Иначе говоря, формула выполняется в состоянии s модели M.

Формальная интерпретация остальных связок true, false,,, G и F может быть получена теперь из определений непосредственной подстановкой. Связка true верна во всех состояниях: так как true = p p, выполнимость true в состоянии s сводится к формуле p Label(s) p Label(s), которая является верным предложением для всех состояний s. Таким образом, M, s true для всех состояний s. В качестве примера рассмотрим семантику F :

{ по определению F } { семантика U } { вычисления } Следовательно, F верно в состоянии s, если и только если есть некоторый (не обязательно прямой) потомок состояния s или само состояние s, в котором верно.

Используя этот результат для F, получим семантику для G :

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

Пример. Если формула U верна в состоянии s, то F тоже верно в этом состоянии. Следовательно, когда утверждается U, неявно подразумевается, что в будущем существует какое-то состояние, в котором выполняется. Более слабый вариант оператора Until, оператор Weak until (unless) W утверждает, что выполняется непрерывно либо до момента, когда впервые будет выполняться, либо в течение всей последовательности. Оператор W определяется следующим образом:

Оператор U можно выразить через W двойственным способом:

Пример. Пусть M задается последовательностью состояний, изображенной в первом ряду рис. 2.1. Состояния обозначаются вершинами, а функция R – стрелками (стрелка идет из s в s', если и только если R(s) = s' ). Так как R – тотальная (всюду определенная) функция, у каждого состояния есть ровно одна исходящая стрелка.

Пометки Label указаны под состояниями.

Рис. 2.1. Примеры интерпретации LTL-формул В нижних рядах показана выполнимость трех формул: F p, G p и q U p. Состояние отмечено черным цветом, если формула верна в этом состоянии, и белым – в противном случае. Формула F p верна во всех состояниях, кроме последнего. Ни одно p-состояние не может быть достигнуто из последнего. Формула G p неверна во всех состояниях, так как нет ни одного состояния, потомками которого были бы только p-состояния. Из всех q-состояний (единственное) p-состояние может быть достигнуто за нуль или более шагов. Следовательно, во всех этих состояниях выполняется формула q U p.

Пример. Пусть M задается последовательностью состояний, изображенной на рис. 2.2, где p, q, r, s, t – атомарные предложения.

Рассмотрим формулу X[r (q U s)], которую запишем в виде X[r (q U s)]. Для всех состояний, прямой потомок которых не удовлетворяет r, формула верна ввиду первого дизъюнкта. Это применимо ко второму состоянию. В третьем состоянии формула неверна, так как r выполняется в его потомке, а q и s – нет. Наконец, в первом и четвертом состояниях формула верна, так как в их прямом потомке верно q, а в следующем состоянии верно s, и поэтому q U s верно в их прямом потомке. Справедливость формул G p, F t, GF r и формулы X[r (q U s)] указана в рядах ниже модели M.

Рис. 2.2. Другие примеры интерпретации LTL-формул Опишем теперь некоторые часто используемые предложения логики LTL и приведем их словесную интерпретацию, такую что M, s.

Семантика последнего выражения: выполняется в состоянии s модели M.

1. F : если вначале (то есть в s), то когда-нибудь.

2. G[ F ]: если, то когда-нибудь (для всех потомков s, включая само s).

3. GF : выполняется бесконечно часто.

4. FG : начиная с какого-то момента, выполняется всегда.

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

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

Задача выполнимости может быть сформулирована так:

При этом отметим, что если для проверки моделей заданы модель M и состояние s, то в задаче выполнимости это не так. Для LTL задача выполнимости разрешима. Поэтому и более простая задача проверки моделей для LTL также разрешима. Выполнимость относится к валидации систем с использованием формальной верификации. В качестве примера рассмотрим спецификацию системы и ее реализацию, которые сформулированы в виде LTL-формул и.

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

Сходная задача, часто встречающаяся в литературе – задача тавтологичности:

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

Следовательно, задача тавтологичности для формулы совпадает с отрицанием задачи выполнимости для формулы.

использованием семантики, как описано выше. Это обычно громоздкая задача, так как приходится рассуждать о формальной семантике, которая определена в терминах модели M. В качестве примера попробуем вывести, что U [ X( U )].

Интуитивно эта формула верна: если в текущем состоянии выполняется, то выполняется и U (для произвольной ), так как может быть достигнуто через путь длины 0. В противном случае, если выполняется в текущем состоянии, а в следующем состоянии выполняется U, то U выполняется в текущем состоянии. В результате получаем следующий вывод:

{ семантика и } { семантика X } { семантика U } { вычисления с использованием R n +1(s) = R n (R(s)) } { вычисления с использованием R0(s) = s } { вычисления с использованием R0(s) = s } { вычисления } { семантика U } Как можно видеть из этих вычислений, манипуляция формулами трудоемка и ненадежна. Более эффективный путь проверять правильность формул – это использовать их синтаксис вместо их семантики. Идея состоит в определении множества правил вывода, которые позволяют переписывать LTL-формулы в семантически эквивалентные LTL-формулы на синтаксическом уровне.

Если, например, – это правило (аксиома), то s тогда и только тогда, когда s для всех моделей M и состояний s.

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

В этом разделе приводятся несколько удобных базовых правил.

Правила, перечисленные ниже, сгруппированы, и каждой группе дано имя. С использованием правил идемпотентности и поглощения, любая непустая последовательность F и G может быть сокращена до F, G, FG или GF. Справедливость этих правил вывода может быть доказана и путем использования семантической интерпретации, как было видно ранее для первого закона расширения. Разница в том, что эти громоздкие доказательства требуется провести только однажды, а после этого правила могут применяться повсеместно. Отметим, что справедливость правил расширения для F и G следует непосредственно из справедливости правила расширения для U по определению операторов F и G.

Аксиоматическое правило называется корректным, если оно выполняется. Формально, аксиома называется корректной, если и только если для всех моделей M и состояний s в M:

M, s тогда и только тогда, когда M, s.

Правила двойственности:

Правила идемпотентности:

Правила поглощения:

Правило коммутирования:

Правила расширения:

Применение корректных аксиом к заданной формуле означает, что справедливость формулы не изменяется: аксиомы не изменяют семантику формулы. Если для любых семантически эквивалентных и эту эквивалентность возможно вывести, используя аксиомы, то аксиоматизацию называют полной. Приведенная аксиоматизация для LTL является корректной и полной [22].

Строгая и нестрогая интерпретации. G означает, что выполняется во всех состояниях, включая текущее. Это называется нестрогой интерпретацией, так как формула также ссылается на текущее состояние. В отличие от нее, строгая интерпретация не ссылается на текущее состояние. Строгая интерпретация G, обозначаемая G, определяется как G XG. Следовательно, G означает, что выполняется для всех состояний-потомков, не говоря ничего о текущем состоянии. Аналогично, строгие варианты F и U определяются как F XF и U X( U ). (Отметим, что для X нет смысла различать строгую и нестрогую интерпретации). Эти определения показывают, что строгая интерпретация может быть определена в терминах нестрогой интерпретации. В обратную сторону имеем:

Первые два равенства следуют из данных выше определений G и F.

Третье равенство подтверждается правилом расширения из предыдущего раздела: если подставить U X( U ) в третье равенство, то получим правило расширения для U. Несмотря на то, что иногда используется строгая интерпретация, более распространена нестрогая, которая и рассматривается в этой книге.

Операторы предшествования. Все операторы ссылаются на будущее, включая текущее состояние. Как следствие, эти операторы известны как операторы будущего. Иногда LTL расширяется операторами предшествования. Это может быть полезно в некоторых приложениях, так как иногда свойства легче выражаются в терминах прошлого, чем в терминах будущего. Например, G («всегда в прошлом») означает (в нестрогой интерпретации), что выполняется сейчас и в любом состоянии ранее. F («когда-нибудь в прошлом») – выполняется в текущем состоянии или в некотором состоянии ранее, а X означает, что выполняется в предыдущем состоянии, если такое состояние существует. Как и для операторов будущего, для операторов предшествования могут быть даны строгая и нестрогая интерпретации. Основная причина введения операторов предшествования состоит в упрощении записи спецификации.

При этом отметим, что выразительная сила LTL не увеличивается при добавлении операторов предшествования2 [23].

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

Коммуникационный канал Рассмотрим однонаправленный канал между двумя сообщающимися процессами: отправителем (S) и получателем (R). Отправитель снабжен выходным буфером (S.out), а получатель – входным. Оба буфера имеют неограниченную емкость. Если S посылает сообщение m к R, то он помещает сообщение в свой выходной буфер S.out.

Выходной буфер S.out и входной буфер R.in соединены однонаправленным каналом. Получатель принимает сообщения путем удаления их из своего входного буфера R.in. Считаем, что все сообщения одинаково идентифицированы, а множество атомарных предложений AP = {m S.out, m R.in}, где m обозначает сообщение.

При этом неявно предполагается, что все свойства формулируются для любого сообщения m (предполагается универсальная квантификация по m). Это делается для удобства и не повлияет на Если в качестве базовой семантической идеи взята дискретная модель, как в данном разделе.

разрешимость задачи выполнимости, если предположить, что число сообщений конечно. Кроме того, будем считать, что буферы S.out и R.in ведут себя нормально – не «портят» и не теряют сообщения, и сообщение не может находиться в буфере бесконечно долго. Схема взаимодействия отправителя и получателя приведена на рис. 2.3.

Рис. 2.3. Взаимодействие отправителя и получателя Формализуем следующие неформальные требования к каналу с помощью LTL:

«Сообщение не может быть в обоих буферах одновременно»:

«Канал не теряет сообщения». Если канал не теряет сообщения, то это означает, что сообщения, помещенные в S.out, в конечном счете будут доставлены в R.in:

G(m S.out F(m R.in)).

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

G(m S.out XF(m R.in)), так как m не может быть в S.out и R.in одновременно.

«Канал сохраняет порядок». Это означает, что если m, а затем m' передано отправителем в его выходной буфер S.out, то m будет принято получателем перед m':

Отметим, что в предпосылке конъюнкт m' S.out требуется для того, чтобы специфицировать, что m' отправлено в S.out после m.

F(m' S.out) само по себе не исключает, что m' в буфере отправителя, когда m в S.out.

Канал не генерирует сообщения спонтанно. Это означает, что любое m в R.in должно быть заранее послано отправителем S.

С использованием оператора предшествования F это может быть удобно формализовано следующим образом:

G[(m R.in) F(m S.out)].

При отсутствии операторов предшествования можно использовать оператор U:

G[(m R.in)U(m S.out)].

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

Предположим, что имеется конечное число процессов, соединенных некоторыми коммуникационными средствами. Коммуникация между процессами асинхронна, как в предыдущем примере. Схематично это изображено на рис. 2.4.

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

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

Рассмотрим множество атомарных предложений:

где leaderi означает, что процесс i является лидером, activei – что процесс i активен, а i < j – что идентификатор i меньше, чем идентификатор j (в линейном порядке идентификаторов). Используем i и j в качестве идентификаторов процессов, а через N обозначим число процессов. Будем считать, что неактивный процесс не является лидером.

В дальнейших формулировках используем универсальную и экзистенциальную квантификацию по множеству идентификаторов.

Строго говоря, кванторы не является частью LTL. Так как в данном случае рассматривается конечное число процессов, универсальная квантификация i: P(i) (где P – некоторое предложение о процессах) может быть расширена до P(1) … P(N). Так же может быть расширено i: P(i). Квантификация в данном случае может быть рассмотрена как сокращение:

«Всегда имеется ровно один лидер»:

G[i: leaderi (j i: leaderj)] Так как в данном случае работаем с динамической системой, в которой все процессы могут быть первоначально неактивны (следовательно, нет и лидера), то это свойство, вообще говоря, неверно. Также в распределенной системе с асинхронной коммуникацией переключение от одного лидера к другому с трудом может быть сделано атомарным, и удобно разрешить временное отсутствие лидера. В качестве первой попытки можно GF[i: leaderi (j i: leaderj)], которая разрешает временное отсутствие лидера, но разрешает также на время иметь нескольких лидеров одновременно. С точки зрения логичности это нежелательно. Поэтому рассмотрим следующие два свойства.

«Всегда имеется максимум один лидер»:

G[leaderi j i: leaderj] «В свое время будет достаточно лидеров». (Это требование избегает конструкции протокола выбора лидера, который никогда не выбирает лидера. Такой протокол удовлетворяет предыдущему требованию, но он не желателен):

GF[i: leaderi] Это свойство не означает, что будет бесконечно много лидеров.

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

«В присутствии активного процесса с более высоким идентификатором лидер в какой-то момент уступит»:

G[i, j: ((leaderi i < j leaderj activej) F leaderi)].

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

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

G[i, j: (leaderi X leaderi XF leaderj) i < j].

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

Другие примеры спецификации темпоральных свойств приведены в работе [24].

Задача проверки моделей для линейной темпоральной логики формулируется в терминах моделей Крипке.

Каждый путь в модели Крипке, начинающийся с состояния s0, представляет собой LTL-модель. Задача проверки LTL-формулы для модели Крипке состоит в том, чтобы определить, на всех ли путях выполняется данная формула (или, что то же самое, существуют ли пути, на которых формула не выполняется).