Raquel Oliveira - Spécification formelle et vérification de systèmes interactifs avec plasticité: applications à la supervision nucléaire

La plasticité fournit aux utilisateurs différentes versions d’une interface utilisateur. Bien qu’elle enrichisse les interfaces utilisateur, la plasticité complexifie leur développement: la cohérence entre plusieurs versions d’une interface donnée devrait être assurée. Cette complexité est accentuée quand il s’agit de systèmes critiques. Les systèmes critiques sont des systèmes dans lesquels une défaillance a des conséquences graves. Étant donné le grand nombre de versions possibles d’une interface utilisateur, il est coûteux de vérifier ces exigences à la main. Des automatisations doivent être alors fournies afin de vérifier la plasticité. La vérification formelle fournit un moyen d’effectuer une vérification rigoureuse, qui est adaptée pour les systèmes critiques. Notre principale contribution est une approche de vérification des systèmes interactifs critiques et plastiques à l’aide de méthodes formelles. Avec l’utilisation d’un outil performant, notre approche permet: (1) la vérification d’ensembles de propriétés sur un modèle du système. Reposant sur la technique de “model checking”, notre approche permet la vérification de propriétés sur la spécification formelle du système. Les propriétés d’utilisabilité permettent de vérifier si le système suit de bonnes propriétés ergonomiques. Les propriétés de validité permettent de vérifier si le système suit les exigences qui spécifient son comportement attendu; (2) la comparaison des différentes versions du système. Reposant sur la technique “d’équivalence checking”, notre approche vérifie dans quelle mesure deux interfaces utilisateur offrent les mêmes capacités d’interaction et la même apparence. Nous pouvons ainsi montrer si deux modèles d’une interface utilisateur sont équivalents ou non. Dans le cas où ils ne sont pas équivalents, les divergences de l’interface utilisateur sont listées, offrant ainsi la possibilité de les sortir de l’analyse. Nous présentons également trois études de cas industriels dans le domaine des centrales nucléaires dans lesquelles l’approche a été appliquée.