A process calculus approach to correctness enforcement of PLCs