Semantic characterization of programmable logic controller programs

PLC is widely used in the field of automatic control. To use formal methods to verify the correctness of PLC programs, semantic characterization of PLC programs are needed. Based on the extended λλ-calculus definition, this paper presents a novel semantic modeling of PLC programs. The results lay the solid underpinnings for theorem proving and modeling checking for PLC systems.