OPS: Automata — различия между версиями

Версия 11:49, 22 июля 2009

Введение

Автоматное программирование (Automata-based Programming, или программирование от состояний) основано на использовании конечных автоматов, описывающих поведение программ.

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

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

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

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

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

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

Данная работа «Разработка программного модуля автоматизации формирования программного кода на языке C по графу переходов конечного автомата» (далее OPS: Automata) предназначена для автоматизации этапов проектирования, разработки и, быть может, верификации программного обеспечения.

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

Задача OPS: Automata предназначена для автоматизации некоторых этапов (этапов проектирования, разработки и, быть может, тестирования) жизненного цикла программного обеспечения (ПО), разрабатываемого с применением автоматного подхода.

Цель решения задачи: генерация кода программ на языке C с явным выделением состояний.

Выходная информация:

• код программы на языке C.

Входная информация:

• граф переходов автомата (возможно, диаграмма состояний).

Обзор программ-аналогов

Начнем с того, что аналогичных программных продуктов (ПП) много.

UniMod

Представляет собой плагин к среде разработки Eclipse. А.А. Шалыто говорит об UniMod, как о единственном средстве генерации программ по автоматам в своем роде [1]. См. также [7, 8, 12, 13].

Немного фактов

• официальный сайт;
• открытое;
• свободное;
• написано на Java;
• сопровождается;
• ведутся работы по доработке [3].

Возможности

• Создание и редактирование схем связей и графы переходов управляющих автоматов, которые создаются на основе диаграмм классов и состояний языка UML.
• Выполнение валидации автоматов: проверяет достижимость состояний, полноту и непротиворечивость условий переходов.
• Поддержка отладки программ в терминах автоматов, когда при пошаговом выполнении на диаграмме состояний подсвечивается текущее состояние, переход, выходная переменная и т. п.
• Позволяет производить проверку корректности построенных с его помощью программ на основе метода Model Checking.
• Может осуществлять как компиляцию диаграмм в код на различных языках программирования (Java, C++), так и непосредственную интерпретацию с промежуточным преобразованием диаграмм в описание на языке XML.

Процесс разработки с использованием UniMod

Процесс разработки системы со сложным поведением с помощью этого инструментального средства состоит в следующем [1]:

1. На основе анализа предметной области производится объектная декомпозиция системы, определяются сущности и отношения между ними.
2. В отличие от традиционных для объектно-ориентированного программирования подходов, из числа сущностей выделяются источники событий, объекты управления и автоматы. Источники событий активны – они по собственной инициативе воздействуют на автомат. Объекты управления пассивны и выполняют действия по команде от автомата. Они также формируют значения входных переменных для автомата. Автомат активируется источниками событий и на основании значений входных переменных и текущего состояния воздействует на объекты управления и переходит в новое состояние.
3. С использованием нотации диаграммы классов, строится схема связей автомата, которая задает его интерфейс. На этой схеме слева отображаются источники событий, в центре – автоматы, а справа – объекты управления. Источники событий с помощью UML-ассоциаций связываются с автоматами, которым они поставляют события. Автоматы связываются с объектами, которыми они управляют.
4. Каждый объект управления содержит два типа компонентов, реализующих входные и выходные переменные.
5. Для каждого автомата с помощью нотации диаграммы состояний строится граф переходов, в котором дуги могут быть помечены событием, булевой формулой из входных переменных и выходным воздействием на переходе. В вершинах могут быть указаны выходные воздействия в состояниях и имена вложенных автоматов. Каждый автомат имеет одно начальное и произвольное число завершающих состояний.
6. Состояния на графе переходов могут быть простыми и составными (суперсостояния). Если в состояние вложено другое состояние, то оно является составным. В противном случае состояние простое. Основной особенностью составных состояний является то, что дуга, исходящая из такого состояния, заменяет однотипные дуги из каждого вложенного состояния.
7. Компоненты объекта управления, соответствующие входным и выходным переменным, реализуются вручную на целевом языке программирования.

Минусы

• Не генерирует исходный код на C.
• Концепция «автоматы и объекты управления как классы» нарушает стройность объектно-ориентированной структуры системы и приводит к появлению в ней нового типа сущностей – автоматов. Это ограничивает модульность (поскольку автоматы в действительности не являются самостоятельными сущностями) и усложняет выделение уровней абстракции.
• Как следствие предыдущего пункта, требуется не только объектная, но и автоматная декомпозиция, что еще больше усложняет структуру системы.
• В графической нотации описания поведения смешиваются элементы из различных языков: используются как составные состояния, так и вложенные автоматы.
• Модули системы не являются в достаточной степени самостоятельными и не предназначены для повторного использования. Например, имена компонентов объектов управления совпадают с краткими идентификаторами входных и выходных переменных автомата. Это довольно странно, если допустить, что класс объекта управления мог разрабатываться отдельно от управляющего автомата и может быть повторно использован в другой системе. Кроме того, для автоматов множество их клиентов ограничивается заранее заданными поставщиками событий, что препятствует использованию разработанных автоматов в другом контексте.
• В инструменте UniMod используется довольно странная автоматная модель [1]. С одной стороны, все автоматы являются пассивными: совершают переходы только при возникновении события. Кроме того, работа системы начинается с запуска источников событий. Однако все автоматы снабжены завершающими состояниями, и окончание работы системы происходит по инициативе автомата. Такая модель находится где-то между пониманием автомата как главной программы (унаследованного из процедурного программирования с явным выделением состояний) и как сущности, предоставляющей набор сервисов. В доказательство наличия пережитков процедурного подхода, в большинстве проектов, созданных с помощью инструмента UniMod, существует единственный главный автомат, в который вложены все остальные. [1]

EiffelState

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

Немного фактов

• официальный сайт.

SMC

SMC (The State Machine Compiler, The State Map Compiler) — Java приложение.

Немного фактов

• официальный сайт;
• Генерирует код на C, C++, C#, Groovy, Java, Lua, Objective-C, Perl, PHP, Python, Ruby, Scala, Tcl и VB.net.

FSME

FSME (Finite State Machine Editor)

Немного фактов

• официальный сайт.

Минусы

• использует Qt3, причем после попытки автоматически привести к Qt4 (qt3to4) возникают неустраняемые (я не могу устранить) ошибки компиляции.

MetaAuto

Немного фактов

• официальный сайт.

dia2fsm, fsmgen

Немного фактов

• сайт.
• генерирует код на C, C++;
• для рисования графов конечных автоматов (КА) используется редактор диаграм Dia (версии 0.96.1);
• Dia распространяется под лицензией GNU;
• есть возможность организации библиотек автоматов;
• текущая версия генератора работает под Win32;
• планируется создание версии для Linux.

Возможности

• производится проверка на непротиворечивость переходов — из одного cостояния не может выходить два и больше переходов по одному и тому же событию, с одним и тем же условием guard.
• Производится проверка переходов по умолчанию (default transitions) со значением guard '*'. При наличии нескольких переходов генерируется ошибка, при отсутствии хотя бы родного — выдается пердупреждение.
• Производится проверка безусловных переходов (не задано guard condition), при наличии нескольких безусловных переходов по одному событию генерируется ошибка.

Вывод

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

Описание существующих технологий решения задачи OPS: Automata

Разработка GUI

GUI (Graphical user interface — графический интерфейс пользователя) может быть разработан с использованием:

• библиотеки Qt4;
• .net;
• java.

Выбор и обоснование средств программной реализации задачи OPS: Automata

Пользовательский интерфейс

Было принято решение не использовать существующие средства создания UML-диаграмм. Одно из самых распространенных средств (MS Visio) является коммерческим, некоторые свободные программы либо идут как плагины к средам разработки (Eclipse, NetBeans), либо не являются достаточно удобными для пользователя (Rational Rose), другие не соответствуют общепринятым стандартам UML (PSUML, MS Visio) [5]. Кроме того, применение даже наиболее удачных средств построения UML диаграмм (BOUML) может мешать дальнейшему расширению возможностей разрабатываемого программного модуля.

Для реализации GUI решено использовать ___, так как это является обязательным требованием.

Список используемых источников

1. Поликарпова Н.И., Шалыто А.А. Автоматное программирование. — 1-е изд. — СПб.: Питер, 2009. — 176 с.
2. Сайт по автоматному программированию
3. SYRCoSE 2008. A. Khoroshilov, V. Mutilin, V. Shcherbina, O. Strikov, S. Vinogradov, and V. Zakharov. How to Cook an Automated System for Linux Driver Verification. Volume 2, pp. 11-14., Presentation
4. Канжелев С.Ю., Шалыто А.А. Автоматическая генерация кода программ с явным выделением состояний. Статья в рамках «Software Engineering Conference (Russia) – 2006», презентация.
5. UML. В поисках инструментов. Обсуждение на нашем форуме.
6. Верификация автоматных программ
7. UniMod. Публикации
8. UniMod. Проекты
9. Визуальное конструирование программ
10. Реализация систем, управляемых событиями
11. Static Finite State Machine. Кодогенерация времени компиляции Compiler-time code generation
12. UniMod. Публикации (англ.)
13. UniMod. Проекты (англ.)

Текущее состояние проекта

22.07.09

В настоящий момент ищу/смотрю/пробую на вкус существующие ПП. Их очень много (возможно, настолько много, что в создании еще одного нет необходимости). Все-таки, не смотря на многообразие, пока не вижу того, который удовлетворил бы всем предъявляемым требованиям. Однако, некоторые (UniMod) очень хороши и я решила, что разработка будет вестись, с оглядкой на них, в частности мне безумно (плохое слово) понравились возможности UniMod по отладке программ и я бы очень хотела повторить это, тем более, что другие ПП не предоставляют средств отладки вообще (это заключение сделано после беглого осмотра), что является не только отсутствием большого плюса, но и наличием большого минуса, поскольку одним из важнейших свойств автоматного подхода является существование средств проверки правильности. Я же не вижу препятствий по диаграмме состояний (или графу переходов, это зависит от реализации) проверять достижимость состояний (в любое состояние автомата должен вести путь из начального состояния, составленный из переходов), непротиворечивость (не должно существовать такого входного воздействия, при котором условия нескольких переходов из некоторого состояния автомата будут одновременно истинными) и полноту (для любого входного воздействия должен существовать хотя бы один переход из множества переходов из данного состояния автомата, условие которого будет истинным) множества переходов, хотя это и весьма трудоемко и, возможно, вскоре я откажусь от своих слов. Так же UniMod позволяет производить корректность на основе метода Model Checking (проверка модели). Я еще не вникала что это, но на сайте [1] представлено много работ [6], посвященных верификации, это заставляет верить в лучшее. Правда, некоторые из возможностей UniMod я реализовать технически не в состоянии, например, делать точками останова элементы графа переходов (для этого требуется связь со средой).

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

22.07.09

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