Exercícios sobre Model Checking
Instale a ferramenta de model checking NuSMV e utilize-a para resolver os seguintes exercícios:
- Verifique que o algoritmo de Peterson para exclusão mútua entre 2 processos satisfaz as seguintes propriedades:
- Exclusão mútua: os processos não estão simultaneamente na região crítica;
- Ausência de starvation: um processo que pretenda aceder à região crítica eventualmente conseguirá;
- Prioridade: o primeiro processo a requisitar o acesso à região crítica é o sempre o primeiro a aceder à dita.
- As seguintes propriedades em lógica temporal não são equivalentes. Tente encontrar sistemas de transição (o mais simples possíveis) que confirmem isso:
-
AG p
e EG p
-
AF p
e EF p
-
AG (p -> p)
e AG (p -> AF p)
-
AG (p -> p)
e AG (p -> AG p)
-
AF (p & q)
e AF p & AF q
-
AG (p | q)
e AG p | AG q
-
AF AX p
e F X p
-
G F p -> G F q
e AG AF p -> AG AF q