An Invariant Preserving Transformation for PLC Models

Many applications in the industrial control domain are safety-critical. A large number of analysis techniques to guarantee safety may be applied at different levels in the development process of a Programmable Logic Controller. The development process is typically associated with a tool chain comprising model transformations. The preservation of safety properties in model transformations is necessary to achieve a safe system. Preservation can be guaranteed by showing that invariants are preserved by transformations. Adequate transformation rules and invariant specification mechanisms are needed for this. We report on a transformation from Sequential Function Charts and Function Block Diagrams of the IEC 61131-3 standard to BIP. Our presentation features a description of formal syntax and semantics of the involved languages. We present transformation rules for generating BIP code out of IEC 61131-3 specifications. Based on this, we establish a notion of invariant preservation between the two languages.