FORMAL VERIFICATION OF PLC PROGRAMS VIA SMV AND UPPAAL

ŠPRDLÍK, O.; ŠUSTA, R.

Abstract

Formal verification methods check properties of miscelaneous systems. For example, they can be used for validation of Programmable Logic Controller (PLC) programs. Verification of PLC programs can be done by their modelling in a universal verification tool as SMV or Uppaal. This paper proposes a modelling procedure which creates a SMV or Uppaal model of PLC program given as system of logical equations got by the APLCTRANS algorithm. The automaton described by this equation system is an abstraction suitable for modelling in the mentioned tools. Proposed procedure is able to model only programs, which can be proceeded by APLCTRANS, that means all programming facilities cannot be used in the modelled program. Obtained model can lead to lower computational burden than models derived from particular models of program elements (for instance instructions). The procedure is suitable for modelling and verification of short control programs or program fragments and functions.

Coresponding author e-mail: sprdlo1[at]fel[dot]cvut[dot]cz

Session: Information Technologies in Automation