PhD Defense Nicolas Nalpon
From LRDE
Résumé :
Les UIDLs (User Interface Description Languages) sont des langages conçus pour faciliter la conception des interfaces utilisateurs. Ils permettent de se concentrer sur le développement de l’interface utilisateur sans se préoccuper du reste du programme tout en offrant une syntaxe adéquate à leur description. Cependant ces langages sont utilisés dans des domaines critiques, tels que l’aéronautique ou le domaine médical, alors qu’ils ne permettent pas, en l’état, d’apporter les garanties requises pour ce type d’applications critiques.
Dans cette thèse, nous nous questionnons sur les UIDLs spécialisés dans la description des interfaces graphiques et leur utilisation dans les contextes critiques. Notre approche porte sur l’étude de la sémantique de ces langages et de leur formalisation. Les sémantiques des UIDLs ont été peu étudiées dans la littérature et pourtant, leur formalisation pourrait permettre de vérifier l’ensemble des interfaces descriptibles. Nous présentons des propriétés communes aux UIDLs afin de réfléchir sur la façon de les formaliser.
Pour répondre à cette question, nous proposons d’utiliser, les bigraphes de Robin Milner, un formalisme mathématique permettant de modéliser un système évoluant en espace et en temps. Nous montrons que la théorie des bigraphes est adéquate pour la formalisation de la sémantique des UIDLs et définissons un UIDL ayant pour fondement théorique les bigraphes. La définition d’un tel UIDL permet de l’utiliser en tant que langage intermédiaire pour la compilation d’autres UIDLs et par son intermédiaire, de vérifier des interfaces graphiques. Nous validons notre approche en compilant le langage Smala, un UIDL utilisé dans le domaine de l’aviation, vers l’UIDL défini et en vérifiant certaines propriétés sur des exemples d’interfaces.
Mots clés : langage de description d'interface graphique, bigraphe, sémantique formelle
Abstract:
UIDLs (User Interface Description Languages) are programing languages specifically designed to simplify the creation of user interfaces. These languages enable developers to concentrate on interface design while providing an optimised syntax for describing interfaces without worrying about other aspects of the program. While, these languages are used in critical domains such as aeronautics or medicine, where their current state does not offer the necessary safety and reliability guarantee.
In this study, we explore specialised UIDLs for describing graphical interfaces and their use in critical contexts. Our approach focuses on analysing the semantics of these languages and their formalisation. The semantics of UIDLs have not been extensively studied in the literature, and yet their formalisation could facilitate the verification of all possible interfaces. We identify common properties of UIDLs and explore ways to formalise them.
In order to formalise these languages, we propose using Robin Milner's bigraphs, a mathematical formalism that models a system's evolution over time and space. We demonstrate that the theory of bigraphs is suitable for formalising the semantics of UIDLs, and we define a UIDL with bigraphs as its theoretical foundation. This definition enables us to use the UIDL as an intermediate language for compiling other UIDLs and testing graphical interfaces. We validate our approach by compiling the Smala language, a UIDL used in the aviation domain, to the defined UIDL and verifying certain properties on interfaces.
Keywords: user interface description languages, bigraphs, formal semantics
Composition du Jury :
- Sylvain CONCHON, Reviewer, Professor, Université Paris-Saclay
- Christine TASSON, Reviewer, Professor, Sorbonne Université
- Timothy BOURKE, Examiner, Associate Professor, INRIA - École Normale Supérieure Paris
- Frédéric DABROWSKI, Examiner, Associate Professor, Université d'Orléans
- Célia MARTINIE, Examiner, Associate Professor, Université Toulouse III - Paul Sabatier
- Xavier THIRIOUX, Examiner, Professor, ISAE-SUPAERO
- Pierre-Loïc GAROCHE, Supervisor, Professor, ENAC
- Célia PICARD, Co-supervisor, Associate Professor, ENAC
- Cyril Allignol, Invited, Associate Professor, ENAC