1.1.1 Essência

Métodos formais são técnicas, embasadas na matemática, que visam verificar que algum hardware/software faz o que se propõe.

As técnicas incluem dois componentes:

• Uma linguagem de especificação
  
• Um sistema de verificação

1.1.2 Histórico da disciplina

• Lá por 2015~2017, ensinava-se uma linguagem chamada Z
  
• Em ~2018, ensinava-se Redes de Petri
  
• Em 2019, o prof Cristiano assumiu a disciplina ensinando Coq
  
• Em 2024/1, eu assumi a disciplina ensinando TLA+ (Temporal Logic of Actions+) e Quint

1.2.1 Sobre Mim

Academia:

• Ciência da Computação - UDESC - 2015-2019
  • TCC: Tradução automática de especificação formal modelada em TLA+ para linguagem de programação
    
• Computação Aplicada - UDESC - 2020-2022
  • Dissertação: Test Generation From TLA+ Specifications

Indústria:

• Magrathea Labs (agora Trusted Health) - 2018-2021
  • Estágio (5 meses) + Engenheira de Software
    
• Informal Systems - 2021-presente
  • Engenheira de Pesquisa

1.2.2 Meu envolvimento com Métodos Formais

• Aprendi TLA+ na graduação para fazer meu TCC, e continuei estudando TLA+ no mestrado
  

• Entrei na Informal Systems devido à pesquisa ativa (minha e deles) em TLA+

  • Muitos engenheiros com dificuldade em aprender e usar TLA+
    

  • Tinham a proposta de uma nova syntaxe para TLA+, que chamamos hoje de Quint

    • Sou a principal desenvolvedora dessa linguagem desde o início de 2022

2.1.1 Plano de ensino

Disponível no SIGA (assim que for aprovado). Vamos ver juntos agora.

1. Objetivo Geral

   Desenvolver habilidades para reconhecimento de cenários, em sistemas computacionais, onde o uso de métodos formais é apropriado; e para aplicação de métodos formais.

2. Objetivo Específico

   • Estimular o senso de necessidade de técnicas que auxiliem a garantir comportamentos em sistemas computacionais.
     
   • Desenvolver a capacidade de abstração ao descrever comportamentos de sistemas em linguagens de especificação formal.
     
   • Trabalhar técnicas de testes baseados em modelos para conectar especificações com implementações.

2.1.2 Conteúdo programático

• Introdução: Programação e matemática não são a mesma coisa
  
• Estruturas de Kripke
  
• Lógica Temporal
  
• Exemplo com semáforos
  
• Motivação para o uso de métodos formais
  
• Linguagens de especificação formal
  
• Lógica Temporal de Ações: TLA+ e Quint
  
• Exemplo com Jogo da Velha
  
• Formulas temporais em TLA+ e Quint
  
• Métodos formais no design de protocolos
  
• Especificações para sistemas distribuídos
  
• Exemplo sobre a efetivação em duas fases (two phase commit)
  
• Verificação vs testes
  
• Testes baseados em modelos
  
• Outros métodos formais
  
• Métodos formais no ciclo de desenvolvimento de software
  
• Model checking
  
• Refinamento
  
• Model values e conjuntos de simetria

2.1.3 Metodologia

A disciplina será desenvolvida através de aulas expositivo-dialogadas, com exercícios e trabalhos práticos, e seminários. O conteúdo da disciplina poderá ser ministrado na modalidade de ensino a distância em até 20% do total de sua Carga Horária (MEC PORTARIA No 4.059, DE 10 DE DEZEMBRO DE 2004 publicado no DOU de 13/12/2004, Seção 1, p. 34).

2.2.1 Do desempenho do aluno

A qualidade do desempenho do aluno será avaliada com base em:
a) Uma prova individual (P) - 30%
b) Dois trabalhos práticos (T1 e T2) - 25% cada
c) Um seminário (S) - 10%
d) Exercícios (E) - 10%

Assim, a Média Semestral (MS) será calculada pela fórmula

MS = (30 * P + 25 * T1 + 25 * T2 + 10 * S + 10 * E)/100

2.2.2 OFF: guia para navegar as avaliações

• O trabalho 1 é o mais trabalhoso e importante
  

• O seminário é bem simples, mas não deixem de fazer porque depois a nota faz falta
  • É também mais no início do semestre onde vocês tem mais tempo livre
    

• Os exercícios existem exclusivamente para prepará-los para o primeiro trabalho.
  • Eu não estava cobrando até semestre passado, mas decidi cobrar para incentivá-los a não chegarem despreparados para o trabalho.
    

• O trabalho 2 é bem tranquilo. Pensem nele como um impulso extra para passar (e não como um motivo de desistir).

2.2.3 Exame

Caso o discente não obtenha média MS igual ou superior a 7,0, um exame escrito será aplicado objetivando aferir o conhecimento teórico do estudante. Não há recuperação das provas por não comparecimento, exceto nos casos previstos no regulamento da UDESC na resolução 0392015 - CONSEPE.

2.2.4 Do desempenho da disciplina e da professora

Os estudantes terão, igualmente, a oportunidade de fazer uma avaliação do desempenho da professora e da disciplina. As informações sobre esta atividade serão fornecidas pelo coordenador do curso.

2.3.1 Bibliografia básica

(BAIER; KATOEN, 2008; LAMPORT, 2002; MONIN; HINCHEY, 2001)

2.3.2 Bibliografia complementar

(KONNOV; KUKOVEC, 2022; LAMPORT, 2024; TEAM, 2024)