Português English
Contato

Lista de Disciplinas | CMP150

Métodos Formais

Responsável: Daltro José Nunes
Pré-Requisitos: –
Carga Horária: 60 hs
Créditos: 4
Semestres Oferecidos: Primeiro semestre
Matrícula de Graduandos: A matricula deverá ser feita como Aluno Especial
Página da Disciplina: –

SÚMULA

Métodos formais, especificação formal, prova da especificação, prova da implementação.

OBJETIVOS

O objetivo da disciplina é apresentar os métodos formais mais importantes na especificação seja de protocolos, de escritórios, de modelos de Banco de Dados, de sistemas operacionais ou de sistemas em geral. Ao final da disciplina o aluno tem condições de identificar o problema e escolher um método formal para apresentar a solução (a especificação). É capaz também de verificar a especificação, de implementar e de provar a implementação contra a especificação.

PROGRAMA

Métodos: Algebrico, VDM, CCS, LOTOS, Z, entre outros
Prova da Especificação
Prova da Implementação

CRITÉRIOS DE AVALIAÇÃO

Os alunos devem estudar um método formal a sua escolha e apresentar um seminário.

BIBLIOGRAFIA

• COHEN, B.; HARWOOD, W. T.; JACKSON, M. I. The specification of complex systems. Reading: Addison- Wesley, 1986.
• GRIES, D. The science of programming. New York: Springer-Verlag, 1981.
• LOGRIPPO, L.; FACI, M.; HAJ-HUSSEIN, M. An introduction to LOTOS: learning by examples. Computer
• Networks and ISDN Systems, v. 23, n. 5, p. 325-342, 1992.
• Especificações em Z. ARNALDO VIEIRA MOURA – Editora Unicamp.
• The Spec# programming system: An overview. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. In CASSIS 2004, LNCS vol. 3362, Springer, 2004.