Verification Methods

Limits of conventional quality methods

Conventional quality methods for PLC programs are increasingly inadequate. They cannot ensure readability and maintainability at an affordable cost. Rules are difficult to formalize and exhaustive compliance is impossible to verify. As a consequence they are considered as poor acceptance criteria.

Itris Verification Method

Itris verification method consists in defining formally the properties of a program and then to prove them. There are mainly two kinds of properties:

• Functional properties which describes what the program should do according to its specifications


• Conception properties are related to the architecture and the format of the program. They describe what the program should look like for maintainability and readability purposes

Itris verification method is then based on three concepts:

• Classes are sets of entities existing in the program that have common characteristics called attributes. A class can inherit attributes of another class. A class can also be defined as the union or intersection of two other classes. Entities of the program may belong to several classes. Some classes are predefined such as all variables, all procedures, all modules...


• Rules are properties that the classes should follow. There consist in expressions made of logic operators and the value of the attributes of one or several classes. A rule is considered as verified if the evaluation of the expression is true. Rules allow an easy formalization of both the functional and conception properties. Some rules are predefined such as the number of time a variable can be written, the location in the program where a variable can be written or read...


• Models are the union of all classes and rules of a program, thus representing all properties of the program. A model can be created as the extension of an existing model.
  

These concepts are at the heart of PLC Checker and they allow advanced verification of PLC programs.