Pascal André

La préoccupation directrice est de s'assurer de la correction des composants utilisés dans les architectures logicielles. La spécification (on parle aussi de modélisation) est une démarche scientifique qui consiste à élaborer une abstraction d'un système (existant ou non) pour des fins d'étude et de développement. Elle induit des modèles permettant de vérifier mathématiquement les propriétés attendues du système réel et ensuite de le développer par raffinements successifs. Nous étudions dans ce thème les méthodes orientées modèles et leur mise en oeuvre dans les architectures logicielles multiparadigmes. Ces travaux devraient aboutir à moyen terme à la définition de méthodes et d'environnements pour la construction de composants logiciels corrects avec une approche compositionnelle (projet COSTO/Kmelia) [TSI 2011].

Dans ce thème nous nous attelons à l'étude et à l'élaboration de concepts, mécanismes et outils pour modéliser et développer des composants et logiciels de qualité (sûreté, extensibilité, maintenabilité). Par sûreté nous entendons un fonctionnement correct c'est à dire tel qu'il est prevu par les spécifications informelles puis formelles. Nous traitons essentiellement les aspects vérification par la preuve de théorèmes, pendant la construction du système. Avec la méthode B par exemple, cela peut être la preuve qu'un niveau concret correspond bien à un niveau abstrait (raffinement). Dans le cadre d'UML, ces travaux rejoignent les préoccupations du groupe pUML [EBF+ 98,EBF+ 98a] sur la formalisation de la notation UML. Contrairement à la plupart des travaux du domaine, nous ne nous focalisons pas sur une description figée ou complète d'un modèle mais sur des descriptions variant selon le positionnement dans un processus. Notre démarche est décrite dans [André 02] et constitue le chapitre 4 de [AV 03]. La preuve de modèles (model-checking) est l'autre technique de vérification que nous utilisons pour mettre l'accent sur la couverture de propriétés dites de vivacité.

Deux principales actions sont menées dans ce thème : vérification de modèles et concepts, mécanismes et outils multiparadigmes pour les composants logiciels.

BOSCO L'outil Bosco est un générateur de code à deux niveaux. Il est paramétré par des méta-modèles. Il accepte des modèles, décrits dans le méta-modèle, et génère le code associé ; ce code comprend différents traitements à appliquer au modèle, sous forme de visiteurs. Les entrées et paramètres sont des descriptions XMI conformes aux standards de lOMG. Le code généré est pour linstant du code Java, conforme au standard JMI. Bosco est un logiciel libre, accessible sur Internet http://bosco.tigris.org/.

COSTO (COmponent Study TOolkit) est un atelier de conception et de vérification de logiciels à base de composants et de services.
Le langage associé (kmelia) permet de décrire finement les composants et leurs services afin d'en vérifier formellement les propriétés d'assemblage et de correction (cohérence, sûreté, ...).
Description succincte au format pdf et poster au format pdf.
Les travaux récents portent sur le test de composants Kmelia comme le montre le poster .

EV3-Nantes (Lego EV3) recense différentes ressources et différents travaux autour de la modélisation, vérification et génération de code à partir de modèles semi-formels comme UML ou SysML.
Nous proposons une approche globale [MEDI2021], des définitions systématiques de transformation et une implantation de certaines transformation avec ATL, Modisco, Papyrus, AgileJ.
La plateforme cible est un système distribué écrit en Java-EV3 et Java-Android, les communication se font en Wifi et BlueTooth. Cette plateforme est simple mais représentative des différents problèmes à traiter lors de la conception logicielle. Différents cas d'études sont proposés.
Site web associé au projet EV3-Nantes.

Securité La sécurité est un casse-tête pour les responsables de production et les RSSI. On se doit de protégéer les données et leur confidentialité mais ainsi assurer le fonctionnement normal des applications. La sécurité est un vaste domaine qui va du matériel aux applications en passant par les infrastructures de communication. Mais souvent il n’est pas pleinement pris en compte dans le développement et par les développeurs, car il n’est pas considéré comme prioritaire vis-à-vis de l’adéquation au besoin. Les travaux présentés ici reste à une échelle de contribution très modeste. L’idée est bien souvent de définir des modèles de sécurité et de vérifier des propriétés sur ces modèles. Nous abordons ces thématiques dans nos travaux :

• La composition de services (web) pour mettre en place des services de haut niveau pose des problèmes de sécurité lorsque les services appelés sont distants, sur d’autre serveurs et que des droits d’accès sont nécessaire à l’exécution (implicite) de ces services qu’on peut qualifier de tiers car on ne les invoquie pas directement. Nous avons étudié ce problème dans la thèse d’Abdramane Bah [Bah20] pour laquelle on se place dans une fédération de serveurs .
• La vérification de sécurité des applications mobiles, notamment autour des droits d’accès, car les smartphones contiennent énormément de données personnelles et les utilisateurs peu avertis sur la dangerosité de telle ou telle application téléchargée. Dans la thèse de Mohammed El Amin Tébib [Teb+23a,Teb+23b], nous prenons le point de vue du développeur pour intervenir lors du développement des applications, les développeurs ne sont pas non plus des spécialistes des failles de sécurité du code qu’ils écrivent et ou des frameworks qu’ils utilisent. (git PrivDroid).
  Un cas particulier est la sécurité des applications mobiles en tenant compte du contexte (Projet CASTAV - LCIS-LIG/LS2N (UGA/NU))

L'objectif est de contribuer à améliorer le cycle de développpement et de maintenance des logiciels de contrôle de systèmes de production. Publié dans la série de conférence Sohoma (link)

• Génie logiciel et ingénierie des modèles pour les HMS.
• MPCT, un outils pour la communication hétérérogène par envoi de messages.

RODIC (ANR 2022-2026) Le projet RODIC vise à accélérer le processus de reconfiguration des systèmes de production à la fois d'un point de vue technique et organisationnel par une approche pluridisciplinaires et d'ingénierie des modèles.

Dans cette thématique nous explorons la capitalisation d'informations issues du code pour améliorer la qualité des modèles (preuve de propriétés, co-évolution de systèmes).

• Rétro-ingénierie d'application à composants et services pour prouver des propriétés de sûreté de fonctionnement, projet ECONET financé par Egide.
• Alignement de modèles pour l'architecture d'entreprise (poster, poster outil) avec SodiFrance.

Nous explorons aussi depuis 2020 le problème de la duplication, copie et plagiat de code à travers les modèles.

• Mesure de similarité entre applications au niveau code et modèle.
• Comparaison de modèles pour l'architecture d'entreprise.

Une méthode d’évaluation de la capacité d’accueil des territoires littoraux (Pgm PUCA) a été créée par plusieurs laboratoires de recherche de l’Université de Nantes (Géolittomer LETG UMR 6554 CNRS ; LEMNA, Laboratoire d’Economie et de Management de Nantes Atlantique, EA 4272 et DCS, Droit et Changement Social, UMR 6225 CNRS), en partenariat avec les services de l’Etat (MEDDTL : Ministère de l’Ecologie, du Développement durable, des Transports et du Logement) et testée sur plusieurs territoires-ateliers du littoral des Pays de la Loire. En associant le Laboratoire d’Informatique de Nantes Atlantique (LINA, UMR 6241-CNRS), il s'agit de un outil numérique web au service de la méthode d’évaluation de la capacité d’accueil mise au point.
Le site de l'application ONECAD-EVAL.

• Vote électronique avec Chantal Enguehard.
• Chasseur de SRI avec Chantal Enguehard