@INPROCEEDINGS{fac06, author = {Benoit Combemale and Alain Caplain and Xavier Cr{\'e}gut and Bernard Coulette and Angel Garcia}, title = {Vers une v\'erification d'un proc\'ed\'e de d\'eveloppement mod\'elis\'e en {SPEM}}, booktitle = {Journ\'ees Formalisation des Activit\'es Concurrentes (FAC, in french)}, address = {Toulouse - France}, month = mar, year = {2006}, irit = {6946}, keywords = {Ing{\'e}nierie des proc{\'e}d{\'e}s, Ing{\'e}nierie des mod{\`e}les, SPEM, Sp{\'e}cification formelle, M{\'e}thode B, OCL.}, url = {http://www.cert.fr/feria/svf/FAC/2006/Papiers/24.pdf}, comment = {slide.pdf}, abstract = { L'OMG a propos{\'e} le m{\'e}ta-mod{\`e}le SPEM pour d{\'e}crire les proc{\'e}d{\'e}s de d{\'e}veloppement. Ce langage semi-formel peut Ítre compl{\'e}t{\'e} par des contraintes OCL pour en pr{\'e}ciser formellement la s{\'e}mantique. Notre objectif est de v{\'e}rifier un tel proc{\'e}d{\'e}. Nous pr{\'e}sentons d'abord une approche qui utilise la m{\'e}thode B, en particulier son raffinement et expliquons pourquoi elle n'a pas {\'e}t{\'e} concluante. Nous indiquons ensuite la voie actuellement suivie qui consiste {\`a}rester sur les standards propos{\'e}s par l'OMG, en particulier OCL. } }