Description du sujet
Un « flux d’événements » peut être défini comme une séquence d’éléments de données arbitraires générés par une entité ou un système. Comme exemples de flux, on peut mentionner des blockchains constituées d’une séquence de blocs générée dynamiquement, des fichiers journaux (logs) dont les lignes sont produites par l’exécution d’un logiciel, ou encore des valeurs brutes émises par des lectures périodiques de capteurs. Le traitement d’un flux d’événements d’entrée se traduit généralement par un autre flux d’événements de sortie, et l’opération peut être connectée en série pour effectuer des calculs complexes sur diverses sources d’événements. Nous appelons « programme de flux » (stream program) tout calcul qui opère sur un flux d’événements pour produire un résultat souhaité: cela inclut les requêtes exprimées dans des langages de traitement de flux d’événements, des extraits de code utilisant des API de traitement de flux d’événements ou des smart contracts opérant sur des éléments d’une blockchain.
Le test et la vérification des programmes classiques font l’objet d’études approfondies depuis des décennies. En revanche, les programmes de flux représentent un nouveau paradigme, où les concepts et les techniques développés pour la programmation impérative ne peuvent pas être directement transférés. L’objectif de ce travail doctoral est de développer la théorie, les techniques et les outils pour le test et la vérification formelle de programmes fonctionnant sur des flux, et en particulier sur des pipelines de traitement de flux définis dans des API telles que le moteur de traitement d’événements BeepBeep (https:// liflab.github.io/beepbeep-3).
Le projet implique à la fois le développement de concepts théoriques liés au test et à la vérification des programmes de flux (en particulier la notion de couverture), le développement de techniques de génération de tests spécifiques aux programmes de flux, la mise en œuvre de ces techniques dans des prototypes, et leur évaluation empirique approfondie. Des premiers résultats prometteurs sur le model checking de tels pipelines ont récemment été publiés [1] et pourraient être utilisés comme point de départ.
Présentation établissement et labo d’accueil
L’Université du Québec à Chicoutimi (UQAC) fait partie du plus grand réseau universitaire au Canada. Elle est située dans la région francophone du Saguenay–Lac-Saint-Jean, réputée pour la beauté de son fjord et la majesté de sa nature environnante. L’UQAC accueille chaque année 6 500 étudiants, dont plus de 1 000 provenant de 50 pays différents. Le programme de recherche en informatique est particulièrement dynamique ; il est l’hôte de deux chaires de recherche du Canada, comprend actuellement une vingtaine de professeurs, 30 doctorants et boursiers postdoctoraux et plus de 100 étudiants à la maîtrise.
Le travail de doctorat se déroulera au Laboratoire d’informatique formelle (https://liflab.ca), sous la supervision du Pr. Sylvain Hallé, titulaire de la Chaire de recherche du Canada sur les tests, la spécifications et la vérification de systèmes informatiques. Le LIF est spécialisé dans l’application de méthodes formelles au test et à la vérification de divers systèmes logiciels. Les projets antérieurs des membres du corps professoral du LIF ont été réalisés en collaboration avec de nombreuses entreprises, dont Ericsson, Industrielle Alliance, Ubisoft LaForge, Devicom et Eckinox Média.
La recherche au LIF est reconnue internationalement et contribue au développement d’outils logiciels concrets et de haute qualité fondés sur des bases mathématiques solides. Les projets notables de longue date développés au LIF incluent le moteur de traitement de flux d’événements BeepBeep 3 [2], le système de surveillance de la blockchain Artichoke [3] et la bibliothèque de lignage de données Petit Poucet [4]. Toutes ces initiatives ont été récompensées et publiées dans des conférences internationales de premier plan au cours de la dernière décennie.
Profil du candidat
Un très bon diplôme de maîtrise universitaire en informatique, informatique de gestion, mathématiques ou dans une discipline connexe est attendu. Nous recherchons en outre les qualifications suivantes:
- Très bonnes connaissances formelles : informatique formelle, théorie des automates, spécification et test de logiciels. Une formation en mathématiques est considérée comme un plus.
- Bonnes compétences en programmation; la connaissance de Java est considérée comme un plus
- Des connaissances en technologie blockchain seront considérées.
- Très bonnes aptitudes à la communication scientifique et à la rédaction.
- Très bonne connaissance de la communication et de l’écriture en anglais.
- Intérêt marqué pour les problèmes scientifiques et motivation à mener une recherche indépendante et ciblée.
L’Université du Québec à Chicoutimi s’engage pour l’équité, la diversité et l’inclusion à toutes les étapes du cursus de ses étudiants; les personnes des groupes sous-représentés sont particulièrement encouragées à postuler. Les candidatures seront évaluées par un panel de trois membres du corps professoral de l’UQAC en se concentrant sur les critères mentionnés ci-dessus. Les personnes sélectionnées dans un premier temps seront convoquées pour un entretien en ligne afin d’évaluer davantage leurs compétences techniques et de communication.
Eléments à fournir pour la candidature
Les personnes souhaitant poser leur candidature doivent fournir les documents suivants:
- Une lettre d’intention, incluant les noms de deux références externes
- Un curriculum vitae complet incluant la liste des publications
- Les copies d’au plus trois publications choisies
- Les relevés de notes de niveau licence (baccalauréat au Canada) et maîtrise
- Une copie du mémoire de maîtrise, si celui-ci est déposé
Références
[1] A. Bédard, S. Hallé. (2021). Model Checking of Stream Processing Pipelines. In Proc. TIME, 5:1-5:17. DOI 10.4230/LIPIcs.TIME.2021.5
[2] S. Hallé. (2018). Event Stream Processing with BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l’Université du Québec, ISBN 978-2-7605-5101-5
[3] S. Hallé, R. Khoury, A. El-Hokayem, Y. Falcone. (2016). Decentralized Enforcement of Artifact Lifecycles. In Proc. EDOC, 1-10. DOI 10.1109/EDOC.2016.7579380
[4] S. Hallé, H. Tremblay. (2021). Foundations of Fine-Grained Explainability. In Proc. CAV, Springer LNCS 12760, 500-523. DOI 10.1007/978-3-030-81688-9_24
Commentaires récents