Author: Majzik, I.
Paper Title Page
WEPGF091 A Formal Specification Method for PLC-based Applications 907
 
  • D. Darvas, E. Blanco Vinuela
    CERN, Geneva, Switzerland
  • I. Majzik
    BUTE, Budapest, Hungary
  
  The cor­rect­ness of the soft­ware used in con­trol sys­tems has been al­ways a high pri­or­ity, as a fail­ure can cause se­ri­ous ex­penses, in­juries or loss of rep­u­ta­tion. To im­prove the qual­ity of these ap­pli­ca­tions, var­i­ous de­vel­op­ment and ver­i­fi­ca­tion meth­ods exist. All of them ne­ces­si­tate a deep un­der­stand­ing of the re­quire­ments which can be achieved by a well-adapted for­mal spec­i­fi­ca­tion method. In this paper we in­tro­duce a state ma­chine and data-flow-based for­mal spec­i­fi­ca­tion method tai­lored to PLC mod­ules. This paper pre­sents the prac­ti­cal ben­e­fits and new pos­si­bil­i­ties of this method, com­pris­ing con­sis­tency check­ing, PLC code gen­er­a­tion, and check­ing equiv­a­lence be­tween the spec­i­fi­ca­tion and its pre­vi­ous ver­sions or legacy code. The usage of these tech­niques can im­prove the level of un­der­stand­ing of the re­quire­ments and in­crease the con­fi­dence in the cor­rect­ness of the im­ple­men­ta­tion. Fur­ther­more, they can help to apply for­mal ver­i­fi­ca­tion tech­niques by pro­vid­ing for­malised re­quire­ments.  
poster icon Poster WEPGF091 [0.569 MB]  
Export • reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)