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 WEPGF092: PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques

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 -