Où docteurs et entreprises se rencontrent
Menu
Connexion

Vous avez déjà un compte ?

Nouvel utilisateur ?

Mot de passe oublié

Vérification d’un langage informatique réactif orienté interactions et de ses composants

ABG-83725 Sujet de Thèse
14/03/2019 < 25 K€ brut annuel
Logo de
École Nationale de l'Aviation civile
Toulouse - Occitanie - France
Vérification d’un langage informatique réactif orienté interactions et de ses composants
  • Informatique
Vérification, preuve formelle, compilation, programmation réactive, propriétés interactives

Description

Contexte

L'équipe d'Informatique Interactive (LII) du laboratoire de recherche de l'ENAC (Ecole Nationale de l'Aviation Civile) développe une plateforme de modélisation nommée djnn [1]. Djnn permet la conception et l’exécution de logiciels offrant un support pour les interactions humain-machine. Cet environnement comprend smala [2], un langage dédié à la description de ces logiciels (structuration en composants, mécanismes de contrôle, flot de données, gestion des entrées et des sorties…). Compilée puis liée à des librairies spécifiques, une application décrite en smala peut alors être exécutée [6,7].

Le langage smala est réactif : il permet de décrire des applications répondant à des événements externes (inputs utilisateur depuis l’interface, timers, etc…) de manière instantanée. Contrairement aux langages traditionnels, smala repose sur des mécanismes de traitement d’événements, de machine à état et de gestion de flots de données.

Le langage smala partage les mécanismes de base (aspects réactifs, propagation d’activation…) des autres langages réactifs comme Lustre. Son originalité réside dans son côté fortement orienté interaction : il produit une représentation perceptible de son état interne [9, 10]. Ainsi, de nombreux composants sont dédiés à la création, l’importation, la manipulation et l’affichage d’objets graphiques et interactifs.

Par ailleurs, le LII s’intéresse plus particulièrement à la description de systèmes interactifs critiques pour le transport aérien (cockpit, position de contrôle, etc.). Ces systèmes logiciels nécessitent une certification qui est décrite par la norme DO-178C. L’annexe 333 de cette norme préconise en particulier l’emploi de méthodes formelles pour les sous-systèmes les plus critiques et encadre leur pratique.

 

Problématique

La formalisation et la validation de composants interactifs et graphiques est un défi à part entière, non adressé par la littérature. En général, ces composants sont validés de façon empirique par des tests utilisateurs et des recettes, qui sont coûteuses en temps et non exhaustives. Plus généralement, nous nous intéressons à la certification du langage smala et de ses composants afin de pouvoir les utiliser dans des applications embarquées (et en tout premier lieu, l’hélicoptère électrique Volta [7]) ou critiques (comme les logiciels interactifs dédiés au contrôle du trafic aérien [11]) réelles.

 

Démarche proposée

Une première étape de cette certification passe par la validation de la chaîne de compilation du langage smala. Il s’agit de démontrer formellement que le résultat de la compilation correspond bien en tous points au programme passé en entrée du compilateur. Un compilateur C certifié, COMPCERT [4], issu de travaux de recherche, est déjà utilisé en particulier par l’industrie aéronautique. L’idée ici est d’effectuer une première transformation de modèle certifiée de smala vers C puis d’utiliser COMPCERT pour compiler le programme C obtenu. Nous pourrons pour cela nous inspirer de travaux effectués pour la vérification d’un compilateur pour le langage Lustre [5].

Une deuxième étape réside dans la définition de composants interactifs certifiés. Nous nous intéresserons en particulier à la définition de composants assurant, par construction, le respect de bonnes propriétés. Dans cette thèse, nous mettrons l’accent sur des propriétés graphiques comme la non-recouvrabilité d’un objet ou sa visibilité.

Par exemple, il serait intéressant de créer un composant « Alarme » qui garantit qu’aucun autre composant ne pourra être affiché au-dessus ou qu’il ne pourra pas être rendu invisible par des filtres de transparence ou des jeux de couleurs.

Pour assurer le respect de ces propriétés par construction il sera nécessaire de travailler sur la loi de composition des composants et donc la sémantique du langage smala. Le travail sur le compilateur certifié en sera donc impacté. Ainsi, les deux étapes de cette thèse sont intimement liées et évolueront constamment ensemble.

 

Travaux existants

Plusieurs compilateurs smala co-existent (en C, C++, java). Ils restent cependant empiriques et un travail préliminaire sur la formalisation de la sémantique du langage est nécessaire. Ce travail a été amorcé au travers de stages. Ils ont en particulier permis de définir les mécanismes minimaux du langage à partir desquels l’ensemble des autres composants peuvent être définis au travers de bibliothèques.

La partie concernant les composants graphiques n’a cependant pas du tout été abordée. Il faut également poursuivre le travail par la définition d’un compilateur.

Des travaux préalables ont été menés sur la vérification de propriétés interactives telles que le non-recouvrement, sur des programmes djnn [8]. Ces vérifications utilisent des méthodes d’analyse statique sur le graphe représentant un programme djnn : elles sont donc ad-hoc (à revalider à chaque nouveau graphe ou à chaque changement dans le graphe). Il s’agirait ici de proposer des composants assurant ces propriétés par construction.

Enfin, une thèse est en cours dans l’équipe sur les techniques et outils pour l’analyse des systèmes interactifs (fin en septembre 2020). Elle s’intéresse en particulier à la vérification de propriétés graphiques par analyse statique du code smala. Elle comprend un travail sur l’identification préalable de certaines de ces propriétés. Elle constituera donc une base de départ intéressante pour choisir les propriétés à adresser ici.

 

Résultats attendus

Les résultats attendus sont de deux ordres. D’une part la définition et la validation d’un compilateur pour le langage smala, d’autre part la définition de composants smala assurant par construction le respect de bonnes propriétés, en particulier interactives.

L’originalité de ce travail réside dans l’aspect interactif et graphique du langage smala, qui le différencie des autres langages réactifs. Cela requiert de manipuler à la fois des concepts de haut niveau (vérification du compilateur, vérification) et bas niveau (affichage, propriétés graphiques) et à les coupler.

 

Bibliographie

[1] M. Magnaudet, S. Chatty, S. Conversy, S. Leriche, C. Picard, and D. Prun. Djnn/Smala: A Conceptual Framework and a Language for Interaction-Oriented Programming. Proc. ACM Hum.-Comput. Interact. 2, EICS, Article 12 (June 2018)
[2]
http://smala.io
[3] https://coq.inria.fr/
[4] X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009
[5] T. Bourke, L. Brun, P. É. Dagand, X. Leroy, M. Pouzet and L. Rieg. (2017, June). A formally verified compiler for Lustre. In
ACM SIGPLAN Notices (Vol. 52, No. 6, pp. 586-601). ACM.

[6] S. Conversy, J. Garcia, G. Buisan, M. Cousy, M. Poirier, N. Saporito, D. Taurino, G. Frau and J. Debattista. 2018. Vizir: A Domain-Specific Graphical Language for Authoring and Operating Airport Automations. In Proceedings of the 31st Annual ACM Symposium on User Interface Software and Technology (UIST '18)

[7] P. Antoine and S. Conversy, Volta: the first all-electric conventional helicopter, More Electric Aircraft, 2017.

[8] S. Chatty, M. Magnaudet and D. Prun. Verification of properties of interactive components from their executable code. 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2015), Jun 2015, Duisbourg, Germany. ACM, EICS '15 Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp.276-285 2015,

[9] M. Beaudouin-lafon, Designing interaction, not interfaces, Proceedings of the working conference on Advanced visual interfaces , AVI '04, pp.15-22, 2004.
[10] B. A. Myers and M. B. Rosson, Survey on user interface programming, Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, pp.195-202, 1992.

[11] M. Cordeil, T. Dwyer, and C. Hurter, Immersive solutions for future Air Traffic Control and Management, Proceedings of the 2016 ACM Companion on Interactive Surfaces and Spaces, ISS Companion '16, pp.25-31, 2016.

Nature du financement

Contrat doctoral

Précisions sur le financement

Bourse ministérielle EDSYS -- financement assuré

Présentation établissement et labo d'accueil

École Nationale de l'Aviation civile

L'ENAC, École Nationale de l'Aviation Civile est la plus importante des Grandes Écoles ou universités aéronautiques en Europe. Elle comprend un laboratoire de recherche composé de 4 équipes.

 

Le candidat retenu sera intégré dans l’équipe d’Informatique Interactive de l’ENAC à Toulouse. L'aéronautique est un système hybride humain-machine complexe, mettant en oeuvre de nombreux sous-systèmes hétérogènes en interaction. Dans ce cadre, les objectifs de l'équipe consistent à mieux prendre en compte le phénomène de l'interaction et à maîtriser la conception de systèmes interactifs plus performants.

 

L'équipe d'Informatique Interactive est composée de 10 enseignants-chercheurs et ingénieur de recherche permanents.

La thèse sera encadrée par Celia Picard et Sébastien Leriche.

Intitulé du doctorat

Doctorat d'Informatique

Pays d'obtention du doctorat

France

Ecole doctorale

EDSYS

Profil du candidat

Vous êtes titulaire d’un Master 2 (ou équivalent en informatique).

Vous êtes intéressés aussi bien par les aspects formels et théoriques de l’informatique que par les problématiques qui touchent à l’utilisabilité des systèmes et à l’interaction humain-système. Des connaissances en méthodes formelles, preuve de programme (Coq), compilation, programmation fonctionnelle (Caml) ou systèmes interactifs sont un plus.

Vous avez un bon niveau d’anglais. Vous êtes motivé, autonome, curieux et aimez le travail collaboratif.

Vous avez une première expérience en recherche (stage, module d’initiation à la recherche...)

Date limite de candidature

14/04/2019
Partager via
Postuler
Fermer

Vous avez déjà un compte ?

Nouvel utilisateur ?


Mot de passe oublié
Besoin d'informations ?

Vous souhaitez recevoir une ou plusieurs lettres d’information de l’ABG. Chaque mois des actualités, des offres, des outils, un agenda…

item1
item1