Formal verification of systems modeled as finite state machines. / Verificação formal de sistemas modelados em estados finitos.
AUTOR(ES)
Nelson França Guimarães Ferreira
DATA DE PUBLICAÇÃO
2006
RESUMO
Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado
ASSUNTO(S)
verificação formal de sistemas de estados finitos verificação formal de sistemas de software programming systems software formal verification formal verification or finite-state systems model checking model checking sistemas de programação
Documentos Relacionados
- Verificação formal de sistemas discretos distribuídos.
- Chemical implementation of finite-state machines.
- Minimização de conjuntos de casos de teste para máquinas de estados finitos
- Geração automática de casos de testes para máquinas de estados finitos
- Test case generation for space area systems using test criteria for finite state machines
