Departamento de Informática e Estatística

Programas de Ensino
Visitante (Entrar)

Programa de Ensino 20092

Aprovado pelo Departamento em: 30-7-2009

  1. Identificação: Visualizar em PDF
    • 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
  2. Curso(s):
    • Ciências da Computação (208)
  3. Requisito(s):
    • Ciências da Computação (208)
      • INE5317 - Linguagens Formais e Compiladores
  4. Ementa:
    • Estudo de técnicas formais utilizadas para concepção de sistemas: especificação, verificação e validação.
  5. Objetivo(s):
    • Geral: Conhecer e utilizar ferramentas de especificação formal e verificação de sistemas.
    • Específicos:
      1. Explicar a importância dos métodos formais no desenvolvimento de sistemas de computação.
      2. Apresentar o papel de métodos formais no processo de desenvolvimento de sistemas de computação.
      3. Introduzir os conceitos básicos das Redes de Petri e Estelle, ilustrando sobre casos de estudo didáticos.
      4. Apresentar as principais extensões das Redes de Petri.
      5. Especificar sistemas simples utilizando-se de técnicas de especificação formal.
  6. 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.
  7. 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.
  8. Bibliografia Complementar: