Аннотация:
Проводится обзор методов и подходов к программированию «дискретных» задач ПЛК на примере задачи построения программы управления кодовым замком. Для этих подходов оценивается удобство анализа программной корректности методом проверки модели относительно средства автоматической верификации Cadence SMV. Выявляются возможные уязвимости ПЛК-программ, возникающие при некоторых подходах к программированию ПЛК.
Ключевые слова:программирование логических контроллеров, верификация программ, метод проверки модели.