5.45.4.14 Evaluación: Métodos Formales (3 horas) [Habilidades AG-C09,AG-C11]

Referencias Bibliográficas: [Sterling et al., 2024,Pacheco and Malensek, 2021]

Temas

1. Métodos formales de verificación y análisis:
   1. Extensiones a requisitos formales secuenciales como la linealizabilidad.
   2. Especificaciones de protocolo, sesión y transacciones.
   3. Uso de herramientas como Lenguaje Unificado de Modelado (UML), Lógica Temporal de Acciones (TLA), lógicas de programa.
   4. Análisis de seguridad: seguridad y vivacidad en presencia de comportamientos hostiles o con errores de otras partes; propiedades requeridas de mecanismos de comunicación (por ejemplo, ausencia de fugas entre capas), filtrado de entrada, limitación de velocidad. Ver también: Seguridad (SEC) -Foundations.
   5. Análisis estático aplicado a corrección, rendimiento (throughput), latencia, recursos, energía. Ver también: Sociedad, ética y la Profesión (SEP) -Sustainability.
   6. Análisis del modelo de Grafo Acíclico Dirigido (DAG) de eficiencia algorítmica (trabajo, span, caminos críticos).

Aprendizaje esperado (Learning Outcomes)

1. Especificar y medir el comportamiento cuando un servicio es solicitado por un número inesperadamente grande de clientes [Analizar]
2. Identificar y reparar un problema de rendimiento debido a cuellos de botella secuenciales [Analizar]
3. Comparar empíricamente el rendimiento (throughput) de dos implementaciones de un diseño común (quizás usando un marco de pruebas existente) [Comparar]