Módulo gratuito
Métodos formales
Aprende métodos formales con práctica: demuestra reglas con Z3, SPIN, TLA+ y Alloy y lee contraejemplos.
Las lecciones
Cada lección se lee completa y gratis. Crea una cuenta gratuita para ejecutar sus comandos en un laboratorio y hacer sus cuestionarios y tareas.
1 · Laboratorio de máquina virtual
Por qué las pruebas no bastan
Puedo explicar qué garantiza una prueba y qué garantiza una demostración.
Leer la lección2 · Laboratorio de máquina virtual
Cómo comprobar una afirmación con Z3
Puedo preguntar a Z3 si una afirmación se cumple siempre.
Leer la lección3 · Laboratorio de máquina virtual
Encontrar una condición de carrera con SPIN
Puedo encontrar una condición de carrera leyendo la traza que muestra SPIN.
Leer la lección4 · Laboratorio de máquina virtual
Exclusión mutua y cerrojos con SPIN
Puedo escribir un cerrojo y comprobar con SPIN que no tiene errores.
Leer la lección5 · Laboratorio de máquina virtual
Invariantes y contraejemplos en TLA+
Puedo escribir un invariante y leer el contraejemplo cuando un modelo lo rompe.
Leer la lección6 · Laboratorio de máquina virtual
Modelos y contraejemplos en Alloy
Puedo leer un contraejemplo de Alloy y decir qué regla falta en el modelo.
Leer la lección
Con un laboratorio real
Cada lección de este módulo se practica en un laboratorio que se inicia solo para ti. Los laboratorios que usa:
¿Enseñas a una clase? Asigna este módulo a tus alumnos con guía del profesor, tareas con corrección automática y un laboratorio para cada alumno.