PLC Program Verification and Analysis Using the COQ Theorem Prover
Gang Chen · 2010
The authors analyse a PLC competition quiz machine program and proves a set of properties using the COQ theorem prover.These properties reveal that only half of output states would be reachable and describe the transition relation over these states in an abstract way.Based on these results the authors introduce the notion of logic automata as a complete description of this PLC program.The authors also point out that the program may produce unfair response in rare situations.