Méthodes de Vérification
Limites des méthodes de vérification traditionnelles
Les méthodes traditionnelles visant à assurer la qualité des programmes automates sont devenues inadaptées. Elles ne parviennent pas à garantir des niveaux satisfaisants de lisibilité et de maintenabilité à des coûts raisonnables. Les règles sont difficiles à formaliser et leur vérification exhaustive est impossible. Elles sont donc souvent considérées comme un critère d’acceptation inadéquat.
Méthodes de vérification Itris
La méthode de vérification d'Itris Automation Square consiste à définir formellement les propriétés que doit avoir un programme et, ensuite, à prouver le respect de ces propriétés. Il y a essentiellement deux types de propriétés :
- Les propriétés fonctionnelles décrivent ce que le programme doit faire, en accord avec ses spécifications.
- Les propriétés de conception portent sur l'architecture et la forme du programme. Elles expriment le besoin de qualité de la conception et décrivent ce à quoi le programme doit ressembler avec pour but d'augmenter la lisibilité et la maintenabilité.
La méthode s’appuie ensuite sur un langage déclaratif très simple. Elle est basée sur la théorie des ensembles et la logique du premier ordre. Le principe consiste à regrouper les entités manipulées par le programme en ensembles, et à vérifier que les éléments de ces ensembles respectent des prédicats énoncés sous forme d’assertions ou règles. Les classes et les règles constituent un modèle. Un modèle regroupe l’ensemble des contraintes à la fois fonctionnelles et de conception que doit respecter une application. Classes et règles sont décrites plus amplement ci-dessous :
- Les classes sont des ensembles d'entités ayant des caractéristiques communes appelées attributs. Une classe peut hériter des attributs d'une autre classe. Elle peut également être définie comme l'union ou l'intersection de deux autres classes. Une entité du programme peut appartenir à plusieurs classes à la fois. Certaines classes sont prédéfinies et correspondent aux entités du programme telles que les variables, les procédures, les modules...
- Les règles sont des assertions qui permettent de spécifier des contraintes imposées au programme. Elles sont définies par des expressions logiques sur la valeur des attributs des éléments d'une ou plusieurs classes. Une règle est considérée comme vérifiée si l'évaluation de l'expression est vraie. Les règles permettent d'exprimer formellement de façon intuitive à la fois les propriétés fonctionnelles et celles de conception. Comme pour les classes, certaines règles sont prédéfinies telles que le nombre de fois qu'une variable peut être écrite, les localisations dans le programme où cette variable peut être écrite ou lue...
Ces concepts sont au coeur de PLC Checker et permettent l'utilisation de techniques de vérification avancées.