UNIVERSIDADE ESTADUAL DE MARINGÁ

PRÓ-REITORIA DE ENSINO

Diretoria de Ensino de Graduação

Secretaria dos Colegiados de Cursos de Graduação

PROGRAMA DA DISCIPLINA

Departamento de: Informática

Disciplina: Métodos Formais I

Código: 1683 Ano Letivo: 2001 Carga Horária: 68

Curso: INFORMÁTICA

1.EMENTA/2.OBJETIVOS/3.PROGRAMA/4.BIBLIOGRAFIA.

EMENTA: Estudo de métodos formais para desenvolvimento de software.

OBJETIVOS: - Estudar aspectos formais para o desenvolvimento de software;

- Estudar métodos formais para especificação, refinamento e verificação de software;

- Utilizar ferramentas de apoio ao desenvolvimento formal de software;

PROGRAMA:

1. Introdução e motivação

1.1 Formalismo no desenvolvimento de software

1.2 Métodos estruturados versus métodos formais

2. Notações para especificação formal

2.1 Especificações algébricas

2.2 Especificações orientadas a modelos

2.3 Álgebra de processos

2.4 Lógica

2.5 Especificações baseadas em redes

3. Revisão de notações básicas no contexto de engenharia de software

3.1 Conjuntos

3.2 Relações

3.3 Funções (mapeamentos)

3.4 Seqüências

4. A notação Z

4.1 Conjunto e operações sobre conjuntos

4.2 Relações e operações sobre relações

4.3 Funções e relações sobre funções

4.4 Seqüências e operações sobre seqüências

4.5 Esquemas

5. Refinamento

5.1 Refinamento de dados

5.2 Refinamento de operações

6. Estudos de casos

BIBLIOGRAFIA DE REFERÊNCIA

BJORNER, D. & JONES, C.B. Formal Specification and Software Development. Prentice Hall International, Englewood Cliffs, NJ, 1982.

EHRING, H. & MAHR, B. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer-Verlag, 1985.

EHRING, H. & MAHR, B. Fundamentals of Algebraic Specification 2: Module Specification and Constraints. Springer-Verlag, 1990.

FENTON, N. & HILL, G. System Construction and Analysis: A Mathematical and Logical Framework. McGraw-Hall International, 1993.HAYES, I. editor. Specification Case Studies. Prentice Hall International, 1987.

GALTON, A. Temporal Logics and Their Applications. Academic Press, 1987.

HAYES, I. editor. Specification Case Studies. Prentice-Hall International, 1987.

HUGLES, G.E. & CRESSWELL, M.J. An Introduction to Modal Logic. Methues and Co., 1968.

JONES, C.B. Systematic Software Development Using VDW. Prentice-Hall International, 1986.

KROGER, F. Temporal Logic of programs. Springer-Verlag, 1987.

McDERMID, A.J. editor. Software Engineer's Reference Book. Butterworth Heinemann, 1991.

MILNER, R. Commuication and Concurrency. Prentice-Hall International, 1989. ISBN: 0-13-115007-3.

MORGAN, C. Programming from Specifications. Prentice-Hall International, 1990.

PETERSON, J.L. Petri Net Theory and The Modelling of Systems. Prentice-Hall International, 1981.

POTTER, J; SINCLAIR, J. & TILL, D. An Introduction to Formal Specification Using Z. Prentice-Hall International, 1991.

REISING, W. Preti Nets: An Introduction. Springer-Verlag, 1985.

REISING, W. Petri Net in software. In W. Brauner, W. Reising, and G. rozenberg, editora, Petri Nets: Applications and Relations to other Models of Concurrency, LNCS 255. Springer-Verlag, 1987.

SPIVEY, J.M. The Z Notations: A Reference Manual. Prentice Hall International, 1989.

WOODCOCK , J. & LOOMES , M. Software Enginnering Mathematics. Pitman, 1988.

WORDSWORTH, J.B. – Software Development with Z. Addison-Wesley, 1993.

MATTSON JR, H.F. Discrete Mathematics with Applicatons – John Wiley & Sons, Inc, 1993.

GUTTAG, J.V. – Larch: Language and Tools for Formal Specification. Springer-Verlag, 1993.

PERIÓDICOS

Acta Informatica – Springer-Verlag

Communications of the ACM

IEEE Transactions ou Software Engineering