Ces recherches se situent à l'intersection des spécifications formelles et de l'approche à objets. Les spécifications formelles s'imposent progressivement comme une condition essentielle à un bon développement logiciel. Leurs avantages sont nombreux : rigueur, preuve, automatisation partielle etc. Par contre leur utilisation dans le domaine industriel reste marginale entre autre par ce qu'elles demandent une formation spécifique et qu'elles sont peu outillées.
L'intégration d'aspects formels (spécifications, modèles formels à objets, preuves, contrôles, transformations de programme, ...) dans le cadre de la programmation par objets, et particulièrement dans les méthodes d'analyse et de conception à objets, est un enjeu important en génie logiciel. En effet ces préoccupations sont à la base d'une bonne inter-opérabilité et de la spécification de composants réutilisables. Les objectifs immédiats sont d'obtenir des concepts, règles, algorithmes, outils que l'on pourra introduire dans les méthodes à objets actuelles : OMT, Fusion, OOD, Shlaer et Mellor, etc. A plus long terme, il s'agit de concevoir et de réaliser un environnement minimum supportant les concepts et les outils mais aussi d'interfacer vers d'autres environnement existants.