Cette thèse propose une approche à la spécification et preuve des propriétés de vivacité<br />avec hypothèses d'équité en B événementiel et présente une sémantique pour ces propriétés<br />fondée sur de points fixes de transformateurs d'ensembles. La proposition utilise une logique<br />de programmation issue de la logique unity pour spécifier et vérifier des propriétés de vivacité<br />sous des hypothèses de progrès minimal et d'équité faible et présente des règles pour préserver<br />ces propriétés dans les raffinements. La sémantique de points fixes nous permet de faire<br />équivalentes les notions d'atteignabilité sous les hypothèses d'équité et de terminaison de<br />l'itération d'événements. Cela nous permet de prouver la correction et la complétude des<br />règles permettant la dérivation des propriétés de vivacité. En outre, cela donne les fondements<br />pour prouver la correction des règles permettant la vérification des propriétés de vivacité et<br />des règles permettant la préservation de la vivacité sous raffinement.