4. Проверка модели ПЛК
ПЛК широко используется во многих приложениях и имеет множество устройств; это большая область исследований. В любой работе ПЛК задействовано различное оборудование и люди, поэтому система ПЛК является параллельной. В то же время, если в системе ПЛК есть ошибки, их трудно обнаружить, в основном из-за ошибок логического проектирования, но не ошибок вычислений. Поэтому мы сосредоточимся на логическом процессе программы обнаружения ПЛК, а эта логика может быть полностью описана битовой логикой. Поэтому, чтобы упростить модель программы ПЛК и сосредоточиться на проверке модели, мы
Выполните следующие настройки:
ПЛК - это программа логического управления, и все управляющие переменные имеют только два состояния: 0 и 1;
Программы ПЛК выполняются в параллельной среде. В этом случае в программировании ПЛК с большой вероятностью могут возникнуть ошибки, которые нелегко обнаружить.
Учитывая вышеперечисленные особенности, для проверки мы используем инструмент проверки моделей SPIN (наш инструмент PLC-Checker также реализует NuSMV). Мы сформулировали ряд правил преобразования для построения вышеуказанной модели на входном языке SPIN - Promela. Атрибуты системы также должны быть переведены на Promela. SPIN собирает их вместе и затем выполняет обнаружение.
Язык PROMELA - это C-подобный язык, и семантически они похожи. Поэтому мы просто приведем несколько примеров, чтобы показать основные концепции перевода. Подробную информацию о языке PROMELA можно найти на сайте www.spin root.com. Мы представим три части файла PRO MELA в качестве входных данных для SPIN.
1) Код контроллера ПЛК
Контроллер ПЛК состоит из нескольких сетей.
Код для контроллера ПЛК также генерируется из сети. Конечно, перед этим необходимо объявить нужные переменные. Каждая сеть имеет входные и выходные порты, и каждый порт может быть представлен булевым выражением. Мы вычисляем все входные порты, логически присваивая им значения выходных портов. Вот как можно перевести сеть ПЛК.
Вот пример преобразования сети SR:
если
::Exp(R) == 1 -> Q = 0;
::Другие->
if::Exp(S) == 1 -> Q = 1;
::else -> skip; фазан;
Фэй;
/* Exp(S) - булево выражение порта S.
Exp(R) - это булево выражение для порта R.
Q - выходной порт*/
2) Кодекс совпадающих организаций
Мы считаем, что каждый параллельный объект - это уникальный процесс, независимо от поведения человека или оборудования. Эти процессы имеют общие переменные с процессом контроллера ПЛК. Это необходимо сделать для обеспечения параллелизма системы. Во второй части этой статьи мы говорили о том, что все параллельные сущности моделируются как автоматы. Автомат означает переход из одного состояния в другое. Для формирования состояния сущности мы используем порты I. В качестве переходов используем операторы goto (как в языке ассемблера). Простой пример выглядит следующим образом:
Статус A:
атом{
если
:: Q1 -> {IB, перейти в состояниеB}
:: Q2 -> {IC, перейти в состояниеC}
Филиппины;}
/* 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. На данном этапе механизм все еще имеет множество недостатков, таких как работа с таймером. Но у него есть большие и уникальные преимущества для решения задач исследования состояния. Мы продолжаем активно исследовать эти вопросы.