Português English
Contato

Lista de Disciplinas | CMP567

Tópicos Especiais em Computação: Teste e Verificação de Software

ResponsávelLeila Ribeiro e Lucio Duarte
Carga Horária: 60 hs
Créditos: 4
Semestres Oferecidos: Segundo semestre

SÚMULA
Técnicas de verificação estática e dinâmica. Modelos de comportamento: tipos, modelagem, verificação. Verificadores de modelos. Provadores de teoremas.

OBJETIVOS
O principal objetivo da disciplina é apresentar conceitos e técnicas fundamentais de verificação de software e sua inserção dentro do desenvolvimento de um software, além de oportunizar a aplicação prática destes conceitos e permitir a discussão das vantagens e limitações de cada técnica apresentada. Ao final da disciplina, espera-se que o aluno: (i) entenda a importância da validação e verificação para a qualidade de sistemas computacionais; (ii) possua capacidade de criar modelos de comportamento para sistemas simples; (iii) compreenda o funcionamento de verificadores de modelo e saiba utilizá-los para verificar propriedades; (iv) possua conhecimentos básicos de prova de teoremas e esteja habilitado a utilizar uma ferramenta que usa esta técnica de verificação; (v) conheça os principais desafios em verificação de software.

PROGRAMA
Semana 1 – Introdução

– Apresentação da disciplina
– Conceitos básicos de validação e verificação;
– Aplicação de validação verificação no ciclo de desenvolvimento de software e sua importância.

Semanas 2 a 7 – Prova de Teoremas
– Revisão de Teoria dos Conjuntos e Lógica de Primeira Ordem
– Especificação de propriedades
– Introdução à Prova de Teoremas
– Provadores de teoremas
– Exercícios com ferramenta de apoio
– Tópicos avançados em Prova de Teoremas
– Realização de trabalho prático

Semanas 8 a 13 – Verificação de modelos
– Introdução a Lógica Temporal
– Lógica Temporal Linear (LTL)
– Especificação de propriedades em LTL
– Introdução à Verificação de Modelos
– Modelagem de sistemas
– Uso de verificadores de modelos
– Realização de trabalho prático

Semanas 14 a 15 – Apresentação de trabalhos
– Apresentação de trabalho comparativo entre o uso de Prova de Teoremas e Verificação de Modelos e suas aplicações em atividades de desenvolvimento de software

CRITÉRIOS DE AVALIAÇÃO

Serão realizados três trabalhos, T1, T2 e T3, considerando os seguintes conteúdos:

– T1: Especificação de propriedades
– T2: Prova de Teoremas
– T3: Verificação de Modelos

Os trabalhos T2 e T3 serão práticos, utilizando as ferramentas computacionais de apoio da disciplina, enquanto os trabalhos T1 e T4 incluirão a confecção de um relatório e apresentação em aula.
A média final (M) será calculada da seguinte forma:

M = (0,2 * T1) + (0,4 * T2) + (0,4 * T3)

A conversão da média M para conceitos será realizada como descrito a seguir:

Faltas > 25% : FF (reprovado)
M < 6.0 : sem conceito (recuperação) – ver Atividades de Recuperação Previstas
6.0<= M < 7.5 : C (aprovado)
7.5 <= M < 9.0 : B (aprovado)
9.0 <= M : A (aprovado)

Obs: Somente serão calculadas as médias finais daqueles alunos que obtiverem, ao longo do semestre, um índice de freqü.ncia às aulas igual ou superior a 75% das aulas previstas. Aos que não satisfizerem este requisito, será atribuído o conceito FF (Falta de Frequencia).

Para poder realizar a prova de recuperação, o aluno deve ter um índice de frequência de no mínimo 75% das aulas. Os que não se enquadrarem nesta situação terão conceito FF. A recuperação versará sobre toda a matéria da disciplina. Serão considerados aprovados na recuperação os alunos que obtiverem um aproveitamento de, no mínimo, 60% da prova. A estes será atribuído o conceito C. Aos demais, será atribuído o conceito D. Não há recuperação dos trabalhos por não comparecimento/entrega, exceto nos casos previstos na legislação (saúde, parto, serviço militar, convocação judicial, luto, etc.), sendo necessária a devida comprovação.

BIBLIOGRAFIA

Clarke, E. M.; Grumberg, O.; Peled, D. A.. Model Checking. The MIT Press, 1999. ISBN 0262032708.
Jastram, M.; Butler, M.. Rodin User’s Handbook v.2.8. CreateSpace Independent Publishing Platform, 2014. ISBN 978-1495438141. Disponível em: http://handbook.event-b.org
Event-B (Rodin platform). Disponível em: http://www.event-b.org/
Rodin (project Deploy). Disponível em: http://www.deploy-project.eu/ Magee, J.; Kramer, J.. Concurrency: State Models and Java Programming. Wiley, 2006. ISBN 978-0-470-09355-9.