Gómez Rojo, Manuel2026-03-192026-03-192026-03-01Gómez Rojo, Manuel. Trabajo de Fin de Máster: Implementación de CoAP verificada formalmente en SPARK/Ada. Universidad Nacional de Educación a Distancia (UNED), 2026https://hdl.handle.net/20.500.14468/32161Este Trabajo Fin de Máster aborda la verificación formal de software como medio de mejorar la ciberseguridad en el ámbito de los dispositivos IoT. Con el objetivo de comprobar la viabilidad y conveniencia de este enfoque, se aplica un proceso de desarrollo seguro en la implementación del protocolo Constrained Application Protocol (CoAP), basándose principalmente en la verificación formal del software escrito en el lenguaje SPARK/Ada. Como parte de la introducción a la verificación formal, se compara este lenguaje con otros que poseen esta característica, como Frama-C o Dafny. También se realiza una breve descripción del protocolo CoAP. En su implementación, se emplean herramientas como GNATprove para demostrar la corrección del código, RecordFlux para la especificación y generación de parsers verificables, y WolfSSL para la seguridad con DTLS. Finalmente, se realiza una validación mediante pruebas de interoperabilidad con servidores CoAP y dispositivos IoT comerciales como el gateway TRÅDFRI. Las conclusiones destacan la viabilidad de la verificación formal para mejorar la ciberseguridad en IoT, pese a su mayor costo inicial.This Master’s Thesis addresses formal software verification as a means to improve cybersecurity in the field of IoT devices. To assess the feasibility and benefits of this approach, a secure development process is applied in the implementation of the Constrained Application Protocol (CoAP), based primarily on the formal verification of software written in the SPARK/Ada language. As part of the introduction to formal verification, this language is compared with others that offer such capabilities, such as Frama-C and Dafny. An brief description of the CoAP protocol is also provided. In its implementation, tools such as GNATprove are employed to demonstrate code correctness, RecordFlux for the specification and generation of verifiable parsers, and WolfSSL for DTLS security. Finally, validation is carried out through interoperability tests with CoAP servers and commercial IoT devices such as the TRÅDFRI gateway. The conclusions underscore the viability of formal verification for enhancing IoT cybersecurity, despite its higher initial cost.esinfo:eu-repo/semantics/openAccess1203.04 Inteligencia artificialtesis de maestríaverificación formalSPARK/AdaCoAPIoTciberseguridadRecordFluxformal verificationSPARK/AdaCoAPIoTcybersecurityRecordFlux