- Redes de Petri
-
- Modelação de sistemas concorrentes com redes de
Petri.
- Cálculo de matrizes de incidência.
- Semântica operacional baseada em sistemas de
transição de estados.
- Propriedades fundamentais de redes: finitude,
animação e invertibilidade.
- Cálculo de invariantes de estado.
- Extensões às redes não coloridas: lugares com
capacidade explicita e arcos inibidores.
- Redes coloridas.
- Ferramentas para especificação e animação de
redes de Petri (DaNAMiCS, PEP).
- Verificação de modelos
-
- Especificação de propriedades de segurança e
animação usando lógica temporal.
- Lógicas CTL*, CTL e LTL.
- Representação mínima de fórmulas CTL.
- Verificação directa de modelos para a lógica
CTL.
- Representação da relação de acessibilidade usando
lógica proposicional.
- Verificação simbólica de modelos para a lógica
CTL baseada em OBDDs.
- Ferramentas para verificação simbólica de modelos
(SMV).