Programa de Ensino 20092
Aprovado pelo Departamento em: 30-7-2009
- Identificação:
- Disciplina: INE5374 - Métodos Formais para Concepção de Sistemas
- Carga horária: 72 horas-aula
Teóricas: 72
Práticas: 0
- Período:
2º semestre de 2009 até a presente data
- Curso(s):
- Ciências da Computação (208)
- Requisito(s):
- Ciências da Computação (208)
- INE5317 - Linguagens Formais e Compiladores
- Ementa:
- Estudo de técnicas formais utilizadas para concepção de sistemas: especificação, verificação e validação.
- Objetivo(s):
- Geral: Conhecer e utilizar ferramentas de especificação formal e verificação de sistemas.
- Específicos:
- Explicar a importância dos métodos formais no desenvolvimento de sistemas de computação.
- Apresentar o papel de métodos formais no processo de desenvolvimento de sistemas de computação.
- Introduzir os conceitos básicos das Redes de Petri e Estelle, ilustrando sobre casos de estudo didáticos.
- Apresentar as principais extensões das Redes de Petri.
- Especificar sistemas simples utilizando-se de técnicas de especificação formal.
- Conteúdo Programático:
- UTILIZANDO MÉTODOS FORMAIS [8 horas-aula]
- Etapas da concepção de sistemas de computação;
- Especificação de Sistemas de Computação
- A validação de sistemas.
- REDES DE PETRI: CONCEITOS [18 horas-aula]
- Origem
- Sintaxe das Redes de Petri
- Paralelismo e Conflito;
- Regras de Disparo de Transições numa Rede de Petri;
- Notação Matricial;
- Grafo de Marcações Acessíveis.
- ANÁLISE DE MODELOS EM REDES DE PETRI [18 horas-aula]
- Propriedades dependentes da marcação (vivacidade, limitação, reinicialização);
- Propriedades estruturais (invariantes de lugar, invariantes de transição);
- Ferramentas de apoio à análise.
- Exemplos ilustrativos.
- REDES DE PETRI DE ALTO NÍVEL [12 horas-aula]
- Redes de Petri Predicado-Transição;
- Redes de Petri Coloridas; Redes de Petri Temporizadas;
- Redes de Petri Temporais.
- A TÉCNICA DE DESCRIÇÃO FORMAL ESTELLE [8 horas-aula]
- Origem da Técnica Estelle;
- Arquitetura de uma especificação Estelle;
- Tipos e Corpos de Módulo, Instâncias de Módulo;
- Estruturação de uma especificação em Estelle;
- Comunicação em Estelle.
- Aspectos de execução de uma especificação em Estelle.
- A SINTAXE DE ESTELLE [8 horas-aula]
- Definição de tipos de módulo e corpos de mdulo.
- Canais e pontos de interação.
- Comandos para criação e conexão de módulos.
- Descrevendo o comportramento em corpos de módulo.
- Transições, pré-condições, pós-condições e ações.
- Exemplos ilustrativos.
- Bibliografia Básica:
- PETERSON, James. Petri Nets Theory and the Modeling of Systems. Ed. Prentice Hall, 1981.
- REISIG, Wolfgang. Petri Nets. Springer Verlag., 1985.
- CARDOSO, Janete, VALETE, Robert. Redes de Petri. Editora UFSC, Florianópolis, 1997.
- Bibliografia Complementar: