Today’s automation industry is driven by the need for an increased productivity, higher flexibility, andhigher individuality, and characterized by tailor-made and more complex control solutions. In the processing indus-try, logic controller design is often a manual, experience-based, and thus an error-prone procedure. Typically, thespecifications are given by a set of informal requirements and a technical flowchart and both are used to be directlytranslated into the control code. This paper proposes a method in which the control program is constructed as a se-quential function chart (SFC) by transforming the requirements via clearly defined intermediate formats. For thepurpose of analysis, the resulting SFC can be translated algorithmically into timed automata. A rigorous verificationcan be used to determine whether all specifications are satisfied if a formal model of the plant is available which isthen composed with the automata model of the logic controller (LC).