Disciplina Curricular

Software Fiável SFia

Mestrado Bolonha em Engenharia Informática - 3_MEI 2012/13

Contextos

Grupo: 3_MEI 2012/13 > 2º Ciclo > Parte Escolar > Ramos > Engenharia de Software > Optativas > 889_1º Ano do Mestrado em Eng. Inf. - AE (ES) > 1º Semestre

Período:

Grupo: 3_MEI 2012/13 > 2º Ciclo > Parte Escolar > Ramos > Arquitetura, Sistemas e Redes de Computadores > Optativas > 883_1º Ano do Mestrado em Eng. Inf. - AE (ASRC) > 1º Semestre

Período:

Grupo: 3_MEI 2012/13 > 2º Ciclo > Parte Escolar > Ramos > Sistemas de Informação > Optativas > 751_1º Ano do Mestrado em Eng. Inf. - GO (SI) > 1º Semestre

Período:

Grupo: 3_MEI 2012/13 > 2º Ciclo > Parte Escolar > Ramos > Interação e Conhecimento > Optativas > 750_1º Ano do Mestrado em Eng. Inf. - GO (IC) > 1º Semestre

Período:

Peso

6.0 (para cálculo da média)

Objectivos

Pretende-se que o aluno fique a conhecer as principais técnicas e ferramentas que são usadas atualmente durante o processo de desenvolvimento de software, a fim de aumentar a confiabilidade dos sistemas. É colocada ênfase em ferramentas para verificar e monitorar 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 padrão 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 em ferramentas de verificação automática. Além disso, os alunos serão expostos aos mais recentes desenvolvimentos em métodos de confiabilidade 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 confiabilidade de software e verificação formal. Verificação dedutiva do programa e 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.