Segurança e Fiabilidade de Software

Imagem d@ André de Matos Pedro [Ficheiro Local]
André de Matos Pedro
Código:
17948
Ano:
1
Semestre:
S1
Créditos ECTS:
6
Carga Horária:
PL(30H)/T(30H)
Área Científica:
Informática
Objectivos de Aprendizagem:
Os objetivos de aprendizagem gerais consistem em
• Compreender o ciclo de vida de sistemas de software seguros e fiáveis, desde a especificação até à verificação, utilizando técnicas baseadas em formalismos matemáticos (métodos formais).
• Conhecer os métodos e técnicas formais modernos, quando devem ser aplicados e quais são os mais adequados em cada fase dos sistemas de software seguros e fiáveis.
• Aplicar os métodos e técnicas formais na especificação e verificação de sistemas de software seguros e fiáveis.
Conteúdos programáticos:
• Introdução de linguagens de especificação e programação para construção de software seguro e fiável
• Lógicas para especificação formal: Lógica proposicional, lógica de primeira ordem e lógica temporal
• Técnicas de prova automática: SAT solving para lógica proposicional, SMT solving para lógica e teorias de primeira ordem, Bounded model-checking via SAT para lógica temporal
• Especificação de Programas: Linguagens de domínio para especificação comportamental, propriedades de segurança de execução e propriedades funcionais, especificação com base em contratos
• Verificação estática de programas: condições de verificação para programas com contratos
• Verificação dinâmica de programas: monitorização em tempo de execução com contratos
• Introdução aos métodos formais para sistemas ciber-físicos
Metodologias de Ensino e Critérios de Avaliação:
Para avaliar as competências adquiridas, as atividades de ensino-aprendizagem avaliam a compreensão dos conceitos teóricos apresentados e a capacidade de os pôr em prática. Esta avaliação será efetuada através de um teste escrito e de uma avaliação contínua baseada em exercícios práticos.

NF = Nota final
NCP = Nota da componente prática (avaliação dos exercícios)
NCT = Nota da componente teórica (prova escrita - exame ou frequência)
NF = Se (NCT >= 6 e NCP >= 6) então (NCT + NCP)/2, caso contrário Reprovado/Não Admitido
Bibliografia principal:
Michael Huth & Mark Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press; 2nd edition (2004).

Aaron R. Bradley & Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer (2007).

J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer (2011).
Língua:
Português