Sistemas Operacionais

Aula 10: Verificação

Verificação de Programas Paralelos

 Extremamente difícil:

Extremamente importante:

Porque tão difícil ?

 Composição paralela de processos é cara:

Se P1 tem m estados e P2 tem n estados, P1 X P2 tem m * n estados!

Explosão de estados.

Teste

Implementa-se o programa e executa-se o mesmo ad nauseam.

Vantagem: simples, eficiente

Desvantagem: cobertura de falhas muito baixa.

Verificação Formal

Prova-se que o programa está correto:

Métodos matemáticos que derivam propriedades do sistema baseado em assunções e teoremas.

Necessários se você quer confiar no seu programa!

Provadores de Teoremas

Provadores de teoremas são programas que dado:

Provadores de Teoremas

Prova Manual por Invariantes

Prova Manual por Invariantes

 
better_lock(k) {

  lock(k->mutex);

  if (!k->free)

    sleep(k->bed, k->mutex);

  k->free = 0;

  unlock(k->mutex);

}





better_unlock(k);





  lock(k->mutex);





  k->free = 1;





  wakeup(k->bed);





  unlock(k->mutex);





}









	 Prova Manual por Invariantes












Last Modified: 01:49pm , December 16, 1998