\input zb-basic
\input zb-ioport
\iteman{io-port 06086756}
\itemau{Barbosa, Haniel; D\'eharbe, David}
\itemti{Formal verification of PLC programs using the B method.}
\itemso{Derrick, John (ed.) et al., Abstract state machines, Alloy, B, VDM, and Z. Third international conference, ABZ 2012, Pisa, Italy, June 18--21, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-30884-0/pbk). Lecture Notes in Computer Science 7316, 353-356 (2012).}
\itemab
Summary: In this paper we propose an approach to verify PLC programs, a common platform to control systems in the industry. Programs written in the languages of the IEC 61131-3 standard are automatically translated to B machines and are then amenable to formal analysis of safety constraints and general structural properties of the application. This approach thus integrates formal methods into existing industrial processes.
\itemrv{~}
\itemcc{}
\itemut{B method; PLC; safety critical systems; formal methods}
\itemli{doi:10.1007/978-3-642-30885-7\_30}
\end