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

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

В шасси два двигателя: по одному на левую и правую гусеницы. Прототип программы состоит из двух автоматных типов: AEngine и AManager.

Рисунок 3.8.1. Граф переходов автоматного типа AEngine

Автомат типа AManager (рисунок 3.8.2) отправляет команды на

управление двигателями в зависимости от команд для управления шасси.

Рисунок 3.8.2. Граф переходов автоматного типа AManager

При входе в состояния этот автомат отправляет следующие события автоматам AEngine (слева от стрелки написано имя автомата, справа - событие):

• Stopped: left stop, right stop.

• MoveForward: left forward, right forward.

• MoveBackward: left backward, right backward.

• TurnRight: left backward, right forward.

• TurnLeft: left forward, right backward.

• ForwardRight: left stop, right forward.

• ForwardLeft: left forward, right stop.

• BackwardRight: left backward, right stop.

• BackwardLeft: left stop, right backward.

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

утверждение относится к аппаратной части, что в диссертации не рассматривается.

Формализуем указанное свойство. Высказывание «Поступила команда «стоп» означает, что в автомат manager пришло событие stop. В нотации инструментального средства Staterоно записывается следующим образом: {manager.stop}. Высказывание «подана команда остановки левого двигателя» означает, что автомат left вызвал функцию EngineStop. В нотации средства Staterоно записывается следующим образом: {left.EngineStop}. Поэтому, рассматриваемое свойство переписывается следующим образом: в любой момент времени в автомат manager пришло событие stop, следовательно, в будущем автомат left вызовет функцию EngineStop:

G ({manager . stop} => (F {left. EngineStop})) (2)

Получаем следующую формулу:

[] ( {manager.stop} -> ( {left.EngineStop} )) (3)

Отметим, что в соответствии с синтаксисом языка Promela,оператор G (всегда) обозначается как [], а оператор F (в будущем) - .

Запустив инструментальное средство Staterи выполнив верификацию, получим ответ, который означает, что верифицируемое свойство выполняется в построенной системе:

0. [] ( {manager.stop} -> ( {left.EngineStop} ))

Verification successful!