Contenido 2012

Tema Sesión Referencias Transparencias Notas de clase y ejemplos
Modelo en event B sesión 1-3 [ 1, cap 1,2] 9, cap 1]Arquitectura y obligaciones de prueba Centro de atención en Rodin
Pruebas: estrategia global sesión 3-5 [ 1, cap 1,2] 9, cap 1]estrategias de prueba
Caso ascensores sesión 3-5 [ 1, cap 1,2] 9, cap 1]ascensores2012_ref5_proved.zip
Patrones de diseño sesión 3-5 [ 1, cap 1,2] 9, cap 1]patrones: slides
Transferencia de archivo sesión 3-5 [ 1, cap 1,2] 9, cap 1]transferencia y patrones protocolo con patrones en Rodin

Contenido 2010-2011

Tema Sesión Referencias Transparencias Notas de clase y ejemplos
Indroducción sesión 1-3 [ 1, cap 1,2] 9, cap 1] introducción universidad probado.zip
Máquinas simples sesión 4,5 [ 9, cap 2] [ 8, cap 4] clase2_2010.pdf Notación (J-R Abrial) parqueo-ref1-req.zip
Refinamientos y obligaciones sesión 6-8 [ 8, cap 4] [ 8, cap 1,2,3] invariante de refinamiento obligaciones de prueba clase3_2011-2.pdfuniv_cursos_abstr.zip
Pruebas del refinamiento sesión 9-10-11 [ 8, cap 4] [ 8, cap 1,2,3] [ 7] obligaciones: formulación Pruebas, ejemplo univ-twoproofs.zip
Diseño de refinamientos sesión 11-14 [ 8, cap 2,3,4] el ejemplo del MIO
Modelar estructuras de datos sesión 11-14 [ 8, cap 2,3,4]clase8-notacion.pdf restaurante-unp.zip restaurante-orden-unp.zip
Patrones de diseño sesión 15 [ 8, cap 2,3,4] patrones acción/reacción
Diseño de programas sesión 15-16 [ 6] [ 7] Introducción secuencias.zip diagcero.zip
Diseño de programas: variante sesión 17-18 [ 6] invariante y variante, ejemplo matriz.zip
Diseño de programas: ejemplos sesión 17-18 [ 6] bandera_almost.zip sumhasta.zip
Diseño de programas: uso de composición sesión 19-20 [ 6] correr secuencias
Diseño de programas: unir módulos sesión 21-22 [ 6] próxima permutación fase1.zip
Diseño de programas: optimizar con invariante sesión 23-24 [ 1, cap 10] ejemplo de maxsuma y pruebas suma-hasta.zip máxima suma.zip
Diseño de programas: simular (“model checking”) sesión 25-26 [ 7] secuencia de colores (para corregir) correr elementos
Diseño de programas concurrentes: introducción sesión 27 [ 7] modelos concurrentes exclusion mutua.zip
Diseño de programas concurrentes: ejemplo sesión 28-29 [ 7] programas-concurrentes1.pdf simpson-partial.zip
Diseño de programas distribuidos: introducción sesión 28 [ 7] transmision-archivo refinamientos
Pruebas interactivas sesiones 27-29 [ 8, cap 5]
Combinación y partición de eventos sesiones 30 [ 8, cap 2]

Archivos 2012-1

http://sunset.usc.edu/classes/cs377_2009/Motivation.ppt

Archivos 2011-2

Proof systems: proofs.pdf

Ejemplo de los grupos de investigación (sin pruebas): grupos-inv.zip

Sequential Programs: sequential-programs.pdf

Taller: taller-seq-progs.pdf

Transferencia de Archivos: sld.ch4.file.pdf (Tomado de : http://www.event-b.org/).

Protocolo: sld.ch6.brp.pdf (Tomado de : http://www.event-b.org/).

Concurrencia: eventb-conc.pdf, http://deploy-eprints.ecs.soton.ac.uk/116/1/sld.ch7.conc.pdf

NTCC: ntcc.pdf

Software

  1. RODIN, Edición y prueba de sistemas EventB: http://sourceforge.net/projects/rodin-b-sharp
  2. Atelier B edición, prueba y generación de código de máquinas B http://www.atelierb.eu/index_en.html
  3. proB edición, “model checking” de máquinas B http://www.stups.uni-duesseldorf.de/ProB/overview.php

Links Útiles

  1. Conceptos básicos de teoría de conjuntos y matemáticas: http://www.cs.odu.edu/~toida/nerzic/content/set/basics.html

Notas de Clase Anteriores

Introducción: Introd-2000
Refinamiento de Máquinas: notas-1999

Transparencias de Clases de años Anteriores

2009

Tema Sesión Referencias Transparencias Notas de clase y ejemplos
Indroducción sesión 1 Introd-2007casos críticos introducción
Modelar un Sistema sesiones 2,3-2009 EventB y B
Modelar un Sistema (2) sesiones 3-2009 Obligaciones de prueba MIO modelo básico en Rodin 1.0
Modelar un Sistema: relaciones y funciones sesiones 4-2009 parqueadero-parcial
Operaciones sobre relaciones sesiones 5-2009 operaciones ejemplo del MIO completo
Refinamiento sesiones 6,7-2009 pruebas y ejemplo de la isla isla, ejemplo de Abrial en Rodin
Pruebas en Rodin sesiones 8-2009 estrategias de prueba y refin. del MIO Redes sociales, sin pruebas
Modelar y probar sesiones 9-2009 Taller: restaurante máquinas de ejemplo del restaurante
Sistemas que terminan sesiones 9,10-2009 protocolo protocolo con canal no confiable protocolo en Rodin
Sistemas que terminan (2) sesiones 11-2009 desarrollo de programas subsecuencia en Rodin
Desarrollo de programas: ejemplos sesiones 12-2009 matriz con fila monotónica
Desarrollo de programas: ejemplos (3) sesiones 13-2009 la siguiente permutación la máxima suma
Desarrollo de programas: ejemplos (2) sesiones 13-2009 Búsqueda binaria
Desarrollo de programas: ejemplos (3) sesiones 14-2009 intersección de conjuntos
Pruebas interactivas sesiones 16-2009 Rueda de Chicago pruebas rc en Rodin
Construcción modular de software sesiones 17-2009 realciones de inclusión
Construcción modular de software(2) sesiones 18-2009 implementación
Tema Sesión Referencias Transparencias Notas de clase y ejemplos
Indroducción sesión 1 [ 1] cap. 1Introd-2007casos críticos introducción
Modelamiento Formal de Sistemas 2008-2, sesiones 2,3,4 [1] cap. 2 introducción al modelamiento ejemplo y notación ejemplos de especificación Observaciones MIO1-Rodin MIO-probado
Refinamiento de modelos 2008-2, sesiones 5,6 [1] cap. 2 la idea supermercado ejemplo colores consultorio supermercado-rodin consultorio.zip
Refinamiento de modelos sesiones 7,8 [1] cap. 2 uso de relaciones
Interacción software/hardware en modelos 9-10-2008-2 [1] cap. 2 acceso lugares acceso lugares: modelo completo ejemplos de especificación lugares en Rodin, probado
Pruebas interactivas 11-2008-2 [1] cap. 2 estrategias sin pruebas.zip con pruebas de Inv3.zip
Hacia Sistemas de software 12, 2008 [1] cap introducción y ejemplo protocolo archivos
Refinamiento de software 13,2008 [1] cap ej. de protocolos: refinamiento Refinamiento(2)
De B-eventos a B 14-2008-2 [1] cap. 2 traducción de modelos busqueda en Rodin las maquinas en B
Sistemas de software en B 2008-2 [1] cap máquinas grandes Ejemplo Las máquinas
Sistemas de software(3) 04/10/2007 [1] cap Fila de mayores a 3
Programas como Sistemas de eventos 18/09/2006 [1] capIntroduccióndesarrollo de programas busqueda.zip
Programas como eventos (2) 10/10/2006 [1] cap subsecuenciaabstracto programa1 programa 2 pruebas arbol
Plantillas 10/10/2008 [1] cap plantillas otras plantillas Mínimo acotado
Sistemas de software: ejemplos 04/11/2007 [1] cap
Software por componentes 8/04/2008 [1] cap Introducción: B vs Event-B
Software por componentes (2) 10/04/2008 [1] cap ejemplos
Software por componentes (3) 10/04/2008 [1] cap Incluir o ver máquinas
Software por componentes (4) 8/04/2008 [1] cap ejemplo: semáforo
ANEXOS 10/03/2008 [1] cap
Especificar mediante relaciones 18/09/2006 [1] cap ejemplosejemplo-pesos
Pruebas de un sistema 10/11/2007 [1] cap toría completa de event-B
Pruebas de un sistema 14/09/2006 [1] cap obligaciones de prueba teoria-eventosB notación

Ejemplos de Exámenes y Ejemplos Anteriores

 
desarrollo/material-adicional.txt · Última modificación: 2014/03/04 10:44 por crueda
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki