Моделирование, спецификация и построение программ логических контроллеров

Предлагается новый подход к построению надежных «дискретных» ПЛК-программ с таймерами — программирование исходя из задач спецификации и верификации. Для спецификации программного поведения используется язык темпоральной логики LTL. Программирование осуществляется на языке ST по LTL-спецификации. Проводится дискретное моделирование таймера. Новый подход к программированию ПЛК демонстрируется на примере.
Предлагаемый подход к программированию ПЛК обеспечивает возможность анализа корректности ПЛК-программ с помощью метода проверки модели. При программировании требуется соблюдение следующих двух условий: 1) значение каждой переменной должно изменяться не более одного раза за одно полное выполнение программы при прохождении рабочего цикла ПЛК; 2) значение каждой переменной должно изменяться только в одном месте программы ПЛК.
В рамках предлагаемого подхода изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL-формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной.