The paper describes a formal method for automatic generation of programs for PLC controllers. The method starts from modeling the desired behavior 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 diagram language. The model is formal, yet readable, and can be verified against the behavioral and safety requirements. The conversion of the model into a program is done automatically, which reduces the need for further program verification.