Парамонов А. В.

Аспирант кафедры управления и информатики в технических системах, Оренбургский государственный университет, Россия

Обзор методов автоматического построения программ плк в задачах логического управления

 

В статье рассматриваются существующие методы автоматического синтеза программ для программируемых логических контроллеров в задачах логического управления по формальным описаниям алгоритмов управления. В качестве таких формальных описаний приводятся конечные автоматы, сети Петри и LTL-спецификации.

Введение

Система логического управления (СЛУ) – система управления, входные и выходные переменные которой принимают только два значения – «истина» (логическая единица) и «ложь» (логический нуль). При построении таких систем в большинстве случаев используют программируемые логические контроллеры.

Программируемый логический контроллер (ПЛК) – управляющее устройство, имеющее определенное количество входов и выходов, подключенных к объекту управления, и работающее в режиме реального времени.

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

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

В статье на примере рассматриваются существующие методы автоматического синтеза программ по формальным описаниям алгоритмов управления.

Пример задачи логического управления

Рассмотрим пример задачи логического управления. Необходимо создать систему управления трансбордером – платформой, перемещающей железнодорожные вагоны между двумя параллельными путями. Допустим, что на пульте управления необходимо иметь только одну кнопку – «Пуск». На рисунке 1 показан общий вид трансбордера и пульта управления, в таблице 1 представлен перечень входных и выходных сигналов будущей системы управления.

Сигнал

Пояснение

x1

Нажатие кнопки «Пуск».

x2

Состояние концевого выключателя 1. Контроль наличия трансбордера на пути 1.

x3

Разрешение от машиниста толкателя 1. Сигнализирует о том, что толкатель загрузил вагон на платформу, отцеплен от него и находится на безопасном расстоянии.

x4

Состояние концевого выключателя 2. Контроль наличия трансбордера на пути 2.

x5

Разрешение от машиниста толкателя 2. Сигнализирует о том, что толкатель выгрузил вагон с платформы.

z1

Сигнал на перемещение трансбордера на путь 2.

z2

Сигнал на перемещение трансбордера на путь 1.

Рисунок 1 – Общий вид трансбордера (вид сверху)

Таблица 1 – Перечень сигналов

В начале работы машинист толкателя 1 загружает вагон на платформу и нажимает кнопку «Разрешение 1» (x3) с фиксацией.

При кратковременном нажатии на кнопку «Пуск» (x1), а также при условии, что платформа находится на пути 1 (x2), начинается перемещение трансбордера на путь 2 (z1). После начала движения кнопка разрешения на толкателе 1 может быть отжата.

Трансбордер останавливается на пути 2 когда замыкается концевой выключатель 2 (x4). Машинист толкателя 2 забирает вагон с платформы и нажимает кнопку «Разрешение 2» (x5) с самофиксацией.

После этого сразу же начинается движение платформы обратно на путь 1 (z2). О достижении исходного положения свидетельствует замыкание концевого выключателя 1 (x2).

Ниже представлено решение данной задачи различными методами.

Синтез программ ПЛК по графам переходов конечных автоматов

Подход заключается в описании алгоритма управления с помощью графа переходов (ГП) конечного автомата, и, затем, формальном переходе от графа к управляющей программе [1].

Рассмотрим процесс построения программы с помощью данного подхода.

1.   Построение схемы связей (рисунок 2).

2.   Построение ГП. Вершины помечаются комбинациями значений выходных сигналов, дуги помечаются булевыми формулами, приводящими к переходу (рисунок 3).

 

Рисунок 2 – Схема связей

Рисунок 3 – Граф переходов

3.   Переход от ГП к системе булевых формул (СБФ). Для каждой выходной переменной строится отдельная формула. Выделяются все вершины, в которых переменная закодирована единицей. Каждую дугу, входящую в эти вершины, представляют конъюнкцией формулы, помечающей эту дугу и формулы, соответствующей коду вершины, из которой эта дуга выходит. Наконец, дизъюнкция всех полученных конъюнкций и будет искомой формулой.

4.   Переход от СБФ к LD-программе. Для каждой формулы строится отдельная цепь (Рисунок 4). Для того чтобы исключить возможность влияния вычисленных значений выходных переменных в одном прогоне программы, необходимо их переобозначить.

Рисунок 4 – LD-программа

Синтез программ ПЛК по LTL-спецификации

LTL (Linear Temporal Logic) – логика линейного времени [3]. В этой логике высказывания принимают истинное или ложное значение в зависимости от того, когда это значение определяется. Например, высказывание «Я голоден» в конкретный момент времени может быть истинным или ложным, но не одновременно.

Помимо булевых связок, выражения связываются при помощи темпоральных операторов. Пусть  – некоторая булева формула, тогда  – означает, что  истинна в следующем состоянии,  – в некотором будущем состоянии,  – в текущем и всех будущих состояниях. При построении ПЛК программ описываются условия установки и сброса каждой выходной переменной ПЛК LTL-формулами. При этом для каждой выходной переменной вводится дополнительная переменная, показывающая значение в предыдущем состоянии. Такие дополнительные переменные дописываются символом «_» перед названием. Рассмотрим процесс построения программы с помощью данного подхода [2].

1.   Составление LTL-формул, описывающих условия установки и сброса каждой выходной переменной. Каждый раз, когда новое значение  становится больше предыдущего , можно утверждать, что выполнилось условие  и т.д.

2.   Построение модели Крипке на языке SMV [4]:

module main() {

x1,x2,x3,x4,x5: 0..1;

z1,z2: 0..1;

init(x1):=0;

init(x2):=1;

init(x3):=0;

init(x4):=0;

init(x5):=0;

init(z1):=0;

init(z2):=0;

case {

 ~z1 & next(x1) & next(x2) & next(x3) & ~next(x4): next(z1):=1;

 z1 & next(x4): next(z1):=0;

 default: next(z1):=z1;

};

case {

 ~z2 & ~next(x2) & next(x4) & next(x5): next(z2):=1;

 z2 & next(x2): next(z2):=0;

 default: next(z2):=z2;

};

p1: assert G(z1 + z2 <= 1);

p2: assert G~(x2 & z2);

p3: assert G~(x4 & z1);

}

3.   Верификация построенной модели (проверка выполнимости свойств, помеченных словом assert, для модели, описанной LTL-формулами) с помощью программы Cadence SMV.

4.   Построение LD-программы по LTL-спецификациям (рисунок 5).

Рисунок 5 – LD-программа

Синтез программ ПЛК по сетям Петри

Рассмотрим процесс построения программы по дискретно-событийной модели объекта управления с супервизором в виде сети Петри [5].

1.   Построение модели объекта управления (рисунок 6, позиции p1 – p14). В сети Петри некоторым определенным позициям будут соответствовать выходы ПЛК, а некоторым определенным переходам – входы.

2.    Формулировка ограничений для модели. Для данной модели необходимо ввести два ограничения. Первое заключается в том, что двигатель не может перемещать трансбордер на путь 2 если он уже находится там, а второе в том, что двигатель не может перемещать трансбордер на путь 1 если он уже находится там. Другими словами позиция p1 достижима только тогда, когда отсутствуют фишки в p12, а p3 – когда отсутствуют фишки в p6.

Матрица ограничений L – матрица размером , где  – количество ограничений,  – количество позиций. В ней единицы стоят в тех столбцах, номера которых соответствуют номерам позиций, участвующих в ограничении.

3.   Построение сети супервизора. Матрица инцидентности сети супервизора определяется по формуле:

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

 

4.   Определение начальной маркировки сети супервизора. Начальная маркировка сети супервизора определяется по формуле:

,

где  – вектор из целых чисел в правых частях ограничений,  – начальная маркировка исходной сети.

Сеть Петри с супервизором представлена на рисунке 6.

Рисунок 6 – Сеть Петри с супервизором

5.   Переход от сети Петри к LD-программе. Для каждой позиции, которой соответствует выходной сигнал, строится отдельная цепь. Если сигнал положительный, то цепь завершается -(S)- катушкой, если же отрицательный, то -(R)- катушкой. Выделяются входные переходы позиции. Для каждого перехода строится конъюнкция, состоящая из условия срабатывания самого перехода, а также условий срабатывания всех входных переходов входных по отношению к данному переходу позиций. При этом повторяющиеся условия не выписываются, как и условия, которым не соответствует ни один вход ПЛК. Кроме того, исключаются условия срабатывания переходов, к которым идут дуги из рассматриваемой позиции. Наконец, строится дизъюнкция полученных конъюнкций. Эта дизъюнкция и будет условием для срабатывания катушки.

На рисунке 7 представлена полученная LD-программа.

Рисунок 7 – LD-программа

Заключение

В работе на примере системы управления трансбордера рассмотрены существующие подходы к автоматическому построению программ ПЛК в задачах логического управления.

При автоматном подходе дуги ГП помечаются только теми входными переменными, от которых зависят соответствующие переходы. ГП в таком случае представляет собой очень наглядную и компактную форму записи алгоритма управления. Для понимания такой формы участникам разработки не нужно обладать специальными знаниями. Кроме того, компактность ГП делает подход пригодным для решения задач большой размерности. Несмотря на указанные достоинства, если строить программы изоморфно ГП, то они получатся неэффективными по времени и памяти. Также построение ГП является сложной творческой задачей, иногда невыполнимой вовсе. Однако для решения данной проблемы применяется генетическое программирование.

Подход на основе LTL-спецификаций – мощное средство для построения корректных и надежных программ. Модель, несмотря на текстовую форму, достаточно наглядна. Построенный код изоморфен LTL-спецификациям. К недостаткам можно отнести применимость только к задачам малой и средней размерности. Метод также требует от разработчика знаний о темпоральной логике.

Графическое представление модели сетью Петри наглядно, но размер графа быстро увеличивается с увеличением размерности задачи. Это затрудняет применение для задач большой размерности. Программа строится формально по модели, но не изоморфно ей.

Каждый из рассмотренных методов предполагает наличие заранее определенного, единого для всей задачи, способа перевода модели в программный код. Например, самофиксация выходных переменных реализуется либо триггерами во всей программе, либо -(S)- и -(R)- катушками во всей программе, либо добавлением контакта фиксируемого сигнала параллельно в цепь также во всей программе. При этом не учитываются все особенности самого языка программирования, которые в некоторых отдельных ситуациях могут помочь сделать программу эффективнее и нагляднее.

Литература

1.   Шалыто А. А. SWITCH – технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998

2.   Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация LD-программ ПЛК по LTL-спецификации // Моделирование и анализ информационных систем. Ярославль, 2013. Т. 20, №6 (2013). С. 78–94.

3.   Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. / Под ред. Р. Смелянского. – М.: МЦНМО, 2002

4.   McMillan K. L. Getting started with SMV, 1999

5.   Хадеев А.С., Браништов С.А. Метод синтеза LD-программ для ПЛК на основе концепции супервизорного управления дискретно-событийными системами, представленными в сетях Петри // Автоматизация, телемеханизация и связь в нефтяной промышленности, №1. – М., 2013. – c. 42-48.