Formal Specification Of A Safe Plc Language And Its Compiler

We present a language for programmable controllers (PLC) that conforms to the International Standard IEC 1131. This language has a fully formalized syntactic and semantic definition. Moreover, there is also a formal definition of the machine-oriented target language such that the whole compilation process is rigorously specified. The availability of these formal definitions also allows early prototyping and systematic testing on several levels of abstraction. INTRODUCTION Safety-critical applications necessitate high quality in the software production process. One important ingredient for achieving this high quality is the use of well-designed programming languages and adequate support tools, such as compilers. The language design has to be oriented towards the application domain, it must conform to given standards, and it must be easily comprehensible. In order to foster the acceptance of such languages in safety-critical environments, the relevant support tools have to meet high sta..