Métodos Formales de Desarrollo de Software26230
- Centro
- Facultad de Informática
- Titulación
- Grado en Ingeniería Informática
- Curso académico
- 2024/25
- Curso
- 4
- Nº Créditos
- 6
- Idiomas
- Castellano
- Código
- 26230
DocenciaAlternar navegación
Guía docenteAlternar navegación
Descripción y Contextualización de la AsignaturaAlternar navegación
Los métodos formales hacen que el desarrollo de software adquiera un carácter más científico y similar a otras disciplinas ingenieriles, así como promueve el uso de herramientas con fundamentos matemáticos sólidos como ocurre en las disciplinas bien consolidadas. Estos métodos se denominan formales por estar basados en matemáticas, principalmente en lógica matemática. Hasta hace pocos años el desarrollo industrial de sistemas, usando dichas técnicas, era considerado un complejo ejercicio teórico e inviable en problemas reales. Pero la creciente complejidad e importancia de los sistemas informáticos acabó por hacer patente la importancia de que dichos sistemas fueran fiables y seguros, es decir carecieran de errores o fallos. No sólo por las terribles repercusiones que pueden tener estos fallos en áreas donde la seguridad es crítica, sino también por las repercusiones económicas y de calidad que afectan a las empresas. Ello, junto a que los sistemas informáticos desempeñan un papel cada día más esencial en la sociedad, hizo que el mundo industrial cambiase de actitud. Así, en las últimas décadas los métodos formales han adquirido un notable avance y su uso en el ámbito industrial ha dejado de ser la utopía que sus detractores aseguraban. En la actualidad hay grandes empresas, como Intel, IBM, Sony, Siemens, Amazon o Microsoft, que colaboran muy activamente tanto en la creación de herramientas de ayudan al desarrollo formal de software, como en la aplicación de dichas herramientas para obtener aplicaciones industriales fiables. De hecho, en esta asignatura se utiliza una herramienta de desarrollo de software que ha sido creada por Microsoft: Dafny. Aunque la utilidad de los métodos formales y su eficiencia en desarrollos industriales están hoy en día demostradas, todavía falta más trabajo para que la mayoría de ingenieros los conozcan y apliquen. Esta labor la deben realizar las universidades, que deben incluirlos en sus contenidos académicos, y los/las profesores(as), quienes se deben formar e investigar en esta área de conocimiento, y también los/las estudiantes, quienes deben tener una formación más sólida en matemáticas y lógica. Esta asignatura contribuye a esta tarea de lograr que la labor del ingeniero del software sea verdadera ingeniería, para que el usuario final reciba productos fiables y seguros.
Competencias/ Resultados de aprendizaje de la asignaturaAlternar navegación
Los objetivos concretos de esta asignatura son:
- Entender la importancia de que la programación sea una actividad más científica que artesanal.
- Conocer la historia y motivación de los métodos formales de desarrollo de software.
- Conocer el estado del arte del área del desarrollo formal de software.
- Conocer lenguajes, métodos y herramientas concretos de desarrollo formal de software.
- Capacidad para manejar lenguajes y herramientas concretas de desarrollo formal de software.
Contenidos teórico-prácticosAlternar navegación
Tema 1.- Introducción
Tema 2.- Inducción matemática
Tema 3.- Introducción al lenguaje y verificador Dafny
Tema 4.- Tipos de valores
Tema 5.- Inducción Estructural y Datatypes
Tema 6.- Arrays y Framing
Tema 7.- Módulos y Orientación a Objetos
MetodologíaAlternar navegación
En esta asignatura se utilizan diversas metodologías de enseñanza. Se impartirán tanto clases de exposición de los contenidos conceptuales de la materia, como laboratorios de resolución de problemas prácticos utilizando la herramienta Dafny, de forma interactiva, en la que los/las estudiantes utilizan la herramienta a la vez que la profesora. Se proporcionarán problemas y ejercicios que los/las estudiantes deberán desarrollar individualmente y que mediran el nivel de aprendizaje a lo largo del cuatrimestre.
Sistemas de evaluaciónAlternar navegación
- Sistema de Evaluación Continua
- Sistema de Evaluación Final
- Herramientas y porcentajes de calificación:
- Trabajos individuales (%): 100
Convocatoria Ordinaria: Orientaciones y RenunciaAlternar navegación
Para superar la asignatura en evaluación continua los/las estudiantes deberán realizar en el laboratorio tres trabajos prácticos individuales que prueben su conocimiento de las herramientas y técnicas abordadas en clase. El porcentaje de la nota de cada trabajo práctico es del 30% para el primero, 40% para el segundo, y 30% para el tercero.
Convocatoria Extraordinaria: Orientaciones y RenunciaAlternar navegación
La evaluación global consiste en realizar en el laboratorio un trabajo práctico individual que equivale al conjunto de trabajos realizados durante el curso para la evaluación contínua.
Materiales de uso obligatorioAlternar navegación
- Transparencias de clase.
- El tutorial on-line y la documentación de la página Web:
https://dafny.org/
BibliografíaAlternar navegación
Bibliografía básica
- Documentación de la página Web:
https://dafny.org/
- K. Rustan M. Leino. Program Proofs. MIT Press, March 2023. ISBN 9780262546232
Bibliografía de profundización
- Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald.
Formal methods: Practice and Experience.
ACM Computing Surveys, 41(4):19:1–19:36, October 2009.
- Jason Koenig and K. Rustan M. Leino. Getting started with Dafny: a guide. In Marktoberdorf 2011 lecture notes. (http://research.microsoft.com/en-us/um/people/leino/papers/krml220.pdf)
- K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16, volume 6355 of LNCS, pages 348-370. Springer, 2010. (http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf)
- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Incorporated, 1976, ISBN 0-613-92411-8
Revistas
- ACM Transactions on Computational Logic
- ACM Transactions on Software Engineering and Methodology
- Applicable Algebra in Engineering, Communication and Computing.
- Formal Aspects of Computing
- Formal Methods in System Design
- Journal of Automated Reasoning
- Software Testing Verification & Reliability
Direcciones web
- Dafny: a language and program verifier for functional correctness
https://dafny.org/
- Formal Methods and Software Technology - Interesting Conferences
http://user.it.uu.se/~bengt/Info/conferences.shtml
GruposAlternar navegación
16 Teórico (Castellano - Tarde)Mostrar/ocultar subpáginas
Semanas | Lunes | Martes | Miércoles | Jueves | Viernes |
---|---|---|---|---|---|
16-30 | 14:00-15:30 (1) | 15:30-17:00 (2) |
Profesorado
16 P. Laboratorio-1 (Castellano - Tarde)Mostrar/ocultar subpáginas
Semanas | Lunes | Martes | Miércoles | Jueves | Viernes |
---|---|---|---|---|---|
16-30 | 17:00-18:30 (1) |