Materia	Carrera	Plan	Año	Periodo
METODOS FORMALES	ING. INFORM.	026/12- 08/15	2020	1° cuatrimestre

Docente	Función	Cargo	Dedicación
FUNES, ANA MARIA	Prof. Responsable	P.Asoc Exc	40 Hs

Las computadoras son empleadas para múltiples tareas, donde la presencia de fallas puede traer aparejado severas consecuencias no sólo a nivel de pérdidas económicas sino de vidas humanas.
En las últimas décadas, las computadoras han pasado a jugar un rol esencial en el control aeroespacial, en la aeronavegación, en el control de trenes, autos, reactores nucleares y equipamiento hospitalario, por dar simplemente algunas pocas de las aplicaciones más críticas. Por esta razón, es que resulta de vital importancia que los sistemas de computación que están por detrás sean altamente confiables.
Para construir software de alta calidad, libre de errores y confiable, una de las vías más importantes, sin descartar otras alternativas, es definiendo el dominio y los requerimientos a través del uso de especificaciones formales. Una de las principales ventajas de las especificaciones formales es que no son ambiguas y permiten la verificación formal de propiedades deseables del sistema especificado, conduciendo al desarrollo de software de calidad.

El objetivo de la materia es que los alumnos tengan la posibilidad de incursionar en la aplicación de métodos formales como herramienta de producción de software de alta calidad.

Unidad I: Aspectos Generales de los Métodos Formales
Introducción al curso y a los Métodos Formales. El papel de los Métodos Formales en Ingeniería de Software. Pros y contras de los Métodos Formales. Un panorama de los Métodos Formales. Diversas clasificaciones de los Métodos Formales. Estilos de especificaciones. Estilos de desarrollo. Grados de rigor.

Unidad II: Especificaciones Formales
Enfoques de especificación de un sistema. Especificaciones basadas en Lógica de Primer Orden y Teoría de Conjuntos. Especificaciones aplicativas, imperativas, concurrentes. Especificaciones orientadas al modelo. Especificaciones algebraicas. Especificaciones orientadas a la propiedad. Especificaciones algebraicas en RSL.

Unidad III: Verificación Formal de Sistemas de Software
Verificación formal del software. Model Checking. Sistema formal. Sintaxis, semántica y sistema de prueba. Relación de refinamiento. Stepwise refinement. Refinamiento de funciones. Refinamiento de datos. Relación de Refinamiento en el Método Formal RAISE.

Unidad IV: Lightweight Formal Methods.
Métodos Formales Livianos. Alloy. Especificaciones formales y verificación en Alloy. La lógica de Alloy: átomos, relaciones, constantes, funciones predefinidas, operadores, restricciones, expresiones, declaraciones, multiplicidades. El lenguaje Alloy: módulos, signaturas, hechos, predicados, funciones, aserciones y comandos run y check. Uso del analizador.

Unidad V: Especificación Formal del Comportamiento.
Definición formal de Red de Petri. Modelado del comportamiento con Redes de Petri. Análisis de una Red de Petri. Árbol de alzanzabilidad. Ecuaciones Matriciales. Algunas extensiones.

Unidad VI: Integración de Técnicas Formales y Semi-formales.
Limitaciones de los diagramas de clase UML. El lenguaje OCL. Características. Especificación de Valores iniciales de atributos. Especificación de reglas de derivación (valores de atributos derivados). Especificación del cuerpo de operaciones de consulta. Especificación de invariantes. Especificación de pre y post condiciones de operaciones.

1. Introducción a los Métodos Formales.
2. Especificaciones algebraicas en RSL.
3. Modelado del comportamiento con Redes de Petri
4. Análisis de Redes de Petri
5. Especificación y Verificación en Alloy.
6. OCL

Para regularizar la materia será necesario cumplir con las siguientes condiciones, las cuales, debido al aislamiento social, preventivo y obligatorio decretado por el Poder Ejecutivo Nacional en el marco de la Emergencia Sanitaria por COVID-19, son excepcionales:
1) Hacer entrega, vía e-mail, y aprobar con una nota mínima de 6 (seis) aquellos trabajos prácticos solicitados por la cátedra, en tiempo y forma.
2) Resolver, de manera individual, no presencial y a libro abierto, el/los ejercicios asignados por la cátedra. La evaluación será vía Google Meet u otro medio similar, y se aprobará con una nota mínima de 6 (seis).
Debido a la situación particular de dictado de la materia, la misma no podrá promocionarse, por lo tanto, para su aprobación, el alumno que haya alcanzado la regularidad, deberá rendir, en los turnos establecidos, un examen final presencial oral o escrito, que podrá incluir tanto temas teóricos como ejercicios prácticos. Dicho examen final se aprobará con una nota mayor o igual a 4 (cuatro).

[1] Funes, A., Dasso, A. “Formal Methods Overview” en Encyclopedia of Information Science and Technology, 3ra Edición, IGI Global, 2014.
[2] George, C.; “Introduction to RAISE”. Report 249 UNU/IIST.
[3] Hung Dang Van, Chris George, Tomasz Janowski, and Richard Moore (Eds). “Specification Case Studies in RAISE”. FACIT sries. Springer-Verlag. 2002.
[4] Jackson, Daniel; “Software Abstractions”, The MIT Press, 2012.
[5] Object Management Group (OMG); Object Constraint Language OMG Available Specification Version 2.4, Feb 2014.
[6] Peterson, James Lyle (1981). "Petri Net Theory and the Modeling of Systems". Prentice Hall. ISBN 0-13-661983-5.
[7] Peterson, James L. (1977). "Petri Nets". ACM Computing Surveys. 9 (3): 223–252. doi:10.1145/356698.356702
[8] The RAISE Language Group. “The RAISE Specification Language”. Prentice-Hall International, 1992.
[9] The RAISE Method Group. “The RAISE Development Method”. Prentice-Hall International, 1995.

[1] Abrial,Jean-Raymond. “The B-Book: Assigning Programs to Meanings”. Cambridge University Press, 1996. ISBN 0-521-49619-5.
[2] Alagar, V. & Periyasamy, K. “Specification of Software Systems”. Springer-Verlag New York, Inc. 1998.
[3] Bowen, J., & Hinchey, M., “Seven more myths of formal methods”. IEEE Software, 12(3). Julio, 1995.
[4] Bowen, Jonathan. “Formal Specification and Documentation using Z: A Case Study Approach”. International Thomson Computer Press (ITCP) Thomson Publishing. ISBN 1850322309. 2003
[5] Bowen, J., & Hinchey, M., “Ten commandments of formal methods”. IEEE Computer. Abril, 1995.
[6] Funes, A., George, C., “Formalizing UML class diagrams”, capítulo 8 de UML and the Unified Process, Idea Group, 2003.
[7] Huth, Michael & Ryan, Mark . “Logic in Computer Science: Modelling and Reasoning about Systems”. Cambridge University Press, 2000.
[8] Luqi & Goguen, J., “Formal methods: Promises and problems”, IEEE Software, 14(1), págs. 73-85., Ene-Feb 1997.
[9] Schneider, Steve. “The B-Method: An Introduction”. Palgrave, Cornerstones of Computing series, 2001. ISBN 0-333-79284-X.

Incursionar en los métodos formales como herramienta de producción de software de alta calidad.

Introducción a los Métodos Formales. Especificaciones formales. Verificación formal de sistemas de software y de sus propiedades. El Método RAISE. Otros estilos de especificaciones formales. Redes de Petri. Métodos Formales Livianos. Alloy. OCL.

Debido al aislamiento social, preventivo y obligatorio decretado por el Poder Ejecutivo Nacional, en el marco de la Emergencia Sanitaria por COVID-19, el presente es un Programa en Fase No Presencial.
En consecuencia, el dictado de la materia, desde el inicio del aislamiento, se realiza de manera virtual, respetando los horarios de dictado presencial y haciendo uso de diversas tecnologías adecuadas para poder llevar adelante el mismo.
Todo el material de la materia, tanto trabajos prácticos como apuntes, libros, filminas de los temas teóricos, se encuentran en el repositorio de la materia en Aulas Virtuales de la FCFMyN.
Las teorías se dictan por Google Meet y algunas de ellas se encuentran grabadas en vídeos y subidas a Aulas Virtuales.
Los trabajos prácticos se dictan también por Google Meet.
Las entregas de prácticos se realizan por e-mail y las evaluaciones de ejercicios por Google Meet o Zoom.
Las comunicaciones de novedades por parte de la cátedra, así como algunas consultas por parte de los alumnos, son realizadas por e-mail o por un grupo de WhatsApp de la materia.