| Apunte sobre B (pdf)
|
| Libro sobre B (capítulos 1, 2, 4-7 y 9; pueden obviar todo lo relacionado a "weakest precondition")
|
| Atelier-B, herramienta para escribir especificaciones B
|
| Práctica 1: B (pdf) |
|
|
| Consejos sobre Requerimientos
y Especificaciones (pdf) |
WRSPM - Introducción y
designaciones (pdf)
|
Especificación que mezcla DK con S
|
|
|
Statecharts (pdf)
Stecharts parametrizados (pdf)
| Un problema resuelto con Statecharts
|
| Práctica 2: Statecharts (pdf) |
|
|
| Apunte sobre Communicating
Sequential
Processes (CSP) (pdf)
|
| Problema horno
microondas en CSP (Versión
PDF) |
| Práctica 3: CSP (pdf) |
|
|
| Seguridad, vitalidad y equidad (pdf) |
Libro de Lamport sobre TLA (capítulos 1 al 8)
| Un ejemplo con requisitos
temporales en TLA (pdf)
|
|
| Práctica 4: TLA+ (pdf) |
|
|
| Material opcional
|
| Mail de L. Lamport
contestando algunas preguntas
sobre TLA. |
| Otro mail de L. Lamport
contestado una consulta sobre el uso del operador choose. |
| Mail de M. Jackson
contestando algunas preguntas
sobre WRSPM. |
| Mail de S.
Jarvis contestando algunas preguntas sobre CSP |
|
|
Material usado hasta 2025
Apunte sobre Z (pdf)
Lista de libros sobre Z (deben leer al menos uno)
Un problema resuelto
| Algo sobre promoción de operaciones
|
| | | | | | |