Contact

Télécharger l’Atelier B

 Support et Maintenance 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.

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 .

ATELIER B 4.5.1 COMMUNITY EDITION

ATELIER B 4.2 COMMUNITY EDITION

HISTORIQUE DES EVOLUTIONS

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.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.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.

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.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.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.

Plus d'informations sur "Support et Maintenance Atelier B"

Copy link
Powered by Social Snap