Los robots colaborativos han experimentado una baja aceptación en aplicaciones, especialmente en la industria. Este hecho ha llamado la atención de investigadores y profesionales, quienes señalan diferentes causas para esta aceptación limitada. Una de las razones principales es la dificultad para converger en métodos adecuados para modelar interacciones colaborativas entre robots y su contexto circundante durante la fase de requisitos. Estas interacciones deben ser recopiladas y modeladas durante la etapa de requisitos para maximizar la creación de valor a través de la colaboración. La verificación formal es necesaria, teniendo en cuenta los riesgos de la interacción humano-robot. Sin embargo, dicho modelado a menudo está ausente en el diseño de robots colaborativos, y elegir un enfoque adecuado sigue siendo un problema abierto. Este documento aborda este problema utilizando un ciclo de requisitos basado en modelos donde la creación de valor se desvincula para proporcionar un análisis directo, posibles optimizaciones y verificación formal. El proceso general se integra con la ingeniería de requisitos basada en modelos del sistema restante. Este enfoque de sistema de servicio se basa en un enfoque de requisitos orientado a objetivos, y se desarrollaron algoritmos específicos para transferir diagramas orientados a objetivos a Redes de Petri para proporcionar verificación formal del proceso. Un estudio de caso ilustra la aplicación del método propuesto en un robot colaborativo utilizado en un entorno hospitalario universitario.