Towards a Property Preserving Transformation from IEC 61131-3 to BIP.

link: http://arxiv.org/abs/1009.0817
Abstract

We report on a transformation from Sequential Function Charts of the IEC
61131-3 standard to BIP. Our presentation features a description of formal
syntax and semantics representation of the involved languages and
transformation rules. Furthermore, we present a formalism for describing
invariants of IEC 61131-3 systems and establish a notion of invariant
preservation between the two languages. For a subset of our transformation
rules we sketch a proof showing invariant preservation during the
transformation of IEC 61131-3 to BIP and vice versa.