© Springer-Verlag Berlin Heidelberg 2005 Automatic Code Generation for PLC Controllers

Abstract. The paper describes a formal method for automatic generation of programs for PLC controllers. The method starts from modeling the desired be-havior of the system under design by means of a state machine with the ability to measure time and ends-up with a complete program written in a ladder dia-gram language. The model is formal, yet readable, and can be verified against the behavioral and safety requirements. The conversion of the model into a pro-gram is done automatically, which reduces the need for further program verification.