Contents

• Contents
• Programação concorrente
  • A linguagem SPL
    • Instruções elementares
    • Instruções esquemáticas
    • Instruções compostas
    • Instruções agrupadas
    • Programas
    • Outros
    • Exemplos
  • Problemas de exclusão mútua
  • Exercícios
• Especificação de propriedades temporais
  • Lógica temporal no STeP
    • Sintaxe dos operadores temporais
    • Estrutura de um ficheiro de especificação
  • Classes e exemplos de fórmulas temporais
  • Pequeno caso de estudo
  • Exercícios
• Fair Transition Systems
  • A notação usada nas aulas teóricas
  • Os FTSs no STeP
  • Exercícios
• Métodos de prova para propriedades de invariância
  • A regra B-INV
  • A regra G-INV
  • Utilização das regras B-INV e G-INV no STeP
  • Provas assistidas no STeP
  • Exercícios
• Métodos de prova para propriedades à espera de
  • Fórmulas com apenas um operador
    • A regra B-WAIT
    • A regra G-WAIT
  • Fórmulas com aplicações sucessivas de
  • Exercícios
• Bibliography