Verificação Formal de Software

Código:

CC4008

Sigla:

CC4008

Nível:

400

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2015/2016 - 2S

Ativa?	Sim
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado em Ciência de Computadores

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
M:CC	13	PE a partir do ano letivo de 2014	1	-	6	42	162
MI:ERS	15	Plano Oficial desde ano letivo 2014	4	-	6	42	162

Língua de trabalho

Inglês

Objetivos

Estudo e utilização de técnicas formais baseadas em modelos e em demonstração aplicadas à verificação de sistemas e programas.

Resultados de aprendizagem e competências

Pretende-se que o aluno:

- em ambas as vertentes, perceba a importância da utilização da lógica e dos sistemas formais no desenvolvimento de sistemas informáticos complexos;

- seja capaz de modelar sistemas simples e de especificar propriedades utilizando lógicas temporais;

- seja capaz de anotar programas simples duma linguagem imperativa ou orientada a objetos de modo a garantir propriedades de segurança e propriedades funcionais.

Modo de trabalho

Presencial

Programa

- Verificação por model checking de sistemas reactivos.

Sistemas reactivos. Lógica temporais: linear (LTL) e ramificada, (CTL e CTL*). Model checkers. NUSMV. Model checking simbólico: BDDs e OBDDs. Algoritmos de decisão baseados em autómatos finitos.

- Verificação de programas.

Cálculos de correção (Lógica de Hoare). Geração de obrigações de prova. Ferramentas para a especificação, verificação e certificação de programas imperativos.

Bibliografia Obrigatória

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175

Bibliografia Complementar

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9
Bérard Béatrice 070; Systems and software verification. ISBN: 9783540415237

Métodos de ensino e atividades de aprendizagem

Aulas expositivas e resolução de problemas e casos de estudo.

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	50,00
Teste	50,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	50,00
Frequência das aulas	50,00
Total:	100,00

Fórmula de cálculo da classificação final

A classificação final é calculada como média aritmética de um teste a meio do semestre e um segundo teste a realizar na época normal de exames.

Melhoria de classificação

Os alunos que não tiveram aprovação através da realização dos dois testes, ou que queiram melhorar a classificação obtida, podem fazê-lo na época de recurso.