| Especificaciones formales (pdf) |
| Apunte sobre Z (pdf) --
Lista de libros sobre Z (deben leer al menos uno)
-- Un problema resuelto
-- Algo sobre promoción de operaciones
|
| WRSPM - Introducción y
designaciones (pdf)
-- Especificación que mezcla DK con S
|
| Consejos sobre Requerimientos
y Especificaciones (pdf) |
| Statecharts (pdf) -- Stecharts parametrizados (pdf)
-- Un problema resuelto
|
| Apunte sobre Communicating
Sequential
Processes (CSP) (pdf)
-- Problema horno
microondas en CSP (Versión
PDF) |
| Seguridad, vitalidad y equidad (pdf) |
| Temporal Logic of Actions (pdf) |
| Un ejemplo con requisitos
temporales en TLA (pdf)
|
| Práctica 2 (pdf) |
| 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 |