Dans les domaines critiques d'application de l'informatique, il peut Aatre vital de disposer d'un gA(c)nie logiciel qui soit capable de garantir le bon fonctionnement des systA]mes produits. Dans ce contexte particulier, la mA(c)thode B A(c)vA]nementielle promeut le dA(c)veloppement de modA]les abstraits du systA]me A concevoir et l'utilisation de dA(c)monstrations formelles ainsi que de la relation de raffinement entre les modA]les. Notre but est de pouvoir travailler sur des systA]mes ayant des aspects temporels quantitatifs. C'est ainsi que nous proposons l'introduction des contraintes de...