Verificação formal de sistemas modelados em estados finitos (2006)
- Autores:
- Autor USP: FERREIRA, NELSON FRANCA GUIMARAES - EP
- Unidade: EP
- Sigla do Departamento: PCS
- Assuntos: AMBIENTES DE PROGRAMAÇÃO; VERIFICAÇÃO E VALIDAÇÃO DE SOFTWARE
- Idioma: Português
- Resumo: Este trabalho reflete os esforços realizados no estudo das principais técnicas automáticas de verificação de sistemas que podem ser modelados em Máquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominação de model checking (verificação de modelos). De modo a permitir ao leitor uma compreensão das vantagens e desvantagens de cada técnica, os fundamentos teóricos de cada uma delas são apresentados e ilustrados através de exemplos. Além de uma apresentação da teoria associada a cada técnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante prático: a verificação de propriedades de um sistema de manufatura originalmente modelado através de uma rede de Petri e a verificação de propriedades do intertravamento de uma seção metroviária. Os dois estudos de caso utilizam técnicas denominadas simbólicas. No primeiro estudo de caso, propõe-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 verificação. O segundo estudo de caso é resolvido a partir da utilização de um procedimento proposto nesta dissertação. Este procedimento permite a verificação de algumas propriedades de segurança sem que a verificação se inviabilize devido à explosão no número de estados. A utilização deste procedimento permite a verificação de propriedades de uma seção de intertravamento com cerca de 2000 variáveis digitais em questão de poucossegundos. A principal conclusão a que este trabalho chega é conseqüência dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicações ainda por ser mais bem explorado
- Imprenta:
- Data da defesa: 09.03.2006
-
ABNT
FERREIRA, Nelson França Guimarães. Verificação formal de sistemas modelados em estados finitos. 2006. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2006. Disponível em: http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/. Acesso em: 18 abr. 2024. -
APA
Ferreira, N. F. G. (2006). Verificação formal de sistemas modelados em estados finitos (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/ -
NLM
Ferreira NFG. Verificação formal de sistemas modelados em estados finitos [Internet]. 2006 ;[citado 2024 abr. 18 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/ -
Vancouver
Ferreira NFG. Verificação formal de sistemas modelados em estados finitos [Internet]. 2006 ;[citado 2024 abr. 18 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/
Como citar
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
