Programmable logic controllers (PLCs) represent a typical class of embedded software systems. They are widely used in safety-critical industrial applications, such as railways, automotive applications, etc. The paper presents a novel method to specify and verify PLC software systems with the theorem proving system Coq. Dependent inductive data types are har- nessed to represent the component specifications. Modular and parameterized specification and verification are proposed. An illustrative example demonstrates the effectiveness of the method.