Le cadre général des travaux du thème Spécification de systèmes avec la méthode Event-B concerne la spécification, la vérification et le développement de systèmes en utilisant des techniques formelles, principalement la méthode Event-B. Les principales caractéristiques de cette méthode sont l'utilisation de la théorie des ensembles et de la logique du premier ordre comme langage de modélisation, l'utilisation du raffinement pour représenter les systèmes à différents niveaux d'abstraction et l'utilisation des preuves mathématiques pour vérifier la cohérence des modèles et du raffinement. Plusieurs outils de modélisation et d'assistance à la preuve existent, les principaux étant l'AtelierB et Rodin.