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

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

Hoy en día, las computadoras son empleadas para múltiples tareas en las cuales la presencia de fallas puede traer aparejado severas consecuencias, desde pérdidas materiales hasta vidas humanas. En este sentido, 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 múltiples aplicaciones críticas donde son utilizadas.
Es por esta razón que resulta de vital importancia que los sistemas de software que están por detrás de estos sistemas críticos sean altamente confiables. Es en estas situaciones donde la aplicación de técnicas y métodos formales puede resultar de gran utilidad.
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 que, además, 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, con especial énfasis en el uso de lenguajes de especificación formal en las etapas iniciales del desarrollo de software.
Dado que se trata de la única materia asociada a la temática se busca que el alumno adquiera un conocimiento integral sobre las múltiples variantes existentes de Métodos Formales, las situaciones en las cuales las mismas resultan adecuadas de aplicar así como que adquiera habilidades para su adopción y aplicación.
Durante el dictado de la asignatura se abordan los siguientes ejes transversales:
1) Identificación, formulación y resolución de problemas de informática.
Se aborda a partir del trabajo práctico 2 al 6, donde se trabaja con problemas que deben ser modelados con el soporte de herramientas. También se trabaja con este tipo de problemas en las evaluaciones parciales de la materia.
Se evalúa por medio de dos evaluaciones parciales.
2) Concepción, diseño y desarrollo de proyectos de ingeniería en sistemas de información/informática.
Se aborda fundamentalmente en el práctico de Alloy, donde se trabaja con problemas que deben ser modelados con el soporte
de herramientas. También se trabaja con este tipo de problemas en la correspondiente evaluación parcial.
Se evalúa por medio de una evaluación parcial.
3) Utilización de técnicas y herramientas de aplicación en la informática.
Se aborda a partir del trabajo práctico 3, donde se comienza a trabajar con problemas que deben ser modelados con el soporte
de herramientas de modelado y análisis de Redes de Petri; también los alumnos emplean soporte automatizado para la especificación formal y la verificación de propiedades en Alloy.
En el caso de Alloy, el uso de la herramienta se evalúa en la correspondiente evaluación parcial donde los alumnos hacen uso del Analizador Alloy.
4) Fundamentos para la comunicación efectiva.
Se busca que el estudiante vaya adquiriendo la capacidad de expresarse utilizando un vocabulario acorde a los contenidos
vistos en la asignatura.
La expresión oral se aborda a partir de la interacción permanente con los docentes tanto durante las clases teóricas como en las prácticas. En ocasiones, en caso de que el examen final sea oral, también se evalúa en esa instancia.
La expresión escrita se evalúa a través de las evaluaciones parciales y, ocasionalmente, en los exámenes finales escritos.
5) Fundamentos para la acción ética y responsable.
Se implementa a través de la entrega desde el primer día de clase de la planificación de las actividades teóricas y prácticas de
la asignatura para que los estudiantes puedan organizar adecuadamente sus horarios y cargas de estudio y trabajo. Asimismo, se informan las fechas de la Evaluación Global Integradora así como de los dos recuperatorios de los parciales.
La evaluación de este eje se da por medio de la verificación del respeto a fechas y formatos pactados.
6) Fundamentos para el aprendizaje continuo.
Este eje es abordado por medio de las actividades teóricas, donde los estudiantes pueden participar e interactuar con el
docente, respondiendo preguntas o planteando inquietudes, todo esto complementado con lectura de material bibliográfico o
apuntes de la cátedra. Por otro lado, las actividades prácticas permiten que el alumno ponga a prueba y practique los
conocimientos que haya ido adquiriendo en las clases teóricas.
La evaluación de este eje se realiza, de forma más informal, por medio del nivel de participación de los alumnos en las clases
prácticas, y formalmente, por medio de dos evaluaciones parciales y de un examen final o, en el caso de los alumnos en condición de promocionar, de una Evaluación Global Integradora.

Metodología de Trabajo:
La asignatura introduce al alumno en la aplicación de métodos para la especificación y la verificación formal de propiedades de sistemas de software.
Las instancias de teoría y práctica son semanales. La teoría trabaja lineamientos conceptuales que se aplican luego en los trabajos prácticos de aula y laboratorio. La teoría y la práctica se encuentran estrechamente vinculadas. En la práctica, se plantean ejercitaciones de aula de complejidad creciente, resolviendo los ejercicios con herramientas de soporte y desarrollo típicas en la comunidad de software libre.
En las clases se trabaja con los siguiente recursos:
- Apuntes, diapositivas, videos, libros, tutoriales.
- Multimedia, computadoras, demostraciones de usos de herramientas con ejemplos en vivo.
- Herramientas: herramientas de modelado de Redes de Petri y analizador de Alloy.
Para cada unidad se deja disponible el material correspondiente a los contenidos de la unidad, las diapositivas de clase, el apunte teórico y su correspondiente trabajo práctico en el repositorio digital de la asignatura.
Para una mejor organización, tanto de los estudiantes como del equipo docente, se presenta un cronograma con la descripción de las actividades que se realizan cada día de clase.

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. Diversas clasificaciones de los Métodos Formales. Estilos de especificaciones de software. Características. Estilos de desarrollo formal. 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.

Unidad III: Integración de Técnicas Formales y Semi-formales con OCL.
Limitaciones de las especificaciones semiformales. 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. Diseño por Contrato. Especificación de pre y post condiciones de operaciones.

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

Unidad V: 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. Especificaciones estructurales y del comportamiento. Uso del analizador.

Unidad VI: Verificación Formal de Sistemas de Software
Aproximaciones. Model Checking. Verificación deductiva por demostración de teoremas. Sistema formal. Sintaxis, semántica y sistema de prueba. Relación de refinamiento. Refinamiento por pasos sucesivos. Refinamiento de funciones. Refinamiento de datos.

Unidad VII: Especificación Formal en JML
Lenguajes de especificación de la interfaz de comportamiento. El lenguaje JML. Aplicaciones de JML. Aserciones en JML y su uso en tiempo de ejecución. Runtime-assertion-checking (RAC). Diseño por Contrato. Verificación deductiva en JML.

Práctico 1 (Aula). Introducción a los Métodos Formales.
Objetivos: Dadas las características netamente teóricas de los temas cubiertos en la unidad 1 del programa analítico, en este
práctico se solicita que el alumno responda una serie de preguntas acudiendo al conocimiento adquirido del estudio de dicha unidad.

Práctico 2 (Aula). OCL
Objetivo: En este práctico el alumno aprenderá sobre la sintaxis y semántica del lenguaje OCL y su aplicación para complementar la semántica de diagramas de clase en UML.

Práctico 3 (Aula y Laboratorio). Modelado del comportamiento con Redes de Petri
Objetivo: En este práctico el alumno aprenderá a modelar sistemas asincrónicos y concurrentes por medio de Redes de Petri tradicionales haciendo uso de alguna herramienta de modelado de libre distribución.

Práctico 4 (Aula y Laboratorio). Análisis de Redes de Petri
Objetivo: El alumno aprenderá a realizar un análisis de los problemas de seguridad, acotabilidad, conservación, vitalidad, alcanzabilidad y cobertura de modelos de redes de Petri de forma analítica y su corroboración por medio de herramientas automatizadas.

Práctico 5 (Laboratorio). Alloy: Modelado estático
Objetivo: El alumno trabajará en el modelado estático de un sistema, especificando las propiedades estructurales del mismo y realizando la verificación de las propiedades planteadas, todo esto haciendo uso del analizador de Alloy.

Práctico 6 (Laboratorio). Alloy: Modelado dinámico
Objetivo: El alumno trabajará en el modelado del dinámico de un sistema, especificando el comportamiento del mismo a lo largo del tiempo y realizando la verificación de las propiedades planteadas, todo esto haciendo uso del analizador de Alloy.

Condiciones para REGULARIZAR la asignatura:
- Haber asistido al menos al 80% de las clases teóricas y prácticas de la asignatura.
- Haber aprobado dos parciales (o sus respectivas recuperaciones) con nota mayor o igual a 6 sobre 10.

Condiciones para PROMOCIONAR la asignatura:
- Haber asistido al menos al 80% de las clases teóricas y prácticas de la asignatura.
- Haber aprobado dos parciales (o sus respectivas recuperaciones) con nota mayor o igual a 7 sobre 10.
- Haber aprobado, al final de la cursada, un examen integrador con nota mayor o igual a 7 sobre 10.
- En caso de haber obtenido nota de promoción en todas las instancias de evaluación, el alumno aprobará la materia con una nota que surgirá del promedio de las mismas.

Recuperaciones:
-Se otorgarán dos recuperaciones para cada examen parcial. Se considera como válida la última nota obtenida en cada recuperación.
-El examen integrador no se recupera.

Examen Final:
En caso de regularizar la materia, el alumno deberá rendir un examen final, el cual podrá ser oral o escrito, en cualquiera de
los turnos de examen establecidos.

Exámenes Libres:
Para aprobar un examen libre, el alumno deberá aprobar en una primera instancia una evaluación sobre temas prácticos de la
materia con una nota de al menos 6 sobre 10. En caso aprobar la evaluación práctica, el alumno además deberá aprobar una
evaluación sobre temas teóricos con una nota de 4 sobre 10. La nota final surgirá del promedio de ambas notas.

[1] Specification of Software Systems, 2nd edition, Springer. V.S. Alagar K. Periyasamy, (2011).
[2] An Introduction to Formal Methods for the Development of Safety-critical Applications. Technical report. A. Haxthausen (2010).
[3] Formal Methods Overiew, Encyclopedia of Information Science and Technology, 3ra Edición, IGI Global. Ana Funes y Aristides Dasso, (2014).
[4] Software Abstractions, The MIT Press, Jackson, Daniel (2012).
[5] Formal Software Design with Alloy 6 (https://haslab.github.io/formal-software-design/). Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo (2021).
[6] Object Constrain Language version 2.4 (https://www.omg.org/spec/OCL/About-OCL/), OMG (2014)
[7] The Object Constraint Language: Getting Your Models Ready for MDA, Second Edition, Addison-Wesley Professional. Warmer, Jos & Kleppe, Anneke (2003).
[8] Petri Net Theory and the Modeling of Systems, Prentice Hall. Peterson, James Lyle (1981).
[9] Tutorial de JML, https://www.openjml.org/tutorial

[1] A Language and Tool for Exploring Software Designs. Commun. ACM 62(9): 66-76. Daniel Jackson (2019).
[2] Specification Case Studies in RAISE. FACIT series. Springer-Verlag. Hung Dang Van, Chris George, Tomasz Janowski, and Richard Moore (Eds) (2002).
[3] The RAISE Specification Language. Prentice-Hall International, The RAISE Language Group (1992).
[4] The RAISE Development Method. Prentice-Hall International, The RAISE Method Group (1995).
[5] System and Software Verification, Model-Checking Techniques and Tools. Springer. B. Bérard, M. Bidot, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci et al. (1999).
[6] Formalizing UML class diagrams, capítulo 8 de UML and the Unified Process, Idea Group, Funes, A., George, C. (2003).
[7] Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition. Cambridge University Press, Huth, Michael & Ryan, Mark (2004).

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. Aproximaciones a la verificación formal de sistemas de software y de sus propiedades. Métodos Formales livianos. Alloy. Model Checking. Verificación deductiva. JML. Otros estilos de especificaciones formales. Redes de Petri. OCL.

 

Contacto: afunes@email.unsl.edu.ar