| Title |
A Formal Specification Method for PLC-based Applications |
| Authors |
- D. Darvas, E. Blanco Vinuelapresenter
CERN, Geneva, Switzerland
- I. Majzik
BUTE, Budapest, Hungary
|
| Abstract |
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.
|
| Paper |
download WEPGF091.PDF [0.172 MB / 4 pages] |
| Poster |
download WEPGF091_POSTER.PDF [0.569 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, controls, software, target, operation |
| 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 |
|
