Nome da Atividade
ESPECIFICAÇÃO E VERIFICAÇÃO DE SISTEMAS
CÓDIGO
22000317
Carga Horária
60 horas
Tipo de Atividade
DISCIPLINA
Periodicidade
Semestral
Unidade responsável
CARGA HORÁRIA TEÓRICA
4
FREQUÊNCIA APROVAÇÃO
75%
CARGA HORÁRIA OBRIGATÓRIA
4
CRÉDITOS
4
Ementa
Especificação Formal. Verificação Formal: model-checking e prova de teoremas.
Objetivos
Objetivo Geral:
Apresentar a importância da especificação e verificação formal no desenvolvimento de sistemas confiáveis. Capacitar o aluno a utilizar uma linguagem de especificação formal e aplicar diferentes técnicas de verificação.Conteúdo Programático
Introdução
• O que são métodos formais
• Importância e aplicabilidade dos métodos formais no desenvolvimento de software
• Classificação de métodos formais
• Técnicas de verificação formal
2. Especificação Formal
• Gramática de Grafos
• Ferramenta Groove
• Linguagem Event-B
• Ferramenta Rodin
• Definição e especificação de um estudo de caso
3. Verificação Formal
• Model-checking
• Prova de Teoremas
• Verificação de propriedades do estudo de caso
• O que são métodos formais
• Importância e aplicabilidade dos métodos formais no desenvolvimento de software
• Classificação de métodos formais
• Técnicas de verificação formal
2. Especificação Formal
• Gramática de Grafos
• Ferramenta Groove
• Linguagem Event-B
• Ferramenta Rodin
• Definição e especificação de um estudo de caso
3. Verificação Formal
• Model-checking
• Prova de Teoremas
• Verificação de propriedades do estudo de caso
Bibliografia
Bibliografia Básica:
- EHRIG,H., EHRIG, K., PRANGE, U., TAENTZER, G. Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science - an EATCS Series). New York: Springer-Verlag , 2006.
- ABRIAL, Jean-Raymond. Modeling in Event-B: System and Software Engineering. New York: Cambridge University Press, 2010.
- CLARKE JR., Edmund M., GRUMBERG, Orna, PELED, Doron A. Model Checking. MIT Press, 2000.
Bibliografia Complementar:
- MONIN, Jean Francois Monin. Understanding Formal Methods. New York: Springer-Verlag, 2001.
- BAIER, Christel, KATOEN, Joost-Pieter. Principles of Model Checking (Representation and Mind Series). MIT Press, 2008.
- ROZENBERG, Grzegorz (Ed.). Handbook of Graph Grammars and Computing by Graph Transformation. Volume I. Foundations. World Scientific Publishing Co., 1997.
- SCHUMANN, Johann M. Automated Theorem Proving in Software Engineering. New York: Springer-Verlag, 2001.
- NUNES, Daltro J. Introdução À Abstração de Dados. Bookman, 2012.
Disciplinas Equivalentes
Disciplina | Curso |
---|---|
ESPECIFICAÇÃO E VERIFICAÇÃO DE SISTEMAS | Ciência da Computação (Bacharelado) |
ESPECIFICAÇÃO E VERIFICAÇÃO DE SISTEMAS | Engenharia de Computação (Bacharelado) |