Formal Verification of PLC Programs Using the B Method

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BarbosaD12,
  author       = {Haniel Barbosa and
                  David D{\'{e}}harbe},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {Formal Verification of {PLC} Programs Using the {B} Method},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {353--356},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_30},
  doi          = {10.1007/978-3-642-30885-7\_30},
  timestamp    = {Sat, 19 Oct 2019 20:28:13 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BarbosaD12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}