Describir: Una Propuesta de Algoritmo Spin / Promela para el Análisis y Diagnóstico de Errores en Diagramas de Secuencia UML