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
  

• 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
  

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
    

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

• Entrei na Informal Systems devido a 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
      

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

• Introdução: Programação e matemática não são a mesma coisa
  
• Estruturas de Kripke
  
• Linguagens de especificação formal
  
• Lógica Temporal
  
• Exemplo com semáforos
  
• Motivação para o uso de métodos formais
  
• Lógica Temporal de Ações: TLA+ e Quint
  
• 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
  

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).

As aulas do dias 7, 9 e 14 de outubro serão na modalidade de ensino a distância porque tenho uma viagem de trabalho agendada.

A qualidade do desempenho do aluno será avaliada com base em:

1. Uma prova individual (P) - 30%
   
2. Dois trabalhos práticos (T1 e T2) - 25% cada
   
3. Um seminário (S) - 20%
   

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

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

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.

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.