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: 2018/2019 - 2S

Ativa?	Sim
Página Web:	http://www.dcc.fc.up.pt/~nam/web/Teaching/vfs19/index.html
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	3	PE a partir do ano letivo de 2014	1	-	6	42	162
MI:ERS	5	Plano Oficial desde ano letivo 2014	4	-	6	42	162

Língua de trabalho

Português - Suitable for English-speaking students

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.

Modelação de sistemas reactivos: sistemas de transição e concorrencia. Propriedades Temporais lineares. Lógica temporais: linear (LTL) e ramificada, (CTL e CTL*). Model checkers. 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

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9
Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175

Bibliografia Complementar

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
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.

Software

spin

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	60,00
Trabalho escrito	20,00
Trabalho prático ou de projeto	20,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	80,00
Frequência das aulas	42,00
Trabalho escrito	40,00
Total:	162,00

Obtenção de frequência

Os estudantes devem assistir às aulas teórico-práticas

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

Serão propostos trabalhos práticos durante o semestre. A classificação final é calculada como média aritmética
das classificações dos trabalhos práticos (TP) e do exame (E)  com os seguintes pesos: 04.TP+06*E
Nota mínima: 9.5 em 20

Observações

Conhecimentos de lógica proposicional e de primeira ordem