Verificação Formal de Software

Código:

CC447

Sigla:

CC447

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

Ocorrência: 2013/2014 - 2S

Ativa?	Sim
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado Integrado em Engenharia de Redes e Sistemas Informáticos

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	7	PE do Mestrado em Ciência de Computadores	1	-	7,5	67	202,5
MI:ERS	20	Plano de Estudos a partir de 2007	4	-	7,5	67	202,5

Língua de trabalho

Portuguê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 de modo a garantir propriedades de segurança e propriedades funcionais; e de especificar teorias que permitam a modelação de estruturas mais complexas, cuja correção será́ demonstrada por um demonstrador automático ou interativo.

Modo de trabalho

Presencial

Pré-requisitos (conhecimentos prévios) e co-requisitos (conhecimentos simultâneos)

Conhecimentos prévios de Lógica e Linguagens de Programação.

Programa

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: geradores de condições de verificação.
Demonstração automática.
Introdução à demonstração assistida.

Verificação por model checking de sistemas reactivos
Sistemas reactivos
Lógica temporais: linear (LTL), ramificada, (CTL e CTL*) e dinâmica.
(model checkeres):NUSMV
Model checking simbólico: BDDs e OBDDs
Algoritmos de decisão baseados em autómatos finitos

Bibliografia Obrigatória

Michael Huth and Mark Ryan; Logic in Computer Science: Modelling and reasoning about systems. , 2004
Bertot Yves; Interactive theorem proving and program development. ISBN: 9783540208549 hbk

Bibliografia Complementar

Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen; Principles of Model Checking, MIT Press, 2008
Winskel Glynn; The formal semantics of programming languages. ISBN: 978-0-262-23169-5
Benjamin C. Pierce; Software Foundations
José Bacelar Almeida,Jorge Sousa Pinto,Maria João Frade,Simão Melo de Sousa ; Rigorous Software Development: An Introduction to Program Verification, Springer-Verlag, 2011. ISBN: 978-0-85729-017-5

Métodos de ensino e atividades de aprendizagem

Aulas teóricas e aulas práticas com resoliução de trabalhos.

Software

http://coq.inria.fr/
http://nusmv.fbk.eu/
http://why.lri.fr/

Palavras Chave

Ciências Físicas > Ciência de computadores

Tipo de avaliação

Avaliação distribuída sem exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	60,00
Trabalho laboratorial	40,00
Total:	100,00

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

Avaliação com exame final. A avaliação é composta por:
1. realização e apresentação de dois trabalhos práticos (T1 e T2)
2. exame final (E)
A classificação final é obtida por:
F=(T1*4 + T2*4 + E*12)/20
Para aprovação é necessário que F>=9.5