| Title |
PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques |
| Authors |
- D. Darvas, E. Blanco Vinuelapresenter, B. Fernández Adiego
CERN, Geneva, Switzerland
|
| Abstract |
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.
|
| Paper |
download WEPGF092.PDF [0.407 MB / 4 pages] |
| Poster |
download WEPGF092_POSTER.PDF [3.550 MB] |
| Conference |
ICALEPCS2015, Melbourne, Australia |
| Series |
International Conference on Accelerator and Large Experimental Physics Control Systems (15th) |
| Proceedings |
Link to full ICALEPCS2015 Proccedings |
| Session |
Poster session |
| Date |
21-Oct-15 17:15–18:15 |
| Main Classification |
Software Technology Evolution |
| Keywords |
PLC, software, controls, framework, background |
| Publisher |
JACoW, Geneva, Switzerland |
| Editors |
Lou Corvetti (AS, Clayton, Australia); Kathleen Riches (SLSA, Clayton, Australia); Volker RW Schaa (GSI, Darmstadt, Germany) |
| ISBN |
978-3-95450-148-9 |
| Published |
December 2015 |
| Copyright |
|
