J'ai continué à travailler dans le domaine de l'ingénierie des modèles en proposant, entre autre, une approche intégrant les diagrammes d'activités UML 2.0 (UML2-AD) et le processus séquentiel communicant (CSP) pour la modélisation et la vérification des systèmes logiciels. Un diagramme UML2-AD est utilisé pour modéliser un système logiciel tandis que CSP est utilisé à des fins de vérification. L'approche proposée consiste en une autre façon de transformer les modèles UML2-AD en modèles Communicating Sequential Process (CSP). Il se concentre également sur la vérification de l'exactitude de certaines propriétés de la transformation elle-même. Ces propriétés sont spécifiées à l'aide de la logique temporelle linéaire (LTL) et vérifiées à l'aide du vérificateur de modèle GROOVE. Cette approche est basée sur le Model Driven Engineering (MDE). La méta-modélisation est réalisée à l'aide de l'outil AToMPM tandis que la transformation du modèle et l'exactitude de ses propriétés sont réalisées à l'aide de l'outil GROOVE. Enfin, nous avons illustré cette approche à travers une étude de cas.