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 Viñuela, E. AU - Majzik, I. ED - Schaa, Volker RW ED - Costa, Isidre ED - Fernández, David ED - Matilla, Ãscar TI - What is Special About PLC Software Model Checking? J2 - Proc. of ICALEPCS2017, Barcelona, Spain, 8-13 October 2017 C1 - Barcelona, Spain T2 - International Conference on Accelerator and Large Experimental Control Systems T3 - 16 LA - english AB - Model checking is a formal verification technique to check given properties of models, designs or programs with mathematical precision. Due to its high knowledge and resource demand, the use of model checking is restricted mainly to core parts of highly critical systems. However, we and many other authors have argued that automated model checking of PLC programs is feasible and beneficial in practice. In this paper we aim to explain why model checking is applicable to PLC programs even though its use for software in general is too difficult. We present an overview of the particularities of PLC programs which influence the feasibility and complexity of their model checking. Furthermore, we list the main challenges in this domain and the solutions proposed in previous works. PB - JACoW CP - Geneva, Switzerland SP - 1781 EP - 1786 KW - ion KW - PLC KW - MMI KW - software KW - controls DA - 2018/01 PY - 2018 SN - 978-3-95450-193-9 DO - 10.18429/JACoW-ICALEPCS2017-THPHA159 UR - http://jacow.org/icalepcs2017/papers/thpha159.pdf ER -