Verificación y Validación Formal de Contratos Inteligentes para Blockchain con Alloy - Baigorria, Lorena; Garis, Ana Gabriela; Riesco, Daniel (Anais Estendidos do Latin-American Symposium on Dependable and Secure Computing (LADC), 2025)
Blockchain es la base tecnológica de una nueva forma de realiz-ar transacciones de manera segura en una red descentralizada. Dicha tecnología permite registrar la validez y el origen de los datos, y realizar transacciones de manera digital, compartida, inalterable y sin la intervención de intermediarios. Frecuentemente, las transacciones requieren de lógica automa-tizada. En estos casos, se vuelve necesaria la definición de con-tratos inteligentes, programas de computación almacenados en Blockchain que se ejecutan automáticamente cuando se cumplen condiciones predeterminadas. Los errores en contra-tos inteligentes pueden tener graves consecuencias, especial-mente en ámbitos como finanzas descentralizadas. Una clara definición de las condiciones es esencial; sin embargo, éstas son generalmente descriptas en lenguaje natural por las partes involucradas, lo que conlleva a la ambigüedad de interpretación por parte de los programadores del contrato. Por otro lado, los errores en la programación también pueden derivar a que el contrato no se ejecute como se esperaba. La calidad del contra-to inteligente podría ser mejorada si las condiciones fueran especificadas en UML con OCL, y luego transformadas al len-guaje de modelado Alloy para llevar a cabo la verificación y validación formal a través del método Model Checking. En este artículo, se describe una línea de investigación que propone un modelo para la especificación de contratos inteligentes en UML y OCL, complementado con una transformación automática a Alloy para su verificación y validación. Dicho modelo contribuye a realizar una auditoría más rigurosa de contratos inteligentes antes de despliegue en Blockchain.