Méthodes de vérification

Les classes, les règles et les modèles sont au cœur des méthodes de vérification d’Itris Automation

Contactez-nous pour en savoir plus

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éthode de vérification d’Itris Automation

La méthode de vérification d’Itris Automation 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é.

Classe, Règle et Modèle

  • 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…
  • Les modèles sont l’ensemble de toutes les classes et les règles d’un programme, représentant ainsi toutes les propriétés du programme. Un modèle peut être créé comme l’extension d’un modèle existant.
Vous ne trouvez pas de réponse à vos questions ?
Contactez-nous