Institutional PortalUFPEL

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.

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 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.
• 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.
• ROZENBERG, Grzegorz (Ed.). Handbook of Graph Grammars and Computing by Graph Transformation. Volume I. Foundations. World Scientific Publishing Co., 1997.