La introducción de los dispositivos electrónicos en los hogares ha permitido la automatización de numerosas tareas repetitivas, un mayor confort y una mejor gestión de los recursos. Con la implantación de redes de comunicaciones para interconectar los dispositivos entre sí, se ampliaron las capacidades de automatización y se abrió la posibilidad de proveer servicios operados remotamente. Sin embargo, la enorme variedad de tecnologías involucradas introduce problemas de interoperabilidad que reducen drásticamente el potencial de evolución de dichos servicios. Esta tesis pretende abordar el problema construyendo una infraestructura de soporte capaz de atender las demandas de futuros servicios domóticos de ámbito regional, nacional o incluso supra-nacional. Los aspectos contemplados abarcan la heterogeneidad de las redes domóticas, la escalabilidad, la tolerancia a fallos, la transparencia, la privacidad de las comunicaciones, etc. Se propone la utilización de modelos formales para el diseño de servicios de próxima generación para el hogar, permitiendo la implementación automática de dichos servicios y el análisis automático de propiedades a partir del modelo formal. Se desarrolla un entorno de modelado y ejecución de servicios con características avanzadas, como la ejecución concurrente de servicios complejos descritos utilizando múltiples modelos de computación. Las contribuciones principales abarcan un amplio abanico de áreas: desde el más bajo nivel, como la solución de problemas de escalabilidad hacia abajo mediante objetos distribuidos hardware, hasta la definición de un marco formal para diseño de servicios.