4. Проверка модели ПЛК
ПЛК широко используется во многих приложениях и имеет множество устройств; это большая область исследований. В любой работе ПЛК задействовано различное оборудование и люди, поэтому система ПЛК является параллельной.
Если в системе ПЛК есть ошибки, которые трудно найти, они в основном связаны с ошибками логического проектирования, но не с ошибками вычислений. Поэтому мы сосредоточимся на логическом процессе программы обнаружения ПЛК, и эта логика может полностью
Описание битовой логики. Поэтому, чтобы упростить модель программы ПЛК и сосредоточиться на проверке модели, мы делаем следующие настройки:
ПЛК - это программа логического управления, и все управляющие переменные имеют только два состояния: 0 и 1;
Программы ПЛК выполняются в параллельной среде. В этом случае в программировании ПЛК с большой вероятностью могут возникнуть ошибки, которые нелегко обнаружить. Учитывая эти особенности, для проверки мы используем инструмент проверки моделей SPIN (наш PLC-Checker также реализует NuSMV на модели, созданной выше). Мы сформулировали ряд правил преобразования для построения вышеуказанной модели на входном языке SPIN - Promela. Атрибуты системы также должны быть переведены на Promela. SPIN собирает их вместе и затем выполняет обнаружение. Язык PROMELA - это C-подобный язык, и они семантически схожи. Приведем несколько примеров.
Показывает основные понятия перевода. Подробную информацию о языке PROMELA можно найти на сайте www.spin root.com. Мы представим три части файла PRO MELA в качестве входных данных для SPIN.
1) Код контроллера ПЛК
Контроллер ПЛК состоит из нескольких сетей.
Код для контроллера ПЛК также генерируется из сети. Конечно, перед этим необходимо объявить нужные переменные. Каждая сеть имеет входные и выходные порты, и каждый порт может быть представлен булевым выражением. Мы присваиваем значение выходному порту с помощью логики
Подсчитайте все входные порты. Это перевод
Сетевой метод ПЛК.
Вот пример преобразования сети SR:
if ::Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp(S) - булево выражение порта S Exp(R) - булево выражение порта R Q - порт вывода */
2) Кодекс совпадающих организаций
Мы считаем, что каждый параллельный объект - это уникальный процесс, независимо от поведения человека или оборудования. Эти процессы имеют общие переменные с процессом контроллера ПЛК. Это необходимо сделать для обеспечения параллелизма системы. Во второй части этой статьи мы говорили о том, что все параллельные сущности моделируются как автоматы. Автомат означает переход из одного состояния в другое. Для формирования состояния сущности мы используем порты I. В качестве переходов используем операторы goto (как в языке ассемблера). Простой пример выглядит следующим образом:
atomic { if :: Q1 -> {IB, geto StateB} :: Q2 -> {IC, goto StateC} fi;} /* StateA - метка состояния A Q1, Q2 - условие перехода IB - установить значение состояния в значение состояния B goto StateB означает переход в состояние B */
3) Код собственности
Свойства - это правила, которым должна соответствовать система ПЛК. В качестве формата ввода мы используем формулу LTL (линейная временная логика). Мы должны написать противоположное свойство из-за механизма SPIN. SPIN обнаружит, что наш случай свойства имеет место, что должно стать контрпримером. Мы не можем написать LTL-формулу напрямую, а используем макрос ing. Сначала мы должны определить все пропозиции в макросах на языке LTL (например, #define p i5 == 0), а затем использовать определенные пропозиции для формирования LTL-формул. Spin может автоматически преобразовывать LTL-формулы в коды PRO MELA с помощью команды "SPIN-f" (подробнее см. в руководстве SPIN).
4) Механизм ожидания уведомлений
При обсуждении моделирования мы рекомендуем не добавлять механизм ожидания времени. Этот механизм также должен быть отражен в коде. Конкретная реализация заключается в том, что битовая переменная каждого процесса, не относящегося к ПЛК (за исключением всех контроллеров ПЛК), подписывается как сигнал. Когда автомат переходит в метку состояния, сигнальная переменная устанавливается в 0, и для продолжения следующего задания требуется, чтобы эта переменная была равна 1. Этот процесс продолжается благодаря особенностям синтаксиса PROMELA. В процессе ПЛК такого ограничения нет. Вместо этого процесс ПЛК может установить эти переменные в 1, тем самым гарантируя, что каждый шаг должен быть завершен, по крайней мере, через одно сканирование ПЛК. Это называется механизмом ожидания уведомления.
Выполнив четыре описанных выше шага, мы получим полный входной файл SPIN для нашей системы. Затем мы можем использовать SPIN для проверки модели. Пошаговую программу проверки модели SPIN можно найти в руководстве SPIN (см. www.spin root.com). SPIN выдаст результат о том, найден ли контрпример. Мы можем использовать теорию для анализа файла отслеживания, предоставленного spin, о котором говорилось выше. Используя этот механизм обнаружения, мы разработали инструмент проверки моделей PLC-checker. Он помогает строить визуальные модели и выполнять проверки, а также может дать простой анализ результатов. Конечно, найденный контрпример необходимо проверять вручную, чтобы определить, является ли он истинным контрпримером. Однако с помощью файлов следов это не очень сложная задача. Мы также успешно использовали некоторые программы проверки ПЛК (см. следующий раздел). В классическом примере из учебника контрпример был найден. Хотя вероятность контрпримеров очень мала, они все же встречаются и могут иметь серьезные последствия. Этот инструмент также доказывает правильность и обоснованность теории данной статьи.
5. Запустите программу PLC-Checker
Мы продемонстрируем эффективность PLC-проверяющего устройства при проверке модели канала с двумя воротами следующим образом. Для того чтобы отгородить комнату от внешнего мира, используются два дверных прохода.
Введя в инструмент лестничную диаграмму и параллельные сущности, которые являются определением свойств, мы выполняем проверку. На рисунке 3 показаны результаты. Как мы видим, в результате есть ошибка. Это подтверждается проверкой подсказок, которые являются реальным контрпримером для ручного архивирования. То есть наш механизм эффективен при проверке подобных ПЛК-программ.
6.в заключение
В данной работе мы изучаем теорию моделирования и проверки ПЛК с помощью формальных методов. В требованиях анализируются особенности моделирования ПЛК и устанавливается модель одновременных сущностей с помощью стратегии временных интервалов. Затем мы доказываем, что модель временных интервалов является супермножеством систем ПЛК, и сокращаем модель, добавляя механизм ожидания без времени. Это также гарантирует, что все изменения в системе могут быть просканированы контроллером ПЛК. Мы обнаружили, что можем находить ошибки в системе, изучая ее контрпримеры. Наконец, приводится использование SPIN для проверки модели. Также дано соответствующее введение в инструмент проверки модели PLC-Checker. На данном этапе механизм еще очень несовершенен, например, его обработка в виде таймера. Но он обладает большими и уникальными преимуществами для решения задач исследования состояния. Мы продолжаем активно изучать эти вопросы.