Author: Darvas, D.
Paper Title Page
WEPGF091 A Formal Specification Method for PLC-based Applications 1
 
  • D. Darvas, E. Blanco Vinuela
    CERN, Geneva, Switzerland
  • I. Majzik
    BUTE, Budapest, Hungary
 
  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.  
poster icon Poster WEPGF091 [0.565 MB]  
 
WEPGF092 PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques 1
 
  • D. Darvas, E. Blanco Vinuela, B. Fernández Adiego
    CERN, Geneva, Switzerland
 
  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.  
poster icon Poster WEPGF092 [3.741 MB]