La nouvelle version 4.4.2 de l’AtelierB est disponible

Cette version contient de nombreux correctifs et plusieurs améliorations. La fonctionnalité le plus marquante est une fonction de visualisation et de gestion des obligations de preuves qui est directement dans l’éditeur de modèle. On retrouve aussi deux nouvelles capacités pour la preuve interactive ainsi qu’un enrichissement de l’outil de gestion des règles de preuves.

Un site publique de gestion de tickets pour l’AtelierB

Avant de lister les améliorations, voici une nouvelle importante : il y a maintenant un site web public de gestion des tickets accessible à https://projets-clearsy.com. Vous trouvez sur ce site un projet nommé « AtelierB report » où il est possible de consulter les tickets de bugs ou les demandes d’améliorations ainsi que de créer les vôtres.

L’accès à cet outil est protégé par une identification, pour y avoir accès vous devez d’abord créer un compte sur https://projets-clearsy.com/account/register puis vous déclarer par email à report@atelierb.eu. Merci d’indiquer si vous un utilisateur de l’édition communautaire ou de l’édition de maintenance. Nous validerons ensuite votre compte et vous serez en mesure d’accéder à « AtelierB report » à https://projets-clearsy.com/projects/ratb.

Nous sommes très heureux de pouvoir recevoir vos demandes tant de correction que d’amélioration car c’est la seule manière pour nous d’orienter le développement de l’AtelierB vers vos besoins effectifs.

Gestion des obligations de preuve dans l’éditeur de modèle

Il y a maintenant une nouvelle possibilité d’explorer la relation entre un modèle B et ses obligations de preuves (OP). Vous pouvez en effet visualiser directement les OP le long du texte source directement dans l’éditeur. Cette possibilité provient des informations de traçabilité des formules que gère le nouveau générateur d’obligation de preuve.

Cette fonction doit être activée dans les préférences de l’éditeur, comme elle peut être lente sur de gros modèles. Une fois ceci fait, deux colonnes apparaissent le long du texte et donnent l’état des OP associées aux lignes visibles d’un part et associées globalement au modèle d’autre part. Le statut de preuve est représenté par des couleurs et il est possible  de regarder une OP particulière en détail.

 

Quand le modèle est modifié, l’AtelierB lance la régénération des OP ainsi que leurs preuves en mode automatique. Il est ainsi possible de travailler complétement dans l’éditeur tant que la preuve interactive n’est pas nécessaire !

Il est aussi possible d’exploiter la traçabilité complète des formules, c’est-à-dire que vous pouvez vérifier quelles parties du modèle influent sur une PO simplement en sélectionnant le texte du modèle. Il est aussi possible de faire l’inverse en sélectionnant une partie de l’OP afin de visualiser de quelles parties du modèle les formules proviennent. Ces deux fonctions constituent un puissant outil pour comprendre comment les propriétés d’un modèle B sont prouvées (ou réfutées).

Améliorations pour la preuve

Deux nouvelles fonctions pour la preuve interactives ont été implémentées.

Il a toujours été possible de limiter précisément le temps d’exécution du prouveur « PP » en ajoutant un paramètre dans la commande textuelle. Maintenant cela est aussi systématiquement fait avec les commandes de l’interface graphique et il est possible de régler le temps avec la valeur numérique qui se trouve à côté des icônes de lancement. Ceci est important pour limiter le temps de rejeu global d’un projet car le prouveur « PP » peut être lent à s’arrêter.

La deuxième amélioration est la possibilité d’écrire des suites de commande de preuves dans une nouvelle section appelée « User_Tactic » du fichier « PatchProver ». On peut ensuite lancer ces sortes de macro de preuves avec la nouvelle commande « at » (Apply Tactic) durant la preuve interactive. La commande « at » en elle-même disparait de l’historique de preuve en faveur de son contenu. Cela permet de ne pas introduire de problème de rejeu de preuve en cas de modification de la section « User_Tactic ».

Nouvelles possibilités pour l’outil de gestion des règles de preuves (seulement pour l’édition avec maintenance)

Dans l’édition avec maintenance de l’AtelierB se trouve un outil pour aider à démontrer  et valider les règles de preuves qui sont écrites pour rendre possible et rapide la preuve d’un modèle B. Cet outil permet de gérer efficacement le grand nombre de règles de preuve que l’on trouve dans les projets industriels.

Cette nouvelle version apporte une meilleure gestion des règles dupliquées d’un projet. Pour des raisons techniques, une même règle est souvent copiée dans plusieurs fichiers de composant et l’outil peut maintenant trouver automatiquement cet ensemble de règles identiques et permet de les traiter toutes avec une seule action de l’utilisateur.

A été ajouté également un nouveau type de rapport qui présente dans un fichier l’ensemble des règles qui nécessitent encore d’être travaillées. L’outil peut aussi maintenant rechercher et supprimer un ensemble de règles (théories) inutilisé.  Finalement l’outil a une meilleure fonction de tri et d’étiquetage des règles considérées comme invalides lors du travail de vérification.

Pour toute information complémentaire sur les nouvelles fonctions, vous pouvez consulter les notes de version. Vous pouvez aussi contacter directement l’équipe de l’AtelierB à contact@atelierb.eu.

Plus de détails dans la note de version