Modélisation en Event-B

Cet ouvrage se concentre sur l'utilisation d'Event-B en tant que méthode formelle pour la modélisation et la vérification de logiciels. Notre étude de cas porte sur le système de commande d'ascenseur (ECS). Les exigences relatives à l'ascenseur sont traduites en modèles mathématiques Event-B. Nous utilisons RODIN pour développer, tester et vérifier les modèles Event-B de l'ECS avant de pouvoir implémenter le système dans un programme logiciel. La modélisation Event-B est si essentielle qu'elle nous permet d'identifier les exigences manquantes, les erreurs dans notre conception et de prouver que le modèle du système fonctionnera comme prévu, contrairement à ce qui se passerait si nous développions un système immédiatement après avoir reçu les exigences du client. Ces exigences sont incomplètes et ambiguës. Grâce à l'utilisation d'Event-B, nous réduisons le coût de développement du système, car les erreurs seront toujours détectées dès les premières étapes du développement. Le passage de la phase des exigences à la phase de spécification formelle est l'une des étapes les plus difficiles. En effet, la construction de modèles initiaux à partir des exigences du système nécessite un haut niveau de compétence et des compétences pratiques en modélisation Event-B. Comme il n'existe pas de processus bien défini pour guider les ingénieurs système, cet ouvrage propose une approche pratique sur la manière de développer de bons systèmes logiciels.