Exclusão Mútua e Intertravamento
Modelar múltiplos processos competindo por recursos compartilhados. Deadlock não é um bug aleatório — é um padrão que você pode visualizar e eliminar.
SISTEMAS CONCORRENTES · VERIFICAÇÃO FORMAL
De código bugado
A comportamento provado.
Modele, simule e verifique formalmente o comportamento de sistemas concorrentes.
Protocolos, deadlock, liveness e sincronização: explore a modelagem de sistemas concorrentes com Redes de Petri. Conheça os cursos de fundamentos e temas que poderiam ser aprofundados em parceria.
Fundamentos para começar. Possibilidades de parceria em engenharia de computação.
LABORATÓRIO INTERATIVO
MUTEX · EXCLUSÃO MÚTUA
Um recurso compartilhado. Dois processos.
DEMODispare uma transição e observe como a exclusão mútua funciona.
Processo A
Processo B
Processo esperando
0 transições
Exclusão mútua simplificada · Um token = um recurso. Apenas um processo pode estar na seção crítica.
TEORIA E PRÁTICA INTEGRADAS
Redes de Petri
/Sistemas concorrentes
/Verificação formal
O PROBLEMA DO ENGENHEIRO
Como garantir que seu código
nunca terá deadlock?
Testes unitários passam. Testes de integração passam. Mas em produção, sob concorrência, algo quebra. A diferença entre código que parece funcionar e código que você pode provar que funciona.
Sincronização e Ordenação
Protocolos de comunicação, handshake, semáforos. Redes de Petri transformam exigências informais em especificações precisas que você pode verificar.
Propriedades Formais Provadas
Safety (nunca acontece algo ruim), Liveness (eventualmente acontece algo bom). Não é simulação — é prova matemática de comportamento.
APRENDER FAZENDO
Do modelo
à prova de correção.
Use os fundamentos de Redes de Petri para investigar sistemas concorrentes. Protocolos e verificação formal são temas com potencial para projetos colaborativos de ensino e pesquisa.
Explorar a plataforma-
01
Modele
Desenhe protocolos e processos concorrentes como redes de Petri. Cada lugar é um estado; cada transição é um evento.
-
02
Simule
Execute a rede manualmente. Veja como estados evolem, onde os deadlocks podem ocorrer, como a sincronização funciona.
-
03
Verifique
Use análise de alcançabilidade para explorar todos os estados possíveis. Procure por estados ruins (deadlock) e prove que não existem.
-
04
Prove
Descubra invariantes e propriedades. Conecte a teoria formal ao seu código real — e veja onde a implementação diverge do modelo.
Antes de começar
Que cursos estão disponíveis agora?
Disponíveis imediatamente:
- Jogo de Damas — Intuição visual e operação da ferramenta
- Introdução às Redes de Petri — Fundamentos completos (7 lições, 48 exercícios)
Estes cursos oferecem a base necessária para explorar qualquer trilha, inclusive sistemas concorrentes.
Que temas poderiam ser explorados em parceria na computação?
Possibilidades para explorar em parceria:
- Modelagem de Sistemas Concorrentes — Protocolos, deadlock e sincronização
- Análise de Concorrência — Propriedades formais, liveness e safety
- Pesquisa em Métodos Formais — Redes coloridas, estocásticas e verificação com model checking
Esses temas poderiam ser explorados em cursos, projetos de pesquisa ou extensão em parceria com docentes, pesquisadores, instituições de ensino e organizações interessadas.
Por onde começo?
Recomendamos:
- Jogo de Damas (15-30 min) — Entenda a interface
- Introdução às Redes de Petri (10-15 horas) — Aprenda a teoria
O curso Jogo de Damas é gratuito e apresenta a interface de forma prática.
Preciso de C++, Java ou outro código?
Não. O WebAPN é um ambiente visual e formal. Você trabalha com redes, não com código. Mas depois que dominar a modelagem, as técnicas se aplicam diretamente: usar semáforos em pthreads, protocolos em microserviços, invariantes em sistemas distribuídos.
Cursos e possibilidades de parceria
Esses temas poderiam ser explorados em cursos, projetos de pesquisa ou extensão em parceria com docentes, pesquisadores, instituições de ensino e organizações interessadas.
✅
Disponível Agora
- Jogo de Damas
- Introdução às Redes de Petri
◇
Temas para projetos em parceria
- Modelagem de Sistemas Concorrentes
- Análise de Concorrência
◇
Possibilidades de pesquisa e extensão
- Redes Coloridas (CPN)
- Redes Estocásticas
- Verificação Formal (Model Checking)
COMECE AGORA
Modele sistemas que você
pode provar que funcionam.
Comece pelo curso gratuito Jogo de Damas e conheça o curso Introdução às Redes de Petri.
Conhecer os cursos