Télécharger l’Atelier B
ATELIER B
L’Atelier B est distribué gratuitement depuis ce site, au travers de sa version communautaire, à tous ceux désirant utiliser l’Atelier B à des fins de recherche, d’enseignement et de développement de projets industriels. Elle est attribuée dès la première utilisation de l’outil pour une durée illimitée. (voir la licence du logiciel).
L’Atelier B comprend tous les outils permettant de développer un projet industriel. Il est disponible sous WINDOWS, MAC et LINUX.
Les utilisateurs, les sociétés ou organismes de recherche et d’enseignement peuvent souscrire à un contrat de maintenance pour obtenir les versions intermédiaires (correctives ou avec de nouvelles fonctionnalités). Le contrat peut être obtenu sur demande à l’adresse atelierb (at) clearsy (dot) com
GUIDE D’INSTALLATION
> Guide d’installation – En Anglais au format PDF
ATELIER B 24.04.2
COMMUNITY EDITION
> Atelier B 24.04.2 – Windows 11 (fonctionne aussi avec 10)
> Atelier B 24.04.2 – Linux Debian 11
> Atelier B 24.04.2 – Linux Debian 12
> Atelier B 24.04.2 – Linux Fedora 39
> Atelier B 24.04.2 – Linux Ubuntu 22.04
> Atelier B 24.04.2 – Linux Ubuntu 23.10
> Atelier B 24.04.2 – Linux Ubuntu 24.04
> Atelier B 24.04.2 – Linux Ubuntu 24.10
> Atelier B 24.04.2 – MacOSX X86-64 (jusqu’à MacOSX 15.0)
> Atelier B 24.04.2 – MacOSX ARM64 (jusqu’à MacOSX 15.0)
ATELIER B 24.04
CLEARSY SAFETY PLATFORM
> Atelier B 24.04 CSP – Windows 11 (fonctionne aussi avec 10)
> Atelier B 24.04 CSP – Linux Debian 11
> Atelier B 24.04 CSP – Linux Debian 12
> Atelier B 24.04 CSP – Linux Ubuntu 22.04
> Atelier B 24.04 CSP – Linux Ubuntu 23.10
> Atelier B 24.04 CSP – Linux Ubuntu 24.04
ATELIER B 4.7.1
COMMUNITY EDITION
> Atelier B 4.7.1 – Windows 11 (fonctionne aussi avec 10)
> Atelier B 4.7.1p1 – Linux Debian 64 Bits (jusqu’à Ubuntu 20.2)
> Atelier B 4.7.1p1 – Linux Universal (zip) (jusqu’à Ubuntu 20.2)
> Atelier B 4.7.1 – MacOSX (jusqu’à MacOSX 11.0)
ATELIER B 4.5.1
COMMUNITY EDITION
> Atelier B 4.5.1 – Windows 11 (fonctionne aussi avec 10)
> Atelier B 4.5.1 – Linux Debian 64 Bits (jusqu’à Ubuntu 18.3)
> Atelier B 4.5.1 – Linux Universal (zip) (jusqu’à Ubuntu 18.3)
> Atelier B 4.5.1 – MacOSX (jusqu’à MacOSX 10.15)
ATELIER B 4.2
COMMUNITY EDITION
> Atelier B 4.2 – Mac OS X
> Atelier B 4.2 – Linux Debian 64 Bits
> Atelier B 4.2 – Linux Debian 32 Bits
HISTORIQUE DES EVOLUTIONS
4.7
- Atelier B supporte macOS 11.0 « Big Sur »
- L’ajout d’un mécanisme extensible permettant l’intégration sans recompilation de prouveurs externes (CVC4 et Z3 par défaut), afin d’améliorer les performances de preuve automatique. Cette version est utilisée industriellement par Alstom, RATP et Siemens Transportation Systems.
- L’amélioration du support du B événementiel pour la certification Critères Communs
- Plusieurs améliorations de l’interface utilisateur des prouveurs automatiques et interactifs
- De nouvelles options permettent de particulariser le comportement du nouveau générateur d’obligations de preuve
- Le manuel du B événementiel (ou Event-B) est disponible en Anglais dans la section Aide/Manuels
4.3
- Vérification des règles de codage dans les modèles B.
- Intégration du model-checker ProB dans l’interface interactive du prouveur.
4.6
- Atelier B CSSP : modélisation B et programmation d’applications pour le starter kit SK0 de la CLEARSY Safety Platform
- L’Atelier B prend désormais en charge macOS 10.15 » Catalina « .
- Preuve interactive
- Les preuves sauvegardées peuvent maintenant être rejouées jusqu’à la première commande défaillante
- La User Pass peut maintenant être sauvegardée dans le fichier patchprover.
- Gestion de projet
- Amélioration de l’utilisation de MANIFEST
- Les fichiers MANIFEST peuvent maintenant être utilisés via la console.
- Traducteur
- C4B : ajout de la traduction des tableaux indexés par une énumération.
- B2C : contrôle sur l’initialisation des tableaux
- Vérification des preuves
- Utilisation des nombres réels
- Il est maintenant possible d’ajouter uniquement la règle validée par PP
- NPOG
- Event-B : ajout du mot clé WITNESS
- Consolidation de la génération des OP
- Ajout du manuel de paramétrage du générateur d’obligations de preuve
4.2
- Support 64 bits complet
- Un nouveau générateur d’obligations de preuve traçable et générique
- Une meilleure intégration des nombres réels et à virgule flottante
- Des accesseurs ajoutés à BART afin de résoudre les conflits de raffinement
- Réglage fin de la traduction booléenne et entière dans le générateur de code C4B
- Ajout d’un serveur de preuve, afin d’accélérer la preuve.
4.5
- Installation simplifiée sous Linux (Universal Installer)
- Pour le B événementiel, des obligations de preuve spécifiques peuvent être générées par le nouveau générateur d’obligations de preuve : absence de blocage, non-divergence, faisabilité, couverture et exclusivité.
- Outil d’interfaçage » IAPA » (Linux uniquement) pour se connecter avec les prouveurs de la plateforme Why3
- Preuve interactive
- Utilisation les solveurs SMT pour définir les règles de preuve s’appliquant au but courant.
- Ajout de ses propres groupes de commandes de preuve
- Amélioration de la typographie des commandes de preuve
- Le générateur de code C4B supporte maintenant les tableaux indexés par des variables de type énuméré.
4.1
- Support amélioré des nombres entiers : la valeur maximale implémentable (MAXINT) peut être de 16, 32 ou 64 bits, les littéraux entiers ne sont pas bornés (BigINT).
- Support expérimental des nombres réels
- Support expérimental des nombres à virgule flottante
- Support des littéraux hexadécimaux.
- Nouveau générateur de code C, C4B, avec profil de traduction et création de makefile.
- Localisation du logiciel en anglais, français, japonais et portugais.
- Support de l’Unicode. Les chaînes de caractères et les commentaires peuvent contenir des caractères non ASCII.
- Ajout d’une vue graphique de l’état des composants
- Exécution parallèle des tâches de preuve
- Amélioration de l’éditeur intégré
- Le prover interactif affiche les buts en attente
- Génération d’obligations de preuve de couverture et d’exclusivité
- Outil de validation des règles mathématiques ajoutées par l’utilisateur
- Vérification orthographique des commentaires du modèle B
- Les règles mathématiques affichées dans la vue « Liste des théories » sont triées en fonction de leur applicabilité
- L’éditeur de modèle B informe l’utilisateur lorsque le fichier édité a été modifié sur le disque.
- Ajout d’une fonction de recherche « à la grep »
- Les règles ajoutées lors de l’utilisation de la commande « pc » sont maintenant affichées.
4.4
- Obligations de preuve affichées dans l’éditeur de modèle.
- Une nouvelle commande de preuve pour Apply Tactic.
- Un délai d’attente configurable pour les commandes de preuve de la famille pp.
- Nouvelles fonctionnalités pour le validateur de règles de preuve.