iSAQB CPSA-A FM

Descrição

Participar do curso iSAQB® CPSA-A Métodos Formais (FM) concede aos participantes 10 créditos de Competência Técnica (TC), 10 créditos de Competência Metodológica (MC) e 10 créditos de Competência Comunicativa (CC), válidos para os 70 créditos exigidos para prestar o exame iSAQB CPSA-A com a Brightest. É importante lembrar que, como parte dos 70 créditos exigidos para realizar o exame iSAQB CPSA-A com a Brightest, você precisará de pelo menos dez créditos em cada uma das seguintes áreas de competência: 

• Competência Técnica (TC)
• Competência Metodológica (MC)
• Competência Comunicativa (CC)

O treinamento credenciado iSAQB® FM – Métodos Formais (CPSA-A) é baseado no currículo atual do iSAQB®:

Parte 1 – Lógica

• Conhecer a estrutura básica da lógica proposicional
• Conhecer a estrutura básica da lógica de predicados / de primeira ordem
• Conhecer a estrutura básica dos operadores temporais
• Compreender os conceitos básicos de um cálculo lógico
• Compreender a diferença entre lógica intuicionista e lógica clássica

Parte 2 – Especificação e Implementação

• Diferenciar noções de especificação
• Compreender que especificações podem se referir a diferentes tipos de componentes
• Compreender que especificações podem se referir a diferentes qualidades
• Diferenciar especificações formais de outros tipos de especificações
• Conhecer as propriedades distintivas de pelo menos três linguagens de especificação diferentes
• Compreender o conceito de refinamento

Parte 3 – Métodos Formais e o Processo de Desenvolvimento

• Identificar onde os métodos formais são aplicáveis
• Conhecer qualidades relevantes que indicam o uso de métodos formais
• Compreender a relevância da especificação precisa
• Conhecer os trade-offs entre métodos formais
• Introduzir métodos formais gradualmente
• Selecionar métodos formais apropriados
• Avaliar arquiteturas com métodos formais

Parte 4 – Ferramentas

• Aplicar testes baseados em propriedades (property-based testing)
• Compreender o papel dos sistemas de tipos
• Aplicar model checking para verificar propriedades de autômatos
• Aplicar assistentes de prova para verificar propriedades de sistemas de software arbitrários
• Aplicar solucionadores SMT para verificar restrições de sistemas de software