Описание интерфейса Stater

Инструментальное средство Staterпредназначено для того, чтобы визуально разрабатывать автоматные программы и подпрограммы. Возможности Stater:

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

• импортировать системы автоматов из Stateflowи стандарта IEC 61499.

• генерировать программный код на языке программирования C#;

• проводить верификацию системы конечных автоматов методом проверки моделей.

Для работы Staterтребуется .NET Frameworkверсии 4.0 или выше.

Генератор кода и верификатор реализованы в виде дополнений к основному модулю инструментального средства.

Верификация в Staterпроводится при помощи дополнения SpinVeriff. Для работы верификатора SpinVeriffтребуется наличие Spinверсии 6.23 и компилятора gcc(например, из пакета MinGW),а также путей к ним, прописанных в переменной окружения PATHиз ОС Windows.

На рисунке 3.7.1.1 изображен внешний вид инструментального средства Stater.

Рисунок 3.7.1.1. Интерфейс Stater

Создание системы конечных автоматов

Создание системы конечных автоматов рассмотрим на примере.

Для того чтобы разработать систему конечных автоматов, требуется создать проект, в котором находиться будет система конечных автоматов. Для этого в меню «Файл» необходимо выбрать пункт «Новый», а далее - «Проект». Появится диалоговое окно «Новый проект» (рисунок 4.3.1.2). В нем требуется выбрать местоположение проекта и его название и нажать кнопку «OK».

Рисунок 3.7.1.2. Новый проект

В результате будет создана папка с названием проекта, а в ней - файл . stp. При последующих открытиях Staterдля работы с этим проектом надо в меню «Файл» выбрать пункт «Открыть», а в нем выбрать «Проект».

Далее создаем диаграмму переходов автомата (рисунок 3.7.1.3).

Рисунок 3.7.1.3. Новая диаграмма

В диалоговом окне «Новая диаграмма» введём название автомата Alи

отметим кнопку «Конечный автомат» (рисунок 3.7.1.4). Если говорить в

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

Рисунок 3.7.1.4. Новая диаграмма - продолжение

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

Для того чтобы создать состояние, требуется нажать кнопку «Состояние» на панели инструментов, а после этого кликнуть в том месте, где на диаграмме должно располагаться состояние (рисунок 3.7.1.5). Состоянию автоматически присвоится имя.

Аналогично создадим еще одно состояние.

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

(отображается в виде красного креста). Рядом с ней находится кнопка отмены последнего действия.

Рисунок 3.7.1.5. Создание состояния

Создадим переход между этими состояниями (рисунок 3.7.1.6). Для этого требуется нажать на кнопку «Переход» на панели инструментов, кликнуть на состояние-начало перехода и на состояние-конец перехода.

Рисунок 3.7.1.6. Создание перехода

По двойному щелчку по состоянию или переходу вызывается редактор атрибутов (рисунок 3.7.1.7 и 3.7.1.8).

Рисунок 3.7.1.7. Атрибуты состояния

Рисунок 3.7.1.8. Атрибуты перехода

Имя состояния также является его идентификатором в сгенерированном программном коде и в модели для верификации. Таким образом, для имени состояния действуют все ограничения целевых языков программирования и языка Promela.Любое состояние может быть одного из трех типов: начальное (start state), обычное (common state) и конечное (end state). Начальное состояние помечается точкой. Конечное состояние помечается точкой внутри окружности. Начальное состояние в автомате может быть только одно. Остальные атрибуты будут описаны далее.

Состояние state0 отметим как начальное.

Откроем двойным щелчком редактор атрибутов созданного перехода (рисунок 3.7.1.8). Переход помечается событием, по которому он выполняется. Событие выбирается из списка «Выберите событие». В нём указаны все события из всех автоматов проекта.

Для создания события требуется нажать на кнопку «Новое событие». Откроется диалоговое окно «Редактирование события» (рисунок 3.7.1.9).

Рисунок 3.7.1.9. Создание события

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

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

Создадим выходное воздействие.

Рисунок 3.7.1.10. Выходные воздействия

Отметим состояние state1 как конечное. Добавим логическую переменную х1 в автомат. Для этого требуется щелкнуть правой кнопкой мыши по диаграмме автомата и выбрать в открывшемся контекстном меню пункт «Переменные». В диалоговом окне введём следующий текст:

bool х1;

Получаем автомат (рисунок 3.7.1.11).

Рисунок 3.7.1.11. Конечный автомат Al

Добавим в систему еще два автомата A2 и A3 и создадим в каждом из них стартовое состояние state 0.

Атрибуты состояния

Редактор атрибутов состоит из следующих вкладок:

• Общие.

• Выходные воздействия.

• Взаимодействие с автоматами.

• Запуск автоматов.

• Вложенные автоматы.

На вкладке «Общие» можно редактировать имя состояния в поле «Имя», его описание в поле «Комментарий» и выбрать тип состояния.

На вкладке «Взаимодействие с автоматами» можно объявить отправку событий другим автоматам в системе. Нельзя отправлять события вложенным автоматам. Отметим, что одни экземпляры автомата могут быть вложенными, а другие нет. Для отправки события экземпляру автомата требуется ввести тип автомата, имя экземпляра и имя события. Экземпляры автоматов могут быть запущены другими автоматами либо внешней средой.

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

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

Атрибуты перехода

Редактор атрибутов перехода состоит из следующих вкладок:

• Событие.

• Выходные воздействия.

• Взаимодействие с автоматами.

• Условия на переходах.

• Выходные воздействия: код.

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

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

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

Вкладка «Условие на переходе» позволяет накладывать условия на переменные автомата. В качестве условий можно задавать одновременно допустимые в целевых языках программирования и в языке Promela.Примеры условий:

• flag == true;

• al > a2.

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

Переменные

Инструментальное средство Staterподдерживает переменные и массивы (рисунок 3.7.1.12) следующих типов:

• bool;

• int8;

• int16;

• int32.

Переменные объявляются следующим образом:

[модификатор] = значение;

либо

[ модификатор] ;

Массивы объявляются так:

[модификатор] [число элементов];

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

Рисунок 3.7.1.12.

Описание флага Autorejectдля выбора режима работы системы автоматов

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

по диаграмме автомата и в контекстном меню отметить галочкой флаг autoreject.

Открытие проекта

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

3.7.2.