Towards a Property Preserving Transformation from IEC 61131-3 to BIP
Jan Olaf Blech, Anton Hattendorf, Jia Huang
TL;DR
This paper presents a formal transformation from IEC 61131-3 Sequential Function Charts to BIP, ensuring the preservation of system invariants through formal syntax, semantics, and proof sketches.
Contribution
It introduces a formal method for transforming IEC 61131-3 to BIP while maintaining system invariants, with proofs for a subset of rules.
Findings
Formal syntax and semantics for both languages
Invariant preservation during transformation
Proof sketches for subset of transformation rules
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Flexible and Reconfigurable Manufacturing Systems