The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.
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 -