Étude et comparaison de scénarios de développements formels d'interfaces multi-modales fondés sur la preuve et le raffinement.