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 - Fernández Adiego, B. ED - Corvetti, Lou ED - Riches, Kathleen ED - Schaa, Volker RW TI - PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques 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 - Model checking is a promising formal verification method to complement testing in order to improve the quality of PLC programs. However, its application typically needs deep expertise in formal methods. To overcome this problem, we introduce PLCverif, a tool that builds on our verification methodology and hides all the formal verification-related difficulties from the user, including model construction, model reduction and requirement formalisation. The goal of this tool is to make model checking accessible to the developers of the PLC programs. Currently, PLCverif supports the verification of PLC code written in ST (Structured Text), but it is open to other languages defined in IEC 61131-3. The tool can be easily extended by adding new model checkers. PB - JACoW CP - Geneva, Switzerland SP - 911 EP - 914 KW - PLC KW - software KW - controls KW - framework KW - background DA - 2015/12 PY - 2015 SN - 978-3-95450-148-9 DO - 10.18429/JACoW-ICALEPCS2015-WEPGF092 UR - http://jacow.org/icalepcs2015/papers/wepgf092.pdf ER -