Prédicats de représentation pour la vérification déductive
Frama-C est une plateforme collaborative pour l'analyse de programmes écrits en C. Parmi les outils proposés au sein de Frama-C, WP est dédié à la vérification déductive de programme, qui permet la preuve mathématique de propriétés fonctionnelles et l'absence d'erreurs à l'exécution. Cet outil est utilisé depuis des années dans l'industrie.
La logique de séparation est la voie la plus prometteuse pour permettre la preuve de propriétés sur des programmes manipulant des structures de données complexes. Cependant, il est difficile de l'utiliser pour des études de cas industrielles. La principale raison à cela est la difficulté pour l'encoder vers des outils de preuve automatique. Aussi, son utilisation nécessite beaucoup de travail de la part de l'utilisateur.
L'outil WP de Frama-C n'utilise pas la logique de séparation. Un projet de recherche actuel vise à intégrer certains éléments de logique de séparation pour augmenter les performances et les capacité de WP à traiter des structures complexes. Cependant, l'extension proposée ne permet pas de traiter des structures récursives, pour cela les prédicats de représentation de la logique de séparation doivent être ajoutés. Le but de ce postdoc est d'étudier l'intégration de ces prédicats à WP.
Sûreté et assurance des systèmes basés Intelligence Artificielle
Le poste est lié à l’évaluation de la sûreté et à l’assurance des systèmes basé IA (Intelligence Artificielle). Actuellement, pour un système n’utilisant pas des composants d’apprentissage automatique, la sûreté fonctionnelle est évaluée avant le déploiement du système et les résultats de cette évaluation sont compilés dans un dossier de sécurité qui reste valable pendant toute la durée de vie du système. Pour les nouveaux systèmes intégrant des composants d’IA, en particulier les systèmes auto-apprenants, une telle approche d’ingénierie et d’assurance n’est pas applicable car le système peut présenter un nouveau comportement face à des situations inconnues pendant son fonctionnement.
L’objectif du post-doc sera de définir une approche d’ingénierie pour effectuer une évaluation de la sûreté des systèmes basés IA. Un deuxième objectif est de définir les artefacts du dossier d’assurance (objectifs, preuves, etc.) pour obtenir et préserver une confiance justifiée dans la sûreté du système tout au long de sa durée de vie, en particulier pour les systèmes basés IA à apprentissage opérationnel. L’approche sera mise en œuvre dans un framework open-source qui sera évaluée sur des applications industrielles.
Le titulaire du poste rejoindra une équipe de recherche et développement dans un environnement très stimulant avec des opportunités uniques de développer un solide portefeuille technique et de recherche. Il devra collaborer avec des partenaires académiques et industriels, contribuer et gérer des projets nationaux et européens, préparer et soumettre du matériel scientifique pour publication, fournir des conseils aux doctorants.
Application d’une approche IDM à la planification basée sur l’IA pour les systèmes robotiques et autonomes
La complexité de la robotique et des systèmes autonomes ne peut être gérée qu’avec des architectures logicielles bien conçues et des chaînes d’outils intégrées qui supportent l’ensemble du processus de développement. L’ingénierie dirigée par les modèles (IDM) est une approche qui permet aux développeurs de la robotique et des systèmes autonomes de passer d’un paradigme centré implémentation à un paradigme centré connaissances du domaine ce qui permet d’améliorer l’efficacité, la flexibilité et la séparation des préoccupations des différents acteurs du développement de ce type de système. L’un des principaux objectifs des approches IDM est d’être intégré aux infrastructures de développement disponibles de la communauté robotique et systèmes autonomes, telles que le middleware ROS, ROSPlan pour la planification des tâches robotiques, BehaviorTree.CPP pour leur exécution et suivi et Gazebo pour la simulation.
L’objectif de ce postdoc est d’étudier et de développer des architectures logicielles modulaires, composables et prédictibles ainsi que des outils de conception interopérables basés sur des approches basées sur des modèles, au lieu d’être centrées sur le code. Le travail sera réalisé dans le cadre de projets européens tels que RobMoSys (www.robmosys.eu), ainsi que dans d’autres initiatives pour les systèmes robotiques et autonomes sur la planification des tâches basée sur l’IA et leur exécution. Le principal objectif est de réduire les efforts des ingénieurs et de permettre ainsi le développement de systèmes robotiques autonomes plus avancés et plus complexes à un coût abordable. Pour ce faire, le post-doctorant contribuera à la mise en place et à la consolidation d’un écosystème, d’une chaîne d’outils et d’une communauté dynamique qui offriront un cadre unifié de conception, de planification et simulation, d’évaluation de la sécurité et un environnement formel de validation et de vérification.
Application de l’ingénierie des ontologies et des connaissances à l’ingénierie de systèmes complexes
L’ingénierie système basée sur les modèles repose sur l’utilisation de diverses descriptions formelles du système pour effectuer des prévisions, des analyses, des automatisations, des simulations, etc. Cependant, ces descriptions sont principalement réparties dans des silos hétérogènes. L’analyse et l’exploitation de l’information sont confinées à leurs silos et manquent ainsi la vue d’ensemble. Les informations et idées transversales restent cachées.
Pour résoudre ce problème, les ontologies et les techniques d’ingénierie des connaissances offrent des solutions souhaitables reconnues par les travaux universitaires. Ces techniques et paradigmes aident notamment à donner accès à un jumeau numérique complet du système grâce à leurs capacités de fédération, à donner un sens à l’information en l’intégrant aux connaissances formelles existantes et à explorer et découvrir des incohérences grâce aux capacités de raisonnement.
L’objectif de ce travail sera de proposer une approche donnant accès à un jumeau numérique complet fédéré avec les technologies d’ingénierie de la connaissance. Les opportunités et les limites de l’approche seront évaluées sur des cas d’utilisation industrielle.
Maitrise et gestion de l’évolution des modèles
La conception de systèmes de plus en plus complexes nécessite de mettre en place de nouveaux paradigmes pour faire face à tous les nouveaux défis soulevé comme par exemple améliorer la sureté et la sécurité des systèmes, tout en réduisant les temps et le coût de mise sur le marché. Les paradigmes promus par l’ingénierie des modèles, principalement les notions de modèles actifs et de transformations de modèles, sont des solutions efficaces pour traiter de ces questions. Toutefois, tel que souligné par les travaux présentés dans la série d’ateliers internationaux sur les modèle et l’évolution (www.modse.fr), l’évolution des modèles, voire la coévolution des modèles, et la gestion de la cohérence entre les modèles deviennent alors des activités cruciales pour faire face aux changements naturels de tout système. En fait, il y a un besoin croissant pour des techniques plus disciplinés et des outils d’ingénierie sous-jacent pour résoudre les problèmes liés à l’évolution des modèles, comme par exemple, l’évolution du système guidé par le modèle, la différence de modèles, la comparaison des modèles, le refactoring de modèle, la gestion des incohérences, la gestion des versions des modèles, etc.
Dans le cadre de ce projet, le LISE veux en particulier examiner les problèmes liés à l’évolution des modèles sous les deux perspectives suivantes:
- La première question est de permettre aux modeleurs de gérer l’évolution de leurs modèles. On devrait être en mesure de suivre les changements qui ont été effectués dans un modèle en fournissant par exemple un mode de "suivi des modifications" dans l’environnement de modélisation.
- La deuxième question concerne le problème de la gestion des versions du modèle. Les utilisateurs ont besoin ici pour gérer et utiliser plusieurs versions de leurs modèles dans un esprit de collaboration.
Test d’intégration à base d’exécution symbolique pour les systèmes à base de composants
Le sujet concerne la mise en place de techniques de test pour les systèmes à base de composants logiciels. L’objectif est de maîtriser l’explosion combinatoire souvent subie à la phase de génération de test pour de tels systèmes. L’idée directrice des travaux est de tirer partie de la définition récursive des systèmes pour découper la phase de génération de test en plusieurs phases concernant, les composants d’une part, et les mécanismes de communication entre composants d’autre part, dans une logique "diviser pour régner" qui est classique en informatique. Le candidat se basera sur des travaux réalisé dans le laboratoire autour de techniques à base d’exécution symbolique pour la génération de test et l’analyse de comportement.
Interprétation Abstraite d’annotations ACSL
Frama-C est un ensemble d’outils pour l’analyse de logiciels C. Dans Frama-C, différentes techniques d’analyse peuvent être implémentées comme plug-ins (greffons) dans un même cadre. La collaboration entre plug-ins repose en partie sur le langage commun de spécification ACSL. Chaque plug-in est supposé interpréter ACSL au mieux de ses possibilités.
Ce post-doctorat consiste à améliorer la précision de l’analyse de valeurs, basée sur la technique d’Interprétation Abstraite, de Frama-C, pour les constructions qui ne sont pas actuellement traitées. Le traitement de certaines constructions nécessitera la conception d’un ou plusieurs domaines abstraits spécifiques.
http://frama-c.com
http://frama-c.com/value.html
http://frama-c.com/acsl.html