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

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.