Este exemplo ilustra a construção do modelo formal do nível de aplicação de uma loja virtual modelada. Este modelo foi elaborado seguindo a metodologia CAFE e os conceitos de verificação formal descritos no texto do livro.
Uma vez instalado o verificador NuSMV, basta executar a seguinte linha de comando:
>> ./NuSMV [arquivo de entrada smv]
O programa produz como saída o resultado da verificação das especificações que
forem definidas no modelo.
As especificações devem ser construídas de acordo com o que se pretende verificar, como ilustra o exemplo a seguir:
- Em algum momento da execução desta loja virtual, o estado do item é disponível? Para verificar isso, a seguinte especificação deve ser elaborada: SPEC EF (item.state = Available)
Voltar
|
