JACoW logo

Joint Accelerator Conferences Website

The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.


RIS citation export for WEPGF091: A Formal Specification Method for PLC-based Applications

TY - CONF
AU - Darvas, D.
AU - Blanco Vinuela, E.
AU - Majzik, I.
ED - Corvetti, Lou
ED - Riches, Kathleen
ED - Schaa, Volker RW
TI - A Formal Specification Method for PLC-based Applications
J2 - Proc. of ICALEPCS2015, Melbourne, Australia, 17-23 October 2015
C1 - Melbourne, Australia
T2 - International Conference on Accelerator and Large Experimental Physics Control Systems
T3 - 15
LA - english
AB - The correctness of the software used in control systems has been always a high priority, as a failure can cause serious expenses, injuries or loss of reputation. To improve the quality of these applications, various development and verification methods exist. All of them necessitate a deep understanding of the requirements which can be achieved by a well-adapted formal specification method. In this paper we introduce a state machine and data-flow-based formal specification method tailored to PLC modules. This paper presents the practical benefits and new possibilities of this method, comprising consistency checking, PLC code generation, and checking equivalence between the specification and its previous versions or legacy code. The usage of these techniques can improve the level of understanding of the requirements and increase the confidence in the correctness of the implementation. Furthermore, they can help to apply formal verification techniques by providing formalised requirements.
PB - JACoW
CP - Geneva, Switzerland
SP - 907
EP - 910
KW - PLC
KW - controls
KW - software
KW - target
KW - operation
DA - 2015/12
PY - 2015
SN - 978-3-95450-148-9
DO - 10.18429/JACoW-ICALEPCS2015-WEPGF091
UR - http://jacow.org/icalepcs2015/papers/wepgf091.pdf
ER -