Vérification formelle de programmes automates avec la méthode B