Именно для верифицируемости опесорцный C++ PLC и нужен -> ЧТобы был готовый публично доступный фремворк, в котором ты поднимаешь модель связи, модели всех "PLC" с реальной программой, модели объектов управления и доказываешь, что все это отвечает http://caxapa.ru/720291.html заданным критериям.
SystemC называется. Там все это для целей разработки и верицикации сложной логики давно и успешно решено.