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

№56-2,

технические науки

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

Похожие материалы

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

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

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

if x < 70then <блок операторов 1>else if x < 80then <блок операторов 2>else <блок операторов 3>;

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

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

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

if T1then begin <блок операторов 1> endelse if T2then begin <блок операторов 2> end...else begin <блок операторов n> end;

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

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

if T1then begin <блок операторов 1> endelse if T3then begin <блок операторов 2> end...else begin <блок операторов n-1> end;

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

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

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

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

Интерпретация переменной l в виде совокупности термов T
Рисунок 1. Интерпретация переменной l в виде совокупности термов T

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

if T1then <открыть подачу бензина на 100%>else if T2then <открыть подачу бензина на 75%>else <остановить подачу бензина>

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

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

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

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

if T1then <открыть подачу бензина на 100%>else if T2then <открыть подачу бензина на 75%>else if T3then <остановить подачу бензина>else <выполнить защитные действия>

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

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

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

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

Список литературы

  1. Седова Н.А., Седов В.А. Методы оценки качества полученных решений // Южно-Сибирский научный вестник. 2012. № 1. С. 88–91.
  2. Седова Н.А. Нечёткая система определения степени влияния мелководья // Научные проблемы транспорта Сибири и Дальнего Востока. 2013. № 1. С. 27–30.
  3. Мустафина С.А., Степашина Е.В. Редукция кинетических схем сложных химических процессов на основе теоретико-графового подхода // Вестник Казанского технологического университета. 2014. № 10. С. 17–20.
  4. Антипин А.Ф. Обзор проблемных ситуаций в коде программ // Современная техника и технологии. 2015. № 2. С. 82–85.
  5. Антипин А.Ф. Способ фаззификации значений непрерывных величин с предсказанием термов в многомерном четком логическом регуляторе // Автоматизация в промышленности. 2013. № 9. С. 65–68.
  6. Антипин А.Ф. Особенности программной реализации многомерных логических регуляторов с переменными в виде совокупности аргументов двузначной логики // Автоматизация и современные технологии. 2014. № 2. С. 30–36.
  7. Антипин А.Ф. Об одном способе анализа структуры многомерного четкого логического регулятора // Прикладная информатика. 2012. № 5. С. 30–36.
  8. Антипин А.Ф. Организация эффективной работы преподавателей в условиях рейтинговой системы обучения // Прикладная информатика. 2014. № 3. С. 48–59.
  9. Антипин А.Ф. К вопросу о семантическом анализе программ автоматизированных систем управления // Информационные системы и технологии. 2015. № 5. С. 45–52.
  10. Антипина Е.В., Антипин А.Ф. Применение интеллектуальных технологий для анализа многомерных данных // Молодой ученый. 2014. № 19. С. 172–175.
  11. Антипин А.Ф. Способ анализа программного кода автоматизированной системы управления технологическими процессами // Автоматизация, телемеханизация и связь в нефтяной промышленности. 2013. № 10. С. 21–25.