Такая структура состоит из пяти компонентов:
•
Множество состояний, включающее в себя начальное состояние.
Этот компонент присутствует в разработанной системе.
•
Множество локальных часов. Часы также используются в систе-
ме — как явно описанные пользователем, так и формульные.
•
Множество действий (включая пустое действие). Во временн ´oм
автомате каждому переходу может соответствовать максимум одно
действие, которое является условием перехода по ребру. Аналогом
в данной системе является событие.
•
Инвариант, присутствующий в некоторых локациях.
•
Множество переходов. Каждый переход помечен действием, вре-
менн´oй защитой перехода и сбрасываемыми часами. Использование
всех этих пометок возможно в системе.
Таким образом, на вход системы можно подать временн´oй автомат.
При этом не используются входные и выходные воздействия. Также
нужно учесть, что во временн´oм автомате переход представляет со-
бой единое целое и разбивать его на отдельные участки не следует.
Поэтому задержку в состоянии, соответствующему любому событию,
нужно сделать нулевой.
При рассмотрении возможности верификации с помощью разрабо-
танной системы программ общего вида (представленных в виде вре-
менн´oго автомата) возникает вопрос: к каким классам систем возмож-
но применение данного верификатора?
Другие классы систем.
Итак, данная система может использовать-
ся для верификации временн ´ых автоматов, с помощью которых могут
быть представлены программы общего вида. Однако существует мно-
жество видов автоматов, которые используются в различных классах
программных систем. Рассмотрим некоторые из этих классов.
Реактивные системы.
Это основное направление, в котором ис-
пользуются автоматные программы. Поэтому в системах этого класса
возможно наиболее полное использование возможностей как самого
автоматного программирования, так и разработанного верификатора.
Отдельно рассмотрим одну из традиционных областей применения
автоматов — задачу логического управления. Системы этого подклас-
са имеют ряд особенностей: не задействованы события, используются
автоматы Мура, большое значение имеет параллелизм, широко исполь-
зуется взаимодействие обменом состояний. Автоматы, применяемые в
таких системах, могут быть проверены с помощью разработанной си-
стемы. При этом не используются события и выходные воздействия
на переходах.
Трансформирующие системы
, например компиляторы, — это тра-
диционная сфера применения конечных автоматов.
52
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
1,2,3,4,5 7,8,9,10,11,12,13,14