- Un nouveau générateur d’obligations de preuves, traçable et paramétrable
- L’introduction d’un serveur de preuve, pour paralléliser l’effort de preuve
- Une meilleure intégration des types réels et flottants
- Le support complet 64-bit
- Le paramétrage fin des types booléen et entier pour le générateur de code C4B
- L’ajout des accesseurs dans BART permettant de traiter les conflits de raffinement
Plus de détails dans les notes de version de l’Atelier B 4.2.
Depuis sa naissance commerciale en 1994 avec la version 3.2, l’Atelier B a évolué de manière continue grâce à de nombreux projets industriels et de R&D dans les domaines ferroviaire et microélectronique. Avec B pour piloter des trains et ouvrir/fermer des portes palières de quais de métros, des millions de passagers sont transportés en sécurité de par le monde. En 2014, plus de 25% des métros automatisés embarquent du logiciel critique développé avec l’Atelier B.
La frise ci-dessous résume les différentes étapes et transformations qu’a subi l’Atelier B au cours de cette période.
