Source: http://cic.puj.edu.co/wiki/doku.php?id=materias:desarrolloformalsistemas
Timestamp: 2019-07-23 02:57:07+00:00

Document:
DECC Wiki [materias:desarrolloformalsistemas]
Traza: • desarrolloformalsistemas
Desarrollo Formal de Sistemas (300CIS002)
* Créditos: 3
Horas de Clase: 4 / semana (3 horas de clase, 1 de taller)
Pre-requisitos: Introducción a la Programación (300CIP001) y Lógica en Ciencias de la Computación (300CIG002)
El curso busca ilustrar sobre la conveniencia de utilizar el modelamiento formal para la construcción de sistemas confiables. Mediante el estudio de casos, el curso promueve la necesidad de asignar el grueso del esfuerzo de modelamiento en la especificación, el diseño y la verificación, antes que en la implementación y depuración. Se utiliza con este fin el método Event-B, apoyado en software de generación automática de obligaciones de prueba y de generación automática de código en Java. El curso estudia también el modelamiento formal de sistemas concurrentes mediante Chequeo de Modelos (“Model-checking”), apoyado en herramientas como Spin-Promela.
Identificar las ventajas de desarrollar software formalmente.
Reconocer qué hay que verificar de un sistema
Explicar el uso de las pruebas en el diseño
Defender la ventaja de animar un modelo formal
Argumentar por qué los métodos formales son un mecanismo de aseguramiento de la calidad del software.
Contrastar verificación y “testing”
Justificar la trazabilidad de los requerimientos
Predecir corrección de una especificación mediante pruebas interactivas
Argumentar cómo insertar métodos formales en el ciclo de desarrollo
Describir formalmente sistemas completos mediante refinamiento formal.
Expresar requerimientos en invariantes y eventos
Indicar propiedades de seguridad y de ausencia de bloqueos
Reconocer la diferencia entre modelo abstracto y refinamiento
Expresar un sistema en una jerarquía de máquinas
Diseñar y verificar sistemas utilizando el método Event-B.
Proponer variables para representar observaciones
Formular propiedades como invariantes de máquinas
Reconocer constantes de un sistema
Colectar constantes y sus propiedades como axiomas en los contextos
Construir el modelo del sistema en Rodin
Desarrollar estrategias para verificar el sistema en Rodin
Integrar las obligaciones de prueba en el proceso de desarrollo de software y entender su importancia.
Relacionar cada obligación con propiedades del sistema
Revisar el modelo a partir de las pruebas interactivas en Rodin
Formular las obligaciones de prueba de un modelo
Contrastar las guardas de los eventos y el invariante, a partir de las pruebas
Expresar el modelo de un sistema en una herramienta de apoyo al desarrollo formal
Identificar los atributos de la herramienta que expresan cada componente del sistema
Reconocer qué componen máquinas y contextos
Distinguir variables, invariantes y eventos
Analizar estrategias para realizar una prueba interactiva
Identificar la suficiencia/insuficiencia de las hipótesis
Distinguir la aplicabilidad de cada probador en Rodin
Inferir cuándo es necesario agregar hipótesis
Seleccionar expresiones que conviene abstraer
Aplicar las pruebas interactivas para el desarrollo y la verificación de sistemas
Interpretar obligaciones no descargadas con posibles fallas del modelo
Emplear chequeo de modelos como verificación previa de un sistema
Predecir guardas adicionales de los eventos a partir de las pruebas
Modelar formalmente un programa
Identificar la precondición en los contextos
Relacionar la máquina abstracta a la poscondición
Inferir el invariante del programa
Relacionar la poscondición a obligación de prueba en el refinamiento
Inferir guardas en los eventos del invariante y la poscondición
Calcular el variante del sistema
Experimentar mediante chequeo de modelos
Conocer los fundamentos teóricos de Chequeo de Modelos (“Model Checking” )
Expresar el modelo de un sistema mediante estructuras de Kripke
Formular propiedades de un modelo en lógicas temporales (LTL, CTL)
Conocer estrategias básicas para determinar si un modelo cumple una propiedad
Aplicar Chequeo de Modelos para verificar sistemas concurrentes
Entender las bases de un lenguaje de modelado para concurrencia (Promela-Spin)
Conocer ejemplos clásicos de chequeo de modelos en concurrencia
Saber modelar un sistema concurrente simple en Promela-Spin
Formular propiedades de seguridad y vivacidad de un sistema en LTL, CTL
Usar herramientas (xSpin, iSpin) para verificar el modelo
1 2 Presentación del curso. Por qué fallan los sistemas [ 1,cap 1,2]
2 2 2 Uso de matemáticas en modelamiento de sistemas [ 9,cap 1]
3 2 2 Dónde integrar métodos formales de diseño [ 10,cap 1]
1-3 8 Tareas semanales, especificación en lógica [ 9,cap 1]
Capítulo 2: Diseño de sistemas simples
4 1 La noción de modelo: parte estática y dinámica [ 9,cap 2]
5 2 2 Máquinas, contextos. Un sistema simple [ 8,cap 4] [ 10,2.1-2.4]
4,5 16 Tareas semanales, resolución de problemas en temas vistos [ 8,cap 4] [ 10,2.1-2.4]
Capítulo 3: Obligaciones de prueba
6 2 1 Qué probar de un sistema, invariantes [ 8,cap 4] [ 10,cap 5]
7 2 1 Prueba de inicializacón y de eventos: ejemplos [ 8,caps 1,2,3], [ 10,cap 2, cap 5]
8 2 2 El cálculo de secuentes. Pruebas en Rodin [ 3,cap 2] [ 10,cap 2]
6-8 8 Tareas semanales, resolución de problemas en temas vistos [1, cap. 1,2]
Capítulo 4: Refinamiento de un sistema
6 1 Jerarquía de modelos. [ 10,cap 2]
7 1 Relación de la abstracción y el refinamiento. Ejemplos [ 8,caps 1,2,3], [ 10,cap 2]
8 1 2 Obligaciones de prueba del refinamiento [ 8,caps 1,2,3], [ 10,cap 2]
9 3 2 Pruebas de refinamiento en Rodin. Estrategias y Ejemplos [ 8,caps 3,4], [ 10,cap 2, cap 3]
6-9 8 Tareas semanales, resolución de problemas en temas vistos [ 8,caps 3,4], [ 10,cap 2, cap 3]
Capítulo 5: Diseño de refinamientos
6 2 Invariante de encadenamiento [ 10,cap 3 ]
7 2 Refinamiento de eventos [ 10,cap 2, cap 3 ], [ 10,cap 2]
8 2 Eventos nuevos en el refinamiento [ 8,caps 3,4], [ 10,cap 2,3]
9 2 Ejemplos de diseño, pruebas, simulación en ProB [ 8,caps 3,4], [ 10,cap 2, cap 3]
10 2 Simulación y chequeo de sistemas en ProB [ 7]
Capítulo 6: Patrones de diseño
11 1 Qué es un patrón de diseño [ 10,cap 3 ]
12 1 1 Sincronización fuerte, ejemplos [ 10,cap 2, cap 3 ], [ 10,cap 2]
13 1 1 Sincronización débil, ejemplos 10,cap 2,3]
11-13 4 Tareas semanales, resolución de problemas en temas vistos 10,cap 2,3]
Capítulo 7: Diseño de programas secuenciales
14 1 El modelo de un programa [ 10,cap 4 ], [ 6]
15,16 4 3 Ejemplos de diseño formal de programas [ 7] [ 10 15.1-15.3]
17 1 1 Refinamiento de programas, variante e invariante [ 6] [ 10 15.4-15.9] [ 10,cap 4 ]
14-17 8 Tareas semanales, resolución de problemas en temas vistos [ 6] [ 10 15.4-15.9] [ 10,cap 4 ]
Capítulo 8: Diseño de programas concurrentes y distribuidos
18 2 Estructuras de Kripke, modelos de sistemas [ 13 cap 1,2]
19 2 2 Lógicas temporales LTL, CTL [ 13 cap 2,3 ]
20 2 2 Satisfacción de una fórmula por un modelo, ejemplos [ 13 cap 3,4 ]
21 2 2 El lenguaje Promela-Spin, ejemplos de programas concurrentes
22,23 4 2 exclusión mutua, protocolos: verificación en Spin
18-23 16 Tareas semanales, resolución de problemas en temas vistos [ 13 cap 3,4 ]
Relevancia 1 2 1 1 1 5 5
(A) Aplicación de Conocimientos (A1) Identificar los fundamentos científicos y los principios de ingeniería que rigen un proceso o sistema. (Conocimiento) Cap 1,2,3 Exposiciones del profesor, solución de ejercicios, tareas y lecturas Exámenes, proyecto y tareas
(B) Análisis de problemas y requerimientos (B1) Describir procesos de manera declarativa ignorando los detalles de su implementación. (Comprensión). (B2) Utilizar el lenguaje propio de las matemáticas, la lógica y la ingeniería para especificar requerimientos funcionales y no funcionales de un sistema o proceso. (Aplicación). (B3) Sintetizar la información, evidencias y hechos necesarios para analizar un problema. (Análisis - Síntesis). Todos Exposiciones del profesor, discusiones en clase, solución de ejercicios, tareas Exámenes, proyecto, tareas
(E) Responsabilidad profesional y ética (E1) Identificar los códigos de ética relacionados con la disciplina. (Conocimiento). Todos lecturas, tareas tareas
(G) Impactos de la computación y la ingeniería (G1) Identificar los eventos históricos y contemporáneos que la computación y la ingeniería han afectado. (Comprensión). Cap 1 Proyecto Proyecto, manejo de la notación
(I) Uso de herramientas y técnicas (I2) Utilizar herramientas de diseño, modelamiento y simulación. (Aplicación). Cap 3,4,5 Tareas, lecturas Proyecto y Tareas
(J) Modelamiento y diseño de sistemas computacionales (J2) Relacionar conceptos y principios teóricos para la resolución efectiva de un problema. (Síntesis). (J3) Combinar principios de matemáticas, computación e ingeniería para modelar una situación. (Síntesis). Todos Exposiciones del profesor, tareas, proyecto Exámenes, proyecto y tareas
(K) Desarrollo de software (K2) Implementar e integrar componentes de software respetando los criterios de diseño. (Aplicación). (K3) Establecer invariantes y propiedades de componentes de software. (Análisis). Todos Exposiciones del profesor, tareas Exámenes, proyecto y tareas
U: se usa, E: se evalúa
Tareas y Talleres 15 % 6% 13% 6% 6% 13% 25% 31%
Primer Parcial 30 % 6% 13% 6% 6% 38% 31%
Segundo Parcial 30 % 6% 13% 6% 6% 38% 31%
Proyecto 25% 6% 13% 6% 6% 13% 25% 31%
Abrial, Jean-Raymond. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010
Huth, M.R. and Ryan,M. Logic in computer science : modelling and reasoning about systems. 1ed.
MATISSE Event B Reference manual Manual
Abrial, Jean-Raymond Guidelines to formal Systems Introducción
Abrial, Jean-Raymond sequential program construction desarrollo de programas
Rodin Project User manual manual de Rodin
EventB Descripción El lenguaje de Event B (leer con cuidado el capítulo IV, de Abrial)
De eventB.org Estrategia de uso de probadores de Rodin http://wiki.event-b.org/index.php/Rodin_Provers
Requerimientos en Rodin Tutorial http://pror.org/content/tutorial
E. Clark, O. Grumberg, D. Peled Model Checking. MIT Press, 2000
C. Baier, J-P. Katoen Principles of Model Checking. MIT Press, 2007
materias/desarrolloformalsistemas.txt · Última modificación: 2019/01/21 10:47 por crueda

References: resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución