Flash Info
La date de clôture de l’étape 1 de l’AAPG2022 est reportée au mardi 2 novembre 2021, 17h.
CE25 - Réseaux de communication multi-usages, infrastructures de hautes performances, Sciences et technologies logicielles

Enrichissement de EventB et de RODIN : EventB-Rodin-Plus – EBRP-EventB-Rodin-Plus

Résumé de soumission

Le développement de systèmes complexes à logiciel prépondérant nécessite la conception de modèles de systèmes correspondant à différentes vues de ce système dans différents domaines d’analyse. La conception de ces modèles nécessite des connaissances spécifiques issues de plusieurs disciplines scientifiques. Par exemple, dans le cas de systèmes autonomes, la modélisation de comportements et d’interactions de systèmes requiert des concepts issus de la théorie du contrôle tels que des équations différentielles, des protocoles de communication ou d’allocation de ressources, des règles pour le contrôle d’accès etc.

Les méthodes formelles à base d’état explicite ont prouvé leur efficacité pour développer de tels systèmes . Une des méthodes, ayant obtenu de nombreux succès dans son utilisation, est la méthode Event-B et son environnement de développement RODIN. Ils sont au cœur de la proposition du projet EBRP.
Actuellement, Event-B et RODIN offrent :
- un langage de modélisation, équipé d’une sémantique formelle fondée sur la théorie des ensembles et la logique du premier ordre, permettant de concevoir des modèles à états explicites et d’exprimer des propriétés de systèmes, en particulier la sûreté ;
- une opération de raffinement, explicitement définie, pour modéliser des mécanismes de décomposition/composition permettant de définir des développements incrémentaux, en plusieurs étapes de raffinement, partant d’un modèle abstrait initial pour aboutir à un modèle concret du système en cours de conception ;
- un système de preuve pour prouver les obligations de preuve engendrées à partir des modèles.

Bien qu’Event-B et sa plate-forme RODIN mettent en œuvre le développement de systèmes nécessitant la formalisation de concepts de domaines d’ingénierie (ex. réels, protocoles de communication, classes, calculs de processus, allocation de ressources, contrôle d’accès) absents du noyau d’Event-B, cette formalisation requiert des modèles définis à partir des concepts du noyau d’Evenyt-B (théorie des ensembles, logique des prédicats, arithmétique sur les entiers). Cette chaîne de modélisation est complexe et la réutilisation de modèles et de preuves peut devenir fastidieuse.

L’objectif scientifique de EBRP est de permettre le développement de modèles de systèmes avec Event-B référençant explicitement, dans des théories de domaine, des concepts vus comme des objets de première classe. Il peut être atteint en étendant Event-B et RODIN par des théories de domaine (et des mécanismes d’import/export) formalisant ces différents concepts.

Pour atteindre cet objectif, EBRP promeut l’idée de définir un cadre formel pour étendre Event-B et RODIN avec des théories de domaine (ainsi que des mécanismes d’import/export) qui formalisent différents concepts de domaine. En plus, la consistance de cette extension devra être justifiée.
Ce cadre d’extension défini devra permettre la définition/ l’instanciation/ l’import/ l’export/ l’extension de théories par l’introduction de type de données génériques associés à des opérateurs, des axiomes et des théorèmes. De plus, ce cadre ne doit pas être ad hoc à une théorie particulière, il doit être générique. Enfin, il doit offrir la possibilité de s’assurer de la correction de l’utilisation de ces théories, en particulier leur consistance lorsque plusieurs théories sont utilisées conjointement, ainsi que la correction des preuves réalisées.

EBRP est organisé autour de 4 tâches techniques traitant de la définition de théories de domaine, leur utilisation par des modèles formels, leur utilisation pour des preuves (automatiques) et la validation de l’approche sur des études de cas complexes et variées en thèmes (continu/discret).

Le consortium EBRP est composé d’experts de la méthode Event-B en France et en Europe. L’inventeur des méthodes B et Event-B, Jean-Raymond Abrial a accepté de se joindre à ce consortium.

Coordinateur du projet

Monsieur Yamine Ait Ameur (Institut de Recherche en Informatique de Toulouse)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

University of Duesseldorf / Departement of Computing
LACL Laboratoire d'algorithmique, complexité et logique
Soton University of Southampton / Department of Computing
IRIT Institut de Recherche en Informatique de Toulouse
LORIA Laboratoire lorrain de recherche en informatique et ses applications (LORIA)
LRI Laboratoire de Recherche en Informatique

Aide de l'ANR 587 357 euros
Début et durée du projet scientifique : janvier 2020 - 48 Mois

Liens utiles

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter