Los sistemas de software de dimensión industrial suelen contener un número significativo de errores y
deficiencias de distintos tipos. Una de las metodologías aceptadas, por la comunidad académica de la
Ingeniería de Software, para mitigar estos problemas es la introducción de métodos formales de desarrollo.
También se acepta que no existe un único método formal que pueda cubrir todas las necesidades. Por estos
motivos la asignatura se centra en un menú variado de métodos formales con los cuales podrán modelar y
especificar sistemas de software. La asignatura incluye la realización de un proyecto de desarrollo usando
métodos formales que se completa durante el cursado de Ingeniería de Software II. Con este fin los alumnos
seleccionan un requerimiento funcional de baja complejidad, escriben una especificación formal de aquel,
traducen la especificación formal a un lenguaje de implementación de alto nivel y realizan un par de actividades
de verificación. Por un lado, la asignatura se relaciona con los cursos dedicados a la programación y a la
lógica en tanto muestra cómo se puede modelar un programa usando formalismos lógicos, pero sin usar
código fuente. Por otro lado, se complementa con Ingeniería de Software II en tanto allí se introducen las
nociones de diseño y arquitectura de software que constituyen otra mirada posible sobre un sistema de
software. Finalmente, se relaciona con Seguridad Informática dado que allí se usan formalismos lógicos para
estudiar propiedades de seguridad de la información.

Enlaces útiles:

• Sitio web
• Comunidades