Ver registro no DEDALUS
Exportar registro bibliográfico

Verificação formal de sistemas modelados em estados finitos (2006)

  • Authors:
  • USP affiliated authors: FERREIRA, NELSON FRANCA GUIMARAES - EP
  • USP Schools: EP
  • Sigla do Departamento: PCS
  • Subjects: AMBIENTES DE PROGRAMAÇÃO; VERIFICAÇÃO E VALIDAÇÃO DE SOFTWARE
  • Language: Português
  • Abstract: 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
  • Acesso online ao documento

    Online access or search this record in

    Exemplares físicos disponíveis nas Bibliotecas da USP
    BibliotecaCód. de barrasNúm. de chamada
    EPBC31200008727FD-4265
    How to cite
    A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas

    • ABNT

      FERREIRA, Nelson França Guimarães; SILVA, Paulo Sérgio Muniz. Verificação formal de sistemas modelados em estados finitos. 2006.Universidade de São Paulo, São Paulo, 2006. Disponível em: < http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/ >.
    • APA

      Ferreira, N. F. G., & Silva, P. S. M. (2006). Verificação formal de sistemas modelados em estados finitos. 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, Silva PSM. Verificação formal de sistemas modelados em estados finitos [Internet]. 2006 ;Available from: http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/
    • Vancouver

      Ferreira NFG, Silva PSM. Verificação formal de sistemas modelados em estados finitos [Internet]. 2006 ;Available from: http://www.teses.usp.br/teses/disponiveis/3/3141/tde-19092006-134100/

    Últimas obras dos mesmos autores vinculados com a USP cadastradas na BDPI: