PLC System Modeling Approach (Part 1)
PLC Model Analysis and Improvement (Part 2)
4. PLC Model Checking
PLC is widely used in many applications and has many devices; it is a large area of research. Any PLC work involves different equipment and people, so the PLC system is concurrent. At the same time, if there are some errors in a PLC system, it is difficult to find them, mainly because of logical design errors, but not calculation errors. Therefore, we focus on the PLC detection program logic process, and this logic can be completely described by bit logic. Therefore, to simplify the PLC program model and focus on model checking, we
Выполните следующие настройки:
ПЛК - это программа логического управления, и все управляющие переменные имеют только два состояния: 0 и 1;
Программы ПЛК выполняются в параллельной среде. В этом случае в программировании ПЛК с большой вероятностью могут возникнуть ошибки, которые нелегко обнаружить.
Учитывая вышеперечисленные особенности, для проверки мы используем инструмент проверки моделей SPIN (наш инструмент PLC-Checker также реализует NuSMV). Мы сформулировали ряд правил преобразования для построения вышеуказанной модели на входном языке SPIN - Promela. Атрибуты системы также должны быть переведены на Promela. SPIN собирает их вместе и затем выполняет обнаружение.
The PROMELA language is a C-like language, and they are semantically similar. So we just give some examples to show the basic concepts of translation. To view detailed information about the PROMELA language, visit www.spinroot.com. We will introduce the three parts of the PRO MELA file as input to SPIN.
1) Код контроллера ПЛК
Контроллер ПЛК состоит из нескольких сетей.
Код для контроллера ПЛК также генерируется из сети. Конечно, перед этим необходимо объявить нужные переменные. Каждая сеть имеет входные и выходные порты, и каждый порт может быть представлен булевым выражением. Мы вычисляем все входные порты, логически присваивая им значения выходных портов. Вот как можно перевести сеть ПЛК.
Вот пример преобразования сети SR:
если
::Exp(R) == 1 -> Q = 0;
::Others->
if::Exp(S) == 1 -> Q = 1;
::else -> skip; pheasant;
Фэй;
/* Exp(S) - булево выражение порта S.
Exp(R) - это булево выражение для порта R.
Q - выходной порт*/
2) Кодекс совпадающих организаций
Мы считаем, что каждый параллельный объект - это уникальный процесс, независимо от поведения человека или оборудования. Эти процессы имеют общие переменные с процессом контроллера ПЛК. Это необходимо сделать для обеспечения параллелизма системы. Во второй части этой статьи мы говорили о том, что все параллельные сущности моделируются как автоматы. Автомат означает переход из одного состояния в другое. Для формирования состояния сущности мы используем порты I. В качестве переходов используем операторы goto (как в языке ассемблера). Простой пример выглядит следующим образом:
Статус A:
атом{
если
:: Q1 -> {IB, goto StateB}
:: Q2 -> {IC, goto StateC}
Филиппины;}
/* StateA - метка состояния A
Q1 и Q2 - условия переноса
IB - установить значение состояния на значение состояния B
goto StateB means jump to state B */
3) The property code is a rule that the PLC system must comply with. We use an LTL (Linear Time Logic) formula as input format. We should write the opposite property because of the mechanism of SPIN. SPIN will find that our case property happens; that should be a counterexample. We cannot write the LTL formula directly but use the ing macro. First, we should define all propositions.
В макросе на языке LTL (например, #define p i5 == 0) мы используем определенную пропозицию для формирования LTL-формулы. Spin может автоматически преобразовывать LTL-формулы в коды PRO MELA с помощью команды “SPIN-f” (подробнее см. в руководстве SPIN).
4) Механизм ожидания уведомлений
In the modeling discussion, we recommend not adding a time wait mechanism. This mechanism also needs to be reflected in the code. The specific implementation is to sign a bit variable of each non-PLC process (except all process PLC controllers) as a signal. When the automaton transitions to a state label, the signal variable is set to 0, and the next assignment requires this variable to be 1 to continue. This process continues due to PROMELA syntax features. There is no such restriction in the PLC process. Instead, the PLC process can set these variables to 1, thereby ensuring that each step must be completed through at least one PLC scan. This is called a notification waiting mechanism. Following the four steps above, we get a complete SPIN input file for our system. Then we can use SPIN.
Check the model. For a step-by-step checker of the SPIN model, see the SPIN manual (visit www.spinroot.com). SPIN will give the result of whether a counterexample is found. We can use theory to analyze the tracking file given by SPIN mentioned above.
Using this detection mechanism, we developed a tool for model checking, PLC-checker. It facilitates the establishment of visual models and implementations of inspections and allows for simple analysis of the results. Of course, the counterexample it finds should be checked manually to determine whether it is a true counterexample. However, with the help of trail files, this is not a very difficult task. We also successfully used some PLC checkers (shown in the next section). In the classic textbook example, a counterexample was found. Although the probability of counterexamples is very low, they do occur and can have serious consequences. This tool also proves the correctness and validity of the theory of this article.
5. Запустите программу PLC-Checker
Мы продемонстрируем эффективность PLC-проверяющего устройства при проверке модели канала с двумя воротами следующим образом. Для того чтобы отгородить помещение от внешнего мира, используется двухдверный проход. Введя в инструмент лестничную диаграмму и параллельные сущности, которые являются определением свойств, мы выполняем проверку. На рисунке 3 показаны результаты. Как мы видим, в результатах есть ошибка. Это подтверждается проверкой подсказок, которые являются реальным контрпримером для ручного архивирования. То есть наш механизм эффективен при проверке подобных ПЛК-программ.
6. In conclusion
We study the modeling and checking theory of PLC using formal methods in this paper. The requirements analyze the characteristics of PLC modeling and establishes a concurrent entity model through a time interval strategy. We then prove that the time interval model is a superset of PLC systems and reduce the model by adding a time-free waiting mechanism. It also ensures that all changes to the system can be scanned by the PLC controller. We discovered that we can find errors in a system by examining its counterexamples. Finally, the use of SPIN to check the model is given. There is also a corresponding introduction to the model-checking tool PLC-Checker. At this stage, the mechanism still has many imperfections, such as its handling of timers. But it has great and unique advantages for solving state exploration problems. We are still actively exploring such issues.
