Верификация автоматов стандарта IEC 61499

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

3.5.1. Верификация базовых функциональных блоков

Базовый функциональных блок (БФБ) (рисунок 3.5.1.1) состоит из следующих компонентов:

• описание конечного автомата;

• список входных событий;

• список выходных событий;

• список входных переменных;

• список выходных переменных;

• список алгоритмов (выходных воздействий).

Рисунок 3.5.1.1. Пример автомата базового функционального блока

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

Алгоритм представляет собой выходное воздействие, аналогичное выходным воздействиям из множества Z₂из математической модели, описанной в разделе 3.1.1.

Листинг 3.5.1.1. XML-описание алгоритма

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

Приведём алгоритм построения автомата (предложенного автором) по автомату из БФБ:

1. Все состояния из БФБ переносятся в множество S. При этом s0 - первое состояние из описания БФБ.

2. Множество T- пустое.

3. Все входные события из БФБ переносятся в множество E.

4. Все входные и выходные переменные переносятся в множество X.

5. Алгоритмы переносятся в множество Z₂.

6. Все логические функции на переходах БФБ переносятся в множество B.

7. По описаниям переходов БФБ строится отношение δ

8. По описаниям вызываемых алгоритмов строится отношение λ

3.5.2. Верификация составных функциональных блоков

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

Рисунок 3.5.2.2. Составной функциональный блок

Пример связи, описывающей общие переменные:

dx1="383.3333" />

Пример связи, описывающей взаимодействие при помощи отправки событий:

Приведём алгоритм, описывающий построение системы

взаимодействующих иерархических конечных автоматов по СФБ.

1. По каждому БФБ, принадлежащему СФБ, строится автомат по алгоритму из раздела 3.5.1.

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

3. Отношение ω, описывающее общие переменные, напрямую строится при помощи связей, описывающих общие переменные.

Второй шаг. Система автоматов, построенная при помощи этого алгоритма, верифицируется при помощи метода, описанного в разделе 3.2.

3.6.