Plano de Estudos

Software Fiável SFia

Contextos

Groupo: 3_MI 2020/21 > 2º Ciclo > Parte Escolar > Optativas > 892 - Mestrado em Informática - Geral > 1º semestre

Groupo: 3_MI 2020/21 > 2º Ciclo > Parte Escolar > Optativas > 787 - Mestrado em Informática - CTP

ECTS

6.0 (para cálculo da média)

Objectivos

Espera-se que os alunos fiquem a conhecer algumas das principais técnicas e ferramentas que podem ser usadas atualmente durante o processo de desenvolvimento de software, a fim de aumentar a fiabilidade dos sistemas de software. A ênfase é em ferramentas para verificar a correção de vários tipos de artefatos produzidos durante o processo de desenvolvimento de software —código, modelos intermediários, projetos, especificações— em relação aos seus requisitos. O uso dessas ferramentas envolve o conhecimento dos modelos formais standard para representar sistemas sequenciais, concorrentes e reativos, e de lógicas para descrever suas propriedades. Espera-se também que os alunos adquiram experiência na utilização de algumas ferramentas de verificação automática. Além disso, os alunos serão expostos aos mais recentes desenvolvimentos em métodos focados na fiabilidade de software, bem como às diferentes estratégias que levam de resultados teóricos para projetos industriais.

Programa

Visão geral dos métodos de fiabilidade de software e verificação formal. Verificação dedutiva de programas e o Cálculo de Hoare. A linguagem de programação Dafny. Design por contrato. Especificação de propriedade com JML (Java Modeling Language), tempo de execução e verificação estática de programas. Verificação de modelos e a ferramenta de verificação SPIN. Estudo de técnicas e ferramentas para análise e verificação de artefatos de software.

Método de Avaliação

Trabalhos e ensaio oral (40%) e exame final (60%).

Carga Horária

Carga Horária de Contacto -

Trabalho Autónomo - 119.0

Carga Total -

Bibliografia

Principal

  • Software Reliability Methods: Doron Peled 2011 Software Reliability Methods,  Doron Peled, Springer, 2001
  • Program Proofs: Rustan Leino 2023

Secundária

  • Principles of the Spin Model Checker: Mordechai Ben-Ari 2008 Principles of the Spin Model Checker. Mordechai Ben-Ari, Springer, 2008

Disciplinas de Execução

2023/2024 - 1 Semestre

2024/2025 - 1 Semestre

2020/2021 - 1º semestre

2026/2027 - 1 Semestre

2022/2023 - 1 Semestre

2025/2026 - 1 Semestre

2021/2022 - 1 Semestre