Compilation or translation is not only an issue at the level of program but also at the level of specification. This talk considers the design of real-time software for Programmable Logic Controllers (PLCs) and discusses questions of correctness and optimization for translations between different semantic models. The need for such translations arises in order to bridge the gap between conceptually clear models on the one hand and computationally feasible models on the other hand.
To exemplify this, the talk considers so-called Constraint Diagrams as formalizations of behavioural requirements and so-called PLC-Automata as design specifications. Both Constraint Diagrams and PLC-Automata are given a formal semantics in the Duration Calculus, a logic for real-time systems. To enable an automatic verification (model-checking) of designs against requirements, translations of Constraint Diagrams and PLC-Automata into Timed Automata are presented. Semantic correctness and optimization of these translations are discussed.
The concepts presented in the talk are implemented in a tool called Moby-RT that besides the above verification facilities also offers a compiler for PLC code generation.