Menu Conteúdo Rodapé
  1. Início
  2. Cursos
  3. Engenharia Informática
  4. Segurança e Fiabilidade de Software

Segurança e Fiabilidade de Software

Código 14466
Ano 1
Semestre S2
Créditos ECTS 6
Carga Horária PL(30H)/T(30H)
Área Científica Informática
Objectivos de Aprendizagem Esta UC visa instruir os seus alunos sobre os conceitos, técnicas, ferramentas e aplicações destas à construção e à validação de software fiável e seguro por construção, de programas comprovadamente correctos. Uma introdução a cada família de técnicas é dada mas nem todas são exploradas com todo o detalhe. A abordagem aqui explorada em profundidade introduz as famílias de técnicas que permitem obter um perfil comportamental expressivo dos programas por análise, raciocínio e demonstração. Por natureza este escrutínio não é sempre automático. No entanto, e este é o foco desta UC, este consegue ser suportado e sistematizado computacionalmente, permite uma expressividade e uma granulosidade ímpar quando comparado com outros métodos.
Conteúdos programáticos Os tópicos seguintes serão abordados.

Introdução: problemática, contexto, história e lugar dos Métodos Formais na Engenharia Informática e na Eng. de Software.
Especificar, Modelar e Analisar SIs: Especificação formal, máquina abstracta de estados, lógica de Hoare. Semântica operacional, semântica denotacional
Especificar e Demonstrar Propriedades de SIs: verificação de modelo, sistemas de prova automática, sistemas de ajuda a prova.
Especificar e Derivar Implementações: extracção de programas, refinamento
Especificar en analisar : Análise estática de programas, análise de fluxo de dados, análise de fluxo de controlo, análise de apontadores.
Especificar e Transformar: transformações de especificações/programas, interpretação abstracta.
Metodologias de Ensino e Critérios de Avaliação A avaliação avaliará a aprendizagem teóricas e prática dos conceitos introduzidos com recurso à resoluções de exercícios que consistem em desafios de desenho de programas correctos e seguros por construção e da demonstração de que esses estão inequivocadamente sem bugs que comprometam a sua segurança.

Fraudes
A equipa docente gostaria de realçar que qualquer tipo de fraude em qualquer dos itens desta disciplina implica a reprovação automática do aluno faltoso, podendo ainda vir a ser alvo de processo disciplinar. Listamos a seguir as diferentes componentes da avaliação.

Nota da avaliação contínua mede a aquisição dos conceitos expostos. Como tal é baseada na realização de três exercícios entregue à equipa docente. Alguns exercícios poderão ter uma parte opcional que, se realizada, poderá valorizar a nota do exercício.
A Nota da Avaliação Contínua (NCP, 20 valores) é a média das notas dos exercícios.
Bibliografia principal Livro de Apoio [2] (web-site : aqui)
?
As referências seguintes são complementares ou abordam alguns dos tópticos de forma mais pormenorizada. São assim de leitura secundária para exposição da matéria nesta aula (mas aconselhada para uma aprendizagem mais aprofundada).
Lógica, Indução, Álgebra Universal:[1, 4, 17, 27, 10, 13, 26]
Model Checking: [8, 12]
Lambda Calculo, Teoria de Tipos, Reescrita:[24, 5, 6, 7, 14, 15]
COQ:[9, 23, 11]
Análise Estática: [25, 19]
Fundamentos das Linguagens de Programação, Semântica:[28, 19, 21, 22, 23, 20, 18, 3, 16]
(detalhe em http://www.di.ubi.pt/~desousa/SFS/sfs.html)
Língua Português
Data da última atualização: 2021-06-24
As cookies utilizadas neste sítio web não recolhem informação pessoal que permitam a sua identificação. Ao continuar está a aceitar a política de cookies.