Métodos Formais no Projecto de Software

A área dos métodos formais inclui todas as aplicações da matemática discreta a problemas de engenharia de software. Os métodos formais, aplicados ao desenvolvimento de software, recorrem a linguagens formais para descrever os artefactos de software (especificações, arquitecturas e código), permitindo a prova formal de propriedades, bem como a reificação dos mesmos para suporte à implementação.

Esta unidade curricular, irá focar-se no estudo do desenvolvimento de sistemas de software baseado em Métodos Formais, com ênfase para as técnicas de especificação baseadas em modelos da matemática discreta, que conduzem ao cálculo de sistemas de informação com garantia de correcção e à certificação de software por construção correcta e/ou verificação.

Programa resumido

• Introdução ao problema do controlo de qualidade em 'software'. Especificação formal -- porquê e para quê? Introdução ao binómio especificação vs implementação.
• Introdução Métodos Formais: taxonomia, ciclo de vida, certificação. Discussão de áreas típicas de aplicação: sistemas críticos e confiáveis; áreas da saúde e da segurança; qualidade de serviços; sistemas de informação avançados.
• Linguagens e métodos para especificação formal. Antecendentes históricos. Do método de Viena (VDM) ao 'standard' ISO/IEC 13817-1 (VDM-SL).
• Estudo da notação VDM-SL. Modelação por conjuntos, sequências e funções.
• Propriedades invariantes. Obrigações de prova.
• Prototipagem e animação. Ambientes de desenvolvimento formal. Experiência com a utilização do ambiente VDMTOOLS.
• Especificação formal por objectos (VDM++). Integração com UML.

Resultados de Apreendizagem Específicos

• Modelar os requisitos de um sistema de software numa linguagem de especificação formal construtiva.
• Raciocionar dentro dos modelos produzidos de forma rigorosa, identificando propriedades e obrigações de prova.
• Utilizar um ambiente de prototipagem de especificações formais.
• Ter uma percepção clara do lugar destes métodos no projecto de sistemas informáticos complexos: áreas de aplicação, formas de introdução, relação com os níveis de modelação semi-formais (e.g., UML) e com o desenvolvimento de código.

-- 08 May 2007