«Методы реализации автоматных объектно-ориентированных программ ...»

Санкт-Петербургский государственный университет информационных

технологий, механики и оптики

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

Степанов Олег Георгиевич

Методы реализации автоматных

объектно-ориентированных программ

Специальность 05.13.11. Математическое и программное обеспечение

вычислительных машин, комплексов и компьютерных сетей

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель – доктор технических наук, профессор А.А. Шалыто Санкт-Петербург 2009

ОГЛАВЛЕНИЕ

ОГЛАВЛЕНИЕ

ВВЕДЕНИЕ

ГЛАВА 1. МЕТОДЫ РЕАЛИЗАЦИИ ОБЪЕКТНООРИЕНТИРОВАННЫХ И АВТОМАТНЫХ ПРОГРАММ

Структура объектно-ориентированных программ

1.1.

Методы повышения качества объектно-ориентированных 1.2.

программ

Автоматное объектно-ориентированное программирование.. 1.3.

Методы повышения качества автоматных объектноориентированных программ

Выводы по главе 1

ГЛАВА 2. ФОРМАЛИЗАЦИЯ ТРЕБОВАНИЙ К АВТОМАТНЫМ

ОБЪЕКТНО-ОРИЕНТИРОВАННЫМ ПРОГРАММАМ

Формализация требований к автоматным программам........... 2.1.

Интерфейсы автоматных объектов

2.2.

Автоматное программирование по контрактам

2.3.

Способы проверки автоматных контрактов

2.4.

Динамический метод проверки спецификаций автоматных 2.5.

программ

Формализация требований к автоматным программам........... 2.6.

Выводы по главе 2

ГЛАВА 3. ВНЕСЕНИЕ ИЗМЕНЕНИЙ В АВТОМАТНЫЕ ПРОГРАММЫ..

Внесение изменений в автоматные программы

3.1.

Классификация изменений автоматных программ

3.2.

Описание базовых изменений автоматов

3.3.

3.3.1. Добавление состояния

3.3.2. Удаление состояния

3.3.3. Установка начального состояния

3.3.4. Снятие начального состояния

3.3.5. Добавление конечного состояния

3.3.6. Удаление конечного состояния

3.3.7. Добавление перехода

3.3.8. Изменение события на переходе

3.3.9. Изменение условия на переходе

3.3.10. Удаление перехода

3.3.11. Перемещение перехода

Рефакторинг автоматных программ

3.4.

3.4.1. Группировка состояний

3.4.2. Удаление группы состояний

3.4.3. Слияние состояний

3.4.4. Выделение автомата

3.4.5. Встраивание вызываемого автомата

3.4.6. Переименование состояния

3.4.7. Перемещение воздействия из состояния в переходы........... 3.4.8. Перемещение воздействия из переходов в состояние.......... Метод внесения изменений в автоматные программы............. Пример использования метода

Выводы по главе 3

ГЛАВА 4. ИНТЕГРАЦИЯ СПЕЦИФИКАЦИИ И КОДА АВТОМАТНЫХ

ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ

Автоматное программирование в динамических языках......... 4.1.1. Определение общих свойств автомата

4.1.2. Описание графов переходов

4.1.3. Пример декларации автомата

4.1.4. Использование библиотеки

4.1.5. Реализация библиотеки

4.1.6. Отладка программ

4.1.7. Взаимодействие с окружением

4.1.8. Формализация спецификаций автоматов

Интеграция спецификации и кода в мультиязыковых средах 4.2.1. Описание языков в системе JetBrains MPS

4.2.2. Автоматное программирование в среде JetBrains MPS...... 4.2.3. Язык спецификации автоматов

4.2.4. Реализация языка спецификации автоматов

4.2.5. Пример использования языка спецификации автоматов... Выводы по главе 4

ГЛАВА 5. ВНЕДРЕНИЕ РЕЗУЛЬТАТОВ РАБОТЫ В ПРАКТИКУ

РАЗРАБОТКИ ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ........... Область внедрения

YouTrack

Автомат управления списком дефектов IssueList.js................ Автомат управления выпадающей подсказкой Suggest.js...... Выводы по главе 5

ЗАКЛЮЧЕНИЕ

ИСТОЧНИКИ

ВВЕДЕНИЕ

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

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

Тестирование не может дать гарантию отсутствия ошибок в программе.

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

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

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

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

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

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

реализации автоматных объектно-ориентированных программ, позволяющих интегрировать процессы разработки автоматных и объектноориентированных программ.

Основными задачами

исследования является создание:

метода формализации требований к автоматным объектноориентированным программам с использованием контрактов;

метода интеграции спецификации и реализации автоматных объектно-ориентированных программ;

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

каталога рефакторингов.

Методы исследования. В работе использованы методы теории автоматов, верификации, контрактного программирования и объектноориентированного проектирования.

результаты, которые выносятся на защиту:

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

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

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

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

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

диссертации, используются на практике:

в компании ООО «ИнтеллиДжей Лабс» при разработке системы в учебном процессе по курсу «Применение автоматов в информационных технологий, механики и оптики (СПбГУ Апробация диссертации. Основные положения диссертационной работы докладывались на III Межвузовской конференции молодых ученых (СПб., 2006 г.), XXXVI научной и учебно-методической конференции профессорско-преподавательского и научного состава СПбГУ ИТМО ( г.), конференциях Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE) (СПбГУ, 2008 г.), 5th Central and Eastern European Software Engineering Conference in Russia (SECR) (М., 2009 г.).

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

Гранты. Диссертация выполнялась в ходе работы над грантом для студентов, аспирантов вузов и академических институтов, находящихся на территории Санкт-Петербурга, который проводился Администрацией СанктПетербурга (2008 г.). Материалы диссертации используются в научноисследовательской работе по теме «Методы повышения качества при разработке автоматных программ с использованием функциональных и объектно-ориентированных языков программирования», которая победила в конкурсе НК-421П «Проведение научных исследований научными группами под руководством кандидатов наук» по направлению «Информатика», который был объявлен в 2009 году Федеральным агентством по образованию по Федеральной целевой программе «Научные и научно-педагогические кадры инновационной России» на 2009–2013 годы.

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

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

ГЛАВА 1. МЕТОДЫ РЕАЛИЗАЦИИ

ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ И АВТОМАТНЫХ

ПРОГРАММ

1.1. Структура объектно-ориентированных программ Большинство разрабатываемых в настоящее время программ строится на основе объектно-ориентированного подхода. Известны различные методы объектно-ориентированного программирования В настоящей диссертации автор придерживается модели, описанной Б. Мейером в книге [3], основные концепции которой перечислены ниже.

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

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

Объекты. Объекты являются экземплярами неабстрактных классов.

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

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

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

1.2. Методы повышения качества объектно-ориентированных повышения качества используются на всех этапах: от проектирования до внедрения. Эти методы могут быть различны, и направлены на уменьшение числа ошибок как при написании программы, так при ее изменениях.

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

Рассмотрим некоторые из них.

Гибкие методологии разработки. В настоящее время широкое распространение получили гибкие (agile) методологии разработки ПО (например, XP [6], Scrum [7] и MSF for Agile Software Development Process Такие методологии ориентированы на постепенное уточнение [8]).

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

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

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

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

Хорошие решения в объектно-ориентированных программах фиксируются в виде паттернов [9, 10].

Среди паттернов объектно-ориентированного проектирования, в применении к теме данной диссертации, особое значение представляют следующие [4]:

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

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

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

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

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

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

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

Тестирование. Тестированием программного обеспечения называется процесс выявления в нем ошибок. Важно отметить, что успешное тестирование не может гарантировать отсутствие ошибок в программе («Тестирование программ, – отмечал Эдсгер Дейкстра, – можно использовать для того, чтобы показать наличие ошибок и никогда – для того чтобы показать их отсутствие!»). Существует много видов тестирования программного обеспечения [12]. Ниже рассматриваются несколько основных видов.

При тестировании ПО специалист по качеству может либо учитывать информацию о реализации тестируемого кода (так называемый метод «стеклянного» (glass box) или «белого» (white box) ящика), либо не учитывать – метод «черного ящика» (black box). При использовании метода «черного ящика» выделяют функциональное тестирование, при котором каждая функция программы тестируется путем ввода ее входных данных и анализа противоположность функциональному тестированию для метода «стеклянного ящика» выделяют структурное тестирование, главной идеей которого является правильный выбор тестируемого программного пути. Так как все программные пути протестировать обычно невозможно, специалисты по тестированию выделяют среди них группы, которые требуется протестировать обязательно. Для отбора таких групп применяются специальные критерии, называемые критериями охвата (coverage criteria).

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

Еще одним важным видом тестирования является регрессионное тестирование. Этот вид тестирования направлен на то, чтобы после исправления ошибки в программе проверить следующие два условия:

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

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

В современных проектах по разработке программного обеспечения особое место занимает модульное тестирование (unit testing) [6]. Оно используется для автоматического тестирования отдельных модулей программы. Для каждой нетривиальной функции создается модульный тест, проверяющий основные сценарии работы с ней. При этом используется структурный подход: учитываются критерии охвата модульных тестов [14].

Для запуска и написания таких тестов применяются специальные библиотеки, существующие для всех популярных языков программирования, например, JUnit [15], NUnit [16], PyUnit [17] и тому подобные.

Модульные тесты обычно запускаются программистами после каждого значительного изменения кода или рефакторинга. Удобство и широкая распространенность модульных тестов связаны с тем, что тесты пишутся на том же языке, что и сама программа, а средства запуска таких тестов реализованы во всех популярных интегрированных средах разработки. Часто все модульные тесты в программе запускаются автоматически после каждого внесения изменений. Такой подход называется непрерывной интеграцией (continuous integration) [18].

Программирование по контрактам (design by contract). Этот подход к объектно-ориентированному программированию был предложен Бертраном Мейером [19]. Основной чертой этого подхода является использование утверждений (assertions) – условий, которые должны выполняться, если код программы верен. Утверждения представляют собой булевы выражения и делятся на два типа:

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

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

специальных утверждений:

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

Важным свойством контрактов является их исполнимость. Это значит, что контракты должны проверяться в ходе работы программы. Для этого требуется интегрировать контракты и код программы. Лучше всего такая интеграция осуществляется при использовании языков, поддерживающих программирование по контрактам. На настоящий момент самым распространенным языком программирования с поддержкой контрактов является язык Eiffel [3], в котором программирование по контрактам и было впервые реализовано. Существуют также библиотеки расширений, реализующие полную или частичную поддержку программирования по контрактам в распространенных языках программирования [21, 22]. Однако, так как эти библиотеки не являются частью соответствующего языка, они не получили широкого распространения.

предусматривает три способа использования контрактов:

использовать контракты как неисполнимые комментарии с соответствия реализации программы описанным контрактам не дополнительных языковых конструкций [23];

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

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

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

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

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

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

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

применяются различные автоматные модели [26]. В настоящей работе рассматриваются автоматы, поведение которых описывается графами переходов со следующими свойствами [27, 28]:

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

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

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

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

Выполнение перехода состоит из следующих шагов:

выполняются действия на переходе (вызываются указанные выходные воздействия в порядке их следования);

текущим становится состояние, в котором заканчивается если произошла смена состояния (текущее состояние до начала обработки события отличается от состояния, в котором заканчивается переход), то вызываются действия Заметим, что в вышеизложенном описании отсутствует взаимодействие «автоматизированные объекты управления как классы» [26], которого автор придерживается в настоящей работе, взаимодействие автоматов осуществляется так же, как и взаимодействие автомата и объекта управления:

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

Одной из основных проблем программирования с явным выделением состояний является организация взаимодействия автоматного и неавтоматного кода. В настоящее время разработан ряд подходов [29] к реализации автоматной части объектно-ориентированных программ. Эти подходы можно условно разделить на два класса: статические и динамические.

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

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

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

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

Существующие подходы к программированию с явным выделением недостатков:

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

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

В работе [33] для решения этих проблем предлагается использовать текстовый предметно-ориентированный язык (DSL) stateMachine, реализованный в системе метапрограммирования JetBrains MPS (Meta Programming System) [35, 36]. Этот язык позволяет присоединить автоматную часть в виде аспекта к любому классу в программе. Каждый автомат в языке stateMachine связан с некоторым классом и описывает его поведение. Для того чтобы задать поведение класса с помощью автомата, необходимо в этом классе определить события, на которые будет реагировать автомат.

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

При этом автоматная логика класса остается скрытой даже для неавтоматной части того же класса.

В настоящее время широкое распространение получили динамические объектно-ориентированные языки программирования. Одной из их особенностей является возможность отправить любому объекту в программе произвольное сообщение (в то время как в статических языках набор возможных сообщений определяется абстрактным типом данных объекта [26]). Другой особенностью динамических языков является возможность замены реализаций методов во время работы программы.

Эти особенности в совокупности со спецификой синтаксиса некоторых динамических языков программирования позволяют описывать автоматную часть программ в терминах состояний и переходов между ними. Таким образом, становится возможным разработать автоматный внутренний предметно-ориентированный язык [36]. Одной из первых реализаций такого языка является библиотека STROBE [37] для языка программирования Ruby.

Это направление получило развитие в работе [38], в которой введена поддержка наследования и вложения автоматов.

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

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

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

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

1.4. Методы повышения качества автоматных объектноориентированных программ автоматных объектно-ориентированных программ. С одной стороны, к автоматным классам, являющимся частью объектно-ориентированной программы, могут применяться все методы, описанные в разд. 1.2, а с другой – в автоматном программировании сложилась своя методика обеспечения и повышения качества.

В основе этой методики лежит ряд особенностей автоматных программ:

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

поведение каждого автомата формализовано;

управляющие состояния выделены;

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

Методы анализа автоматных программ можно разделить на два класса:

статические и динамические.

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

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

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

Статическую проверку можно проводить на нескольких уровнях.

Применительно к автоматным программам – это проверка корректности описания автоматов: существование всех использованных идентификаторов переменных, отсутствие переходов «в никуда» и т. д.

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

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

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

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

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

Существует ряд инструментальных средств, выполняющих валидацию автоматных программ, например, UniMod [34, 40].

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

доказательная верификация [41, 42] и верификация на модели [43].

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

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

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

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

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

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

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

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

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

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

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

ГЛАВА 2. ФОРМАЛИЗАЦИЯ ТРЕБОВАНИЙ К

АВТОМАТНЫМ ОБЪЕКТНО-ОРИЕНТИРОВАННЫМ

ПРОГРАММАМ

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

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

Достоинством методов, основанных на тестировании – возможность проверки правильности работы управляющих автоматов совместно с управляемыми объектами.

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

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

термостата не должны превышать допустимые.

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

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

Temporal Logic, LTL) [50]. Формулы этого языка построены на множестве атомарных высказываний (Prop) с применением булевых операторов, унарного темпорального оператора («на следующем шаге») и бинарного темпорального оператора («до тех пор, как»).

Моделью для LTL-формул является вычисление – функция :

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

Также используются темпоральные операторы («всегда») и («в будущем»), которые эквивалентны следующим формулами:

Говорят, что удовлетворяет формуле (обозначается ), если и только если, 1.

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

набор высказываний, которые разрешено использовать в LTLформулах спецификации;

способ построения протокола выполнения автомата;

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

получение события;

вычисление условий на переходах;

выполнение действий на переходе. Одним из таких действий является вызов другого автомата. При выполнении вызова управление передается вызываемому автомату с соответствующим событием. Этот автомат совершает переход по указанному событию и затем возвращает управление вызвавшему автомату;

переход в новое состояние.

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

, : автомат обрабатывает событие ;

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

, : автомат находится в состоянии,.

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

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

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

Автоматным интерфейсом является внешняя информация об автомате:

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

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

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

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

2 : напряжение превысило пределы диапазона допустимых 3 : показания термостатов превысили пределы диапазона 1 : открытие дверцы холодильника.

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

С применением введенных атомарных утверждений первые два пункта требований к программе управления холодильником могут быть записаны следующим образом:

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

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

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

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

2.3. Автоматное программирование по контрактам Целью настоящего раздела является расширение объектноориентированного контрактного программирования на класс автоматных объектно-ориентированных программ. Для демонстрации недостатков существующего подхода к формализации требований рассмотрим еще один пример вербальных требований – к системе управления лифтом, которую обозначим «лифт 1»:

1. Во время движения двери лифта закрыты.

2. Пока двери лифта открыты, свет в кабине включен.

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

1 : включить мотор привода кабины в направлении «вверх»;

2 : включить мотор привода кабины в направлении «вниз»;

3 : остановить мотор привода кабины;

4 : включить механизм открывания дверей;

5 : включить механизм закрывания дверей;

41 : вызов лифта на первый этаж;

42 : вызов лифта на второй этаж;

43 : вызов лифта на третий этаж.

Выделим следующие состояния автомата:

2. «Открывание дверей».

3. «Закрывание дверей».

4. «Ожидание с открытыми дверьми».

5. «Ожидание с закрытыми дверьми».

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

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

Команда о запуске привода кабины выражается формулой 1 2, об остановке привода – формулой 3. Открытие дверей выражается формулой 4, закрытие – формулой 5. Таким образом, эквивалентное утверждение Эта формула достаточно сложна для понимания, поэтому при ее возникновению ошибок.

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

1 ((4 5 ) 4 ). Она значительно проще предыдущей.

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

Второе соотношение делает спецификацию достаточно сложной.

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

Большая часть ошибок при автоматном программировании возникает из-за неточного специфицирования состояний. Разделение требований на части, относящиеся к конкретным состояниям, помогает более четко специфицировать эти состояния. Задача спецификации конкретных состояний автомата аналогична задаче, решаемой контрактами в объектноориентированном программировании, рассмотренными в первой главе.

Напомним, что контракты в объектно-ориентированных программах состояниях, являются контрактами этих состояний.

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

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

Требования для лифта, сформулированные выше, можно представить в виде контрактов. Первое условие является инвариантом 4, второе – предусловием 2 4.

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

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

Например, для выходных воздействий 1 и 2 имеет смысл предусловие 1, которое устанавливает, что при включении привода лифта управляющий автомат должен находиться в состоянии «Движение».

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

Второй пункт требований к автомату управления лифтом («Пока двери лифта открыты, свет в кабине включен») может быть сформулирован как в виде инвариантов 4 для состояний 2 и 4.

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

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

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

2.4. Способы проверки автоматных контрактов Проверка выполнения контрактов может, как и в объектноориентированном программировании, выполняться различными способами – статическим и динамическим.

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

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

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

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

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

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

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

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

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

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

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

Методы динамической верификации рассматривают работу программы на конечном отрезке времени. Поэтому для применения LTL–логики в динамической верификации требуется расширить определение LTL на конечные вычисления, в которых момент времени является значением из отрезка 1,. Это сделано в работе [53].

положительных булевых формул над (булевых формул, построенных из элементов, которые соединены операторами и ) и формул и.

=,, 0,, [54], где – непустой конечный алфавит, – непустое конечное множество состояний, 0 – начальное состояние, – множество принимающих состояний, а : +() – функция перехода.

Запуском альтернирующего автомата Бюхи на бесконечном слове = 0, 1, … называется -помеченное дерево, функцию пометок которого обозначим, такое, что его корень помечен значением 0 и справедливо:

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

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

Можно построить аналог альтернирующего автомата Бюхи для автоматом.

В работе [55] показано, что для любой LTL-формулы можно построить альтернирующий автомат Бюхи такой, что () = (), причем число состояний автомата линейно зависит от размера формулы.

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

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

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

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

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

Третий из предложенных в работе [53] алгоритмов (алгоритм обратного обхода в глубину) похож на обход в глубину, но вместо рекурсивных вызовов использует состояние, уже вычисленное для «хвоста»

протокола.

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

запись отрицания верифицируемой спецификации в виде LTLформул. Это преобразование производится вручную в соответствии с рекомендациями, изложенными в работе [57];

альтернирующего автомата;

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

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

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

Для динамической верификации системы автоматов с использованием предлагаемого метода требуется определить:

набор высказываний, которые разрешено использовать в LTLформулах спецификации;

способ построения протокола выполнения автомата;

правила вычисления значений высказываний в записях протокола.

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

Для пояснения способа построения протокола и правил вычислений значений высказываний будем рассматривать верификацию системы автоматов управления лифтом этим методом. Граф переходов этой системы (назовем ее «лифт 2») представлены на рис. 1.

Рис. 1. Графы переходов автоматов управления лифтом Автомат 1 моделирует поведение лифта ( 1 – «Ожидание, двери закрыты», 2 – «Движение», 3 – «Ожидание, двери открыты»). Автомат моделирует лампу в кабине лифта (1 – «Выключена», 2 – «Включена»).

Когда автомат 1 получает событие 1 («Вызов»), он переходит в состояние 2, в котором он ожидает событие 2 («Прибытие»). При его получении автомат 1 переходит в состояние 3 и вызывает автомат 2 c событием 3, включая тем самым лампу. При получении события 4 («Двери закрыты») автомат 1 пересылает это событие автомату 2, который в ответ выключает лампу.

В качестве спецификации, для которой производится верификация, выберем условие «через некоторое время после вызова у лифта открываются двери». В виде LTL-формулы эта спецификация имеет вид: 1,1 1,3.

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

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

Введем несколько определений. Назовем секцией обработки события автоматом последовательность записей, …,. Заголовком секции назовем начальную подпоследовательность записей длины 1 + :, ….

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

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

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

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

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

Рис. 2. Альтернирующий автомат, соответствующий требованию «После вызова Жирно обведены принимающие состояния, дугой объединены «и»переходы.

По заданному протоколу можно построить принимающий запуск в полученном альтернирующем автомате.

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

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

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

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

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

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

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

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

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

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

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

ГЛАВА 3. ВНЕСЕНИЕ ИЗМЕНЕНИЙ В АВТОМАТНЫЕ

ПРОГРАММЫ

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

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

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

изменения в программе в соответствии с изменившимися исправление ошибок;

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

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

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

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

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

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

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

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

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

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

3.3. Описание базовых изменений автоматов В данном разделе приводится каталог базовых изменений автоматов.

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

При описании каждого базового изменения графа переходов автомата будем придерживаться определенного формата, приведенного ниже:

неформальное описание приводимого изменения;

рекомендации по проведению такого изменения.

3.3.1. Добавление состояния Описание. В граф переходов добавляется новое состояние.

Рекомендации.

Обеспечить достижимость состояния.

3.3.2. Удаление состояния Описание. Из графа переходов удаляется состояние и все связанные с этим состоянием переходы.

Рекомендации.

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

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

Следует также учитывать описанные ниже рекомендации при 3.3.3. Установка начального состояния Описание. Состояние объявляется начальным в автомате.

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

3.3.4. Снятие начального состояния Описание. Начальное состояние объявляется нормальным.

Рекомендации Необходимо объявить начальным другое состояние.

3.3.5. Добавление конечного состояния Нормальное состояние объявляется конечным в автомате.

Рекомендации Если из этого состояния выходили какие-то переходы, то их необходимо удалить (следуя рекомендациям при удалении 3.3.6. Удаление конечного состояния Конечное состояние объявляется нормальным.

Рекомендации Необходимо пересмотреть набор конечных состояний в автомате.

3.3.7. Добавление перехода Описание. Добавление перехода между двумя состояниями. На переходе указывается событие, по которому данный переход осуществляется.

Также может указываться условие и выходное воздействие.

Рекомендации Необходимо проверить полноту и непротиворечивость условий 3.3.8. Изменение события на переходе Описание. Изменяется событие, по которому активизируется переход.

Рекомендации Проверить полноту и непротиворечивость условий на переходах.

3.3.9. Изменение условия на переходе Описание. Изменяется условие, при котором осуществляется переход.

Рекомендации Проверить полноту и непротиворечивость условий на переходах.

3.3.10. Удаление перехода Описание. В автомате удаляется переход.

Рекомендации Проверить полноту и непротиворечивость условий на переходах.

Проверить достижимость состояний.

3.3.11. Перемещение перехода Описание. Переход имеет начальное и конечное состояния. При перемещении перехода возможно:

изменение начального состояния;

изменение конечного состояния.

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

Рекомендации Проверить полноту и непротиворечивость условий на переходах.

Проверить достижимость состояний в автомате.

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

Выбор рефакторингов для каталога основан на наборе экспериментов.

В качестве основы были взяты несколько автоматов, созданных студентами кафедры «Компьютерные технологии» СПбГУ ИТМО в ходе выполнения курсовых работ по курсу «Применение автоматов в программировании» [59].

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

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

Описание каждого рефакторинга имеет следующую структуру:

сначала следует название рефакторинга;

за названием следует неформальное описание изменения;

доказательство корректности рефакторинга.

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

Будем рассматривать последовательность событий 1, 2, …,. При следующих обозначений: – изначальный автомат, ’ – автомат с последовательность состояний, событий и выходных воздействий автомата A последовательность для автомата A' – 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, …, где:

и – выходные воздействия, совершаемые при входе в и – выходные воздействия, совершаемые на переходах Если автоматы и ’ не эквивалентны, то найдется такое > 0, что или. При доказательстве эквивалентности автоматов будем опираться на технику выполнения рефакторинга.

3.4.1. Группировка состояний Описание. Несколько простых состояний объединяются в группу состояний. При этом добавляются групповые переходы, заменяющие одинаковые переходы, исходящие из всех группируемых состояний (рис. 3).

Рис. 3. Пример применения рефакторинга «группировка состояний»

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

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

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

При наступлении события («Выключение лампы в кнопке») в каждом из состояний 1–4 автомат должен перейти в состояние 0. Такое поведение реализуется следующим графом переходов (рис. 4).

автомата (рис. 5).

выполнить следующие действия:

1. Добавить группу, объединяющую состояния 1, 2, …,.

2. Выбрать один переход, исходящий из 1, который требуется 3. Убедиться, что каждое из состояний 2, …, имеет переход с такими же атрибутами, что и (под атрибутами понимаются конечное состояние, событие, условие и выходные воздействия).

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

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

3.4.2. Удаление группы состояний Описание. При удалении группы состояний все исходящие из него переходы добавляются в состояния, находящиеся в группе, после чего сгруппированные состояния выносятся из группы.

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

Для удаления группы, объединяющей состояния 1, 2, …,, необходимо выполнить следующие действия:

1. Выбрать переход, исходящий из группы.

2. Добавить переходы, исходящие из состояний ( = 1.. ), c атрибутами перехода.

3. Удалить переход.

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

3.4.3. Слияние состояний Описание. Несколько состояний с одинаковыми исходящими переходами сливаются в одно состояние. При этом сохраняются переходы, соединяющие эти состояния с другими состояниями автомата.

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

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

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

5. Перегорела лампа в кнопке «1»;

6. Перегорела лампа в кнопке «2»;

7. Перегорела лампа в кнопке «3»;

8. Перегорела лампа в кнопке «S»;

9. Неисправность.

Измененный граф переходов представлен на рис. 6:

Рис. 6. Граф переходов автомата управления лифтом до слияния состояний 5– Граф переходов автомата после слияния состояний 5–8 в одно состояние представлен на рис. 7.

Для слияния состояний 1, 2, …, необходимо выполнить следующие действия:

2. Убедиться, что состояния 1, 2, …, имеют исходящие переходы с одинаковыми атрибутами, и эти переходы заканчиваются в 3. Изменить конечные состояния переходов, которые ведут в Доказательство корректности. Между состояниями автоматов A и A’ строится соответствие :. При этом все сливаемые состояния Начальное состояние автомата A соответствует начальному состоянию автомата A’. Тогда в цепочках элементов 0, 0, 1, 1, 1, 1, 2, 2, 2, соответствуют друг другу: 1 = 1 и 0 = 0.

Докажем, что если в цепочках совпадают первые t (t > 0) элементов, то (t+1)-е элементы также совпадают. Другими словами, если выполняется:

+1 = +1, +1 = +1, +1 = +1. Состояние может входить или не входить в множество сливаемых состояний (1, 2, …, ). Рассмотрим оба случая:

1) не входит в множество сливаемых состояний:

a) +1 входит в множество сливаемых состояний 1, 2, …,. Тогда b) +1 не входит в множество сливаемых состояний 1, 2, …,.

соответствующий переход и состояние не претерпевали никаких 2) входит в множество сливаемых состояний:

a) +1 также входит в множество сливаемых состояний 1, 2, …,.

рассматриваемого рефакторинга), +1 = +1 (см. п. 1 техники).

b) +1 не входит в множество сливаемых состояний 1, 2, …,. Но так как 1, 2, …, имеют исходящие переходы с одинаковыми атрибутами, в том числе с одинаковыми конечными состояниями (см. п. 2 техники), то после события +1 автомат A’ перейдет в Корректность рассмотренного рефакторинга доказана.

3.4.4. Выделение автомата Описание. Часть логики программы переносится в отдельный вызываемый автомат (рис. 8).

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

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

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

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

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

Следование такому критерию декомпозиции приводит к выделению в архитектуре программы пар автомат – объект управления (или группа автоматов – объект управления) и значительно приближает ее к «идеалу»

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

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

Для выделения состояний 1, 2, …, и исходящих из них переходов 1, 2, …, в вызываемый автомат необходимо выполнить следующие действия:

1. Убедиться, что среди состояний 1, 2, …, есть ровно одно такое состояние, в которое ведет хотя бы один переход из состояния, не входящего в множество 1, 2, …,. Обозначим отмеченный переход как, а его начальное состояние –.

2. Убедиться, что из отмеченного состояния достижимы все остальные состояния выбранного подмножества.