Verification methods

La vérification d'une application de contrôle-commande développée dans REFLEX Studio a pour objectif de vérifier que l'application est correctement conçue.

Cette vérification s'obtient d'abord par la compilation, puis par une méthode hybride de vérification qui combine la vérification formelle des propriétés désirées, les tests manuels et les tests automatisés.

> Le compilateur

Le langage REFLEX impose la rigueur au programmeur. Il permet une approche synchrone de la programmation de type machines d'états et flots de données.

L'origine du langage est issue d'un compromis entre le besoin de rendre le langage le plus formel possible, de faciliter son utilisation et la volonté de permettre différents types de programmation.

Le compilateur est chargé de vérifier le code écrit et de remonter toute erreur syntaxique et sémantique trouvée.

> La vérification formelle

L'approche de vérification formelle permet de garantir contractuellement l'absence d'erreurs à l'exécution et de prouver le respect de propriétés désirées pour une application à travers des mécanismes de vérification automatique.

Les propriétés s'expriment en utilisant des annotations sur le code, mécanismes natifs de REFLEX pour définir formellement les propriétés attendues. D'une manière générale, ces annotations permettent de décrire des « contrats »  entre le programmeur et l’utilisateur d’un programme, où l’utilisateur s'engage à utiliser le programme en respectant les contraintes du contrat et le programmeur garantit le comportement du programme si l'utilisation s'effectue dans les conditions édictées par le contrat.

Les mécanismes de preuves déductives et formelles sont à la base de la méthode de vérification automatique.

> Les tests manuels

Les tests manuels consistent à vérfier manuellement le respect des propriétés trop complexes pour lesquelles la vérification automatique a échouée ou est impossible. La démarche dans ce contexte consiste à écrire des procédures de test et à les exécuter manuellement.

> Les tests automatisés

REFLEX Studio permet de définir des séries de tests, de rejouer automatiquement ces séries de tests et d'obtenir un rapport sur chacun des tests. Ces tests peuvent correspondre à des tests unitaires au niveau d'un composant (fonctions élémentaires) ou à des tests d'intégration au niveau d'une application.