Cet ouvrage pr sente une m thode de d veloppement de syst mes automatis s bas e sur les m thodes formelles B et TLA+. Le d veloppement par raffinement est au coeur de la m thode propos e. Un syst me automatis est mod lis par deux composants, un contr l form par le dispositif physique et son environnement, et un contr leur pilotant ce dernier. La premi re contribution de cet ouvrage concerne la proposition d'une approche qui combine le B v nementiel et le langage de mod lisation TLA+ pour la v rification des propri t s de vivacit . Nous d finissons une extension syntaxique et s mantique du B v nementiel permettant d'exprimer des propri t s de vivacit . Dans la deuxi me contribution, nous proposons une approche de d veloppement des syst mes automatis s en utilisant la technique de composition o il s'agit de d velopper conjointement le contr leur et le composant physique qu'il contr le et appliquer le raffinement aussi bien sur le contr leur que le contr l . La derni re contribution porte sur la d finition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des syst mes de production manufacturi re.