Formal verification of graphical properties of interactive systems

Les systèmes critiques, particulièrement aéronautiques, contiennent de nouveaux dispositifs hautement interactifs. Dans ce contexte, les processus de certification décrits dans la DO-178C offrent une place importante à la vérification formelle des exigences de ces systèmes. Cependant, il est difficile avec les méthodes formelles actuelles de vérifier le respect des exigences concernant les éléments graphiques d'une interface telles que la couleur, la superposition, etc. De ce fait, notre objectif est de proposer une approche pour l'expression et la vérification formelle des exigences relatives à la scène graphique des interfaces humain-machine afin de profiter des apports des méthodes formelles dans un processus de développement.Nous avons identifié un premier ensemble d'opérateurs graphiques de base nous permettant de décrire formellement des exigences graphiques. Le langage de programmation réactive Smala, supportant les éléments du format graphique SVG, est notre point d'entrée pour la mise en œuvre de cette étude. En effet, ce langage permet de décrire et d'animer une scène graphique en fonction d'événements d’entrée divers et variés (clic souris, compteur, ordre vocal, etc.). Nous avons conçu et développé un algorithme qui, par analyse statique du graphe de scène enrichi des applications Smala, permet de vérifier des propriétés graphiques exprimées préalablement avec notre formalisme. Le résultat est un système d'équations sur les variables d'entrée du système pour lesquelles la propriété vérifiée est vraie. Ce système d'équations peut alors être résolu par un outil d'analyse symbolique ou par simulation numérique.Comme cas d'étude de nos travaux, nous utilisons le TCAS (Traffic alert and Collision Avoidance System), un système aéronautique ayant pour objectif d’améliorer la sécurité aérienne. Par l'intermédiaire de GPCheck, l'outil implémentant notre algorithme, pour chaque propriété graphique attendue, nous construisons le système d'équations portant sur les variables d'entrée de l'interface.Critical systems, particularly in aeronautics, contain new, highly interactive devices. In this context, the certification processes described in DO-178C offer an important place for formal verification of the requirements of these systems. However, it is difficult with current formal methods to ensure requirements for graphical elements of an interface such as color, overlay, etc., which are not always easy to verify. Therefore, our objective is to propose an approach for the expression and formal verification of requirements for the graphical scene of human-machine interfaces in order to take advantage of the contributions of formal methods in a development process.We have identified a first set of basic graphical operators allowing the verifier to formally describe graphical requirements. The Smala reactive programming language, supporting elements of the SVG graphical format, is our entry point for the implementation of this study. Indeed, this language allows the developer to describe and animate a graphic scene according to various input events (mouse click, counter, voice command, etc.). We have developed an algorithm which, by static analysis of the enriched scene graph with Smala applications, allows the verifier to verify graphical properties previously expressed with our formalism. The result is a system of equations on the input variables of the system for which the verified property is true.This system of equations can then be solved by a symbolic analysis tool or by numerical simulation.As a case study of our work, we use the TCAS (Traffic alert and Collision Avoidance System), an aeronautical system whose objective is to improve air safety. Through GPCheck, the tool implementing our algorithm, for each expected graphical property, we build the system of equations dealing with the input variables of the interface