2.11.14 PDC/Evaluación: Métodos Formales

Temas:
Core

• 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):
Core:

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]