We present an approach to the design of correct real-time software for Programmable Logic Controllers (PLCs), a widespread hardware platform in the area of traffic and automation control [19,26]. Requirements are formulated in a graphical formalism called Constraint Diagrams (CDs) [12]. A CD consists of waveforms that describe the timewise behaviour of observables and of arrows that describe the timed interdependencies between these waveforms. Design specifications are formulated as so-called PLC-Automata [7]. These can be understood as a special class of timed automata that model in an abstract way the cyclic behaviour of PLCs. Programs are formulated in ST (Structured Text), a dedicated programming language for PLCs. PLC-Automata can be easily compiled into ST code.
The semantic link between CDs and PLC-Automata is stated in terms of the Duration Calculus [37], a logic and calculus for specifying realtime behaviour. This enables us to formally establish the correctness of designs with respect to the requirements. The approach is illustrated by a case study defined by an industrial partner engaged in designing railway signalling systems [23]. It is supported by a tool called Moby/plc [11].