К вопросу о верификации программ программируемых логических контроллеров

Рассмотрим метод верификации программ программируемых логических контроллеров, входящих в состав автоматизированных систем управления технологическими процессами, основанный на положениях концепции семантического анализа структуры многомерных интервально-логических регуляторов (МИЛР), которые являются альтернативной ступенью развития нечетких регуляторов [1, 2, 3, 4].

Предварительно введем понятия полной, частично полной и неполной системы продукционных правил (СПП) [5, 6, 7, 8].

Предположим, что значение переменной x может меняться в диапазоне [0; 100]. Тогда для СПП S:

if x then else if x then else ;

термы переменной x соответствуют интервалам: [0; 70), [70; 80) и (80; 100].

Данная СПП является полной, т. е. она описывает все возможные действия при всех возможных вариантах значений переменной x.

В общем виде полная СПП S_п для переменной x, представленной совокупностью n термов T, имеет вид [9, 10]:

if T1then begin  endelse if T2then begin  end...else begin  end;

СПП S_чп является частично полной, если её можно считать полной, но при этом в ней отсутствует проверка истинности некоторых термов.

Например, в СПП S:

if T1then begin  endelse if T3then begin  end...else begin  end;

отсутствует проверка истинности терма T₂, но, если нахождение переменной x в пространстве значений T₂ не влияет на значения других переменных, то такая СПП является частично полной.

Если система правил не включает в себя все возможные действия при всех возможных вариантах значений переменной x, то она является неполной и обозначается как S_н.

Решить, является ли некоторая СПП S полной, частично полной или неполной может только эксперт.

Рассмотрим следующий пример. В резервуар с вмонтированным датчиком уровня наливают бензин со скоростью, которая зависит от значения переменной l, хранящей текущее значение уровня бензина в резервуаре, и представленной в виде совокупности термов T так, как показано на рис. 1.

Упрощенно, СПП S для переменной l имеет вид:

if T1then else if T2then else 

На первый взгляд данная система правил кажется полной, однако, в ней нет ни единого правила, описывающего действия в случае, если подача бензина в резервуар не прекратилась при достижении уровня l отметки в 85%.

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

Чтобы избежать такой ситуации можно, например, разбить терм T₃ на два терма T₃ и T₄, установив тем самым сигнализацию верхнего и аварийного уровней.

СПП S в этом случае будет иметь вид:

if T1then else if T2then else if T3then else 

Учитывая все сказанное выше, разработанный автором метод верификации программ программируемых логических контроллеров заключается в следующем:

1. Представить систему управления в виде МИЛР, а все переменные интерпретировать эквивалентной совокупностью аргументов двузначной логики, то есть термами.
2. Выделить в программном коде продукционные правила для каждой из переменных, термы которых содержатся в антецедентах правил.
3. Установить тип каждой из выделенных СПП. Если имеются неполные системы правил, то их необходимо дополнить до полных или, как минимум, до частично полных.
4. Выполнить семантический анализ МИЛР, например, в прикладном программном обеспечении [11], разработанном автором.

Шаги 1 и 2 можно объединить, а шаги 3 и 4 можно выполнять в любой последовательности и неоднократно до тех пор, пока не будут выявлены и устранены все ошибки.

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