Projet de recherche P6/39 (Action de recherche P6)
Les systèmes à forte composante logicielle comptent parmi les dispositifs les plus complexes jamais construits : il sont soumis à une multitude de spécifications sans cesse changeantes, ils sont composés de nombreux composants hétérogènes et communicant entre eux, ils doivent pouvoir s’adapter rapidement aux changements technologiques, et ils existent
souvent en plusieurs variantes vivant en parallèle.
Lors du développement de tels systèmes, l’utilisation de modèles précis et de méthodes d’analyse rigoureuses est essentielle pour s’assurer que le logiciel satisfera à son cahier des charges et fera preuve des propriétés désirées (p.ex. sûreté, sécurité, fiabilité, consistance). En même temps, dans le but de s’adapter aux changements constants de technologies et de spécifications, ces systèmes doivent être capables d’évoluer au cours du temps, sans mettre à mal leurs propriétés essentielles.
Nos recherches se focalisent sur le développement, l’intégration et l’extension de langages, formalismes et techniques de pointe permettant de modéliser et de vérifier des sytèmes logiciels et de supporter l’évolution de ces systèmes.
Dans ce projet, nous adoptons une définition généraliste de la conception guidée par modèle (Model Driven Engineering, MDE) en tant qu’approche qui promeut l’utilisation de modèles (au sens large) comme éléments de référence dans tous les aspects du génie logiciel, y compris non seulement l’ingénierie de cahier des charges, la conception système, la définition de langages et de plate-formes, la définition de correspondance entre artefacts, mais aussi la modélisation de données, l’analyse de modèles de conception, la spécification d’outils et le développement de familles de produits.
La modélisation et vérification formelle (Formal Modelling and Verification, FMV) apporte une contribution inestimable au MDE, en offrant des outils et techniques pour composer et décomposer les modèles en d’autres modèles, pour détecter et résoudre les inconsistances dans et entre les modèles, pour raffiner, transformer et synthétiser de nouveux modèles tout en préservant leur consistance, pour abstraire des modèles au départ de descriptions plus détaillées et pour construire des méthodes et des outils de vérification.
Une séparation accrue des préoccupations, telle que prônée par la communauté de développement logiciel orienté aspect (Aspect Oriented Software Development, AOSD) est bénéfique à l’évolution des logiciels, en ce qu’elle permet aux différentes préoccupations d’évoluer indépendamment. Paradoxalement, toutefois, la décomposition d’un logiciel selon différentes préoccupations mène à une multitude de modèles différents qui présentent des interactions subtiles et dont la consistance doit être préservée lorsque l’un d’eux évolue. De ce fait, la combinaison de l’AOSD et du MDE introduit des défis supplémentaires.
Par la synergie et la fertilisation croisée de nos expertises cumulées en conception guidée par modèle, modélisation et vérification formelle, évolution logicielle et développement logiciel orienté aspect, nous proposons de faire progresser l’état de l’art dans chacun de ces domaines, en menant :
• Des recherches avancées sur les langages de programmation et de modélisation, qui sont utilisés pour de modéliser et de réaliser les logiciels et pour exprimer les propriétés pertinentes des logiciels développés, tout en permettant et supportant la vérification automatisée de ces propriétés lors du développement initial et suite aux étapes successives de leur évolution.
• Des recherches innovantes sur les méthodes et techniques rigoureuses permettant de construire, de combiner et de vérifier des modèles et des programmes dans un contexte MDE/AOSD. Notre objectif est de fournir des techniques et méthodes efficaces pour transformer les modèles et pour vérifier, garantir ou obtenir la consistance entre les différents modèles par des techniques de vérification capables de passer à l’échelle.
• Des recherches innovantes sur l’évolution de modèles, avec une attention particulière à l’étude de techniques permettant de faire co-évoluer et de restructurer des modèles, et à l’adaptation de techniques de vérification au contexte de modèles évolutifs. Notre objectif est d’offrir un support pour estimer l’impact de changements sur, et synchroniser d’autres modèles avec, un modèle ayant évolué ou ayant été restructuré, et de vérifier de manière incrémentielle les propriétés de modèles ayant évolué, plutôt que de répéter la vérification complète.
Ce consortium rassemble les équipes de recherche belges de premier plan en génie logiciel, avec une excellence scientifique reconnue en conception guidée par modèle, évolution logicielle, modélisation et vérification formelles et développement logiciel orienté aspect. L’objectif à long terme de notre réseau est de renforcer les collaborations existantes et de forger de nouveaux liens entre les équipes participantes, de manière à valoriser et disséminer notre expertise de recherche au niveau européen.
