Верификация моделей программ на процесс-ориентированном расширении языка Structured Text стандарта IEC 61131-3

Процессно-ориентированное программирование — это парадигма, основанная на концепции процесса. Каждый процесс представляет собой конечный автомат. Эта парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) для написания программного обеспечения с поддержкой Индустрии 4.0. Язык poST является многообещающим процессно-ориентированным расширением языка структурированного текста (ST) МЭК 61131-3, предназначенным для обеспечения концептуальной согласованности исходного кода ПЛК с технологическим описанием управляемого процесса. Этот язык сочетает в себе преимущества программирования на основе конечных автоматов со стандартным синтаксисом языка ST. Мы предлагаем трансформационную семантику poST, заданную правилами перевода операторов языка poST в Promela — входной язык средства проверки моделей SPIN. Следуя этим правилам, наш транслятор, основанный на технологии Xtext, строит модель Promela для программы poST.
Основной вклад нашей статьи — это трансформационная семантика poST и метод автоматической генерации кода Promela из программ управления PoST. Полученная модель Promela готова к проверке с помощью системы верификации моделей SPIN на соответствие требованиям к исходной программе poST, выраженных в терминах линейной темпоральной логики LTL. В статье мы приводим обзор связанных работ, а также краткое описание языков poST и Promela. Представленные далее правила трансляции poST в Promela покрывают операторы потока управления, конструкции создания процессов и управления их состояниями, а также операторы для таймаутов. Отдельно определены сервисные процессы для моделирования внешней среды и задания высокоуровневых LTL спецификаций. Затем мы останавливаемся на основных идеях реализации транслятора poST в Promela, и далее иллюстрируем наш подход на примере системы управления потреблением и производством электроэнергии, в том числе из возобновляемых источников.