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

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)

Página gerada em 04/10/2024 05:31:45 (consulta levou 0.113865s)