Formal modeling and verification of PLC systems become paramount in engineering applications. This paper presents a novel PLC domain-specific modeling language Edola. Important characteristics of PLC embedded systems, such as reactivity, scan cycling, real-time and property patterns, are embodied in the language design. Formal verification methods, such as model checking and automatic theorem proving, are supported in Edola modeling. The TLA+ specification language constitutes an intermediate language layer between Edola and the verification tools, enhancing a large degree of reusability. A prototype IDE for Edola and its seamless integration of a model checker TLC and an automatic theorem prover Spass for verification are implemented. A case study illustrates and validates the applicability of the language.