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