• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Disertación de Maestría
DOI
https://doi.org/10.11606/D.45.2007.tde-06032014-080953
Documento
Autor
Nombre completo
Thiago Carvalho de Sousa
Dirección Electrónica
Instituto/Escuela/Facultad
Área de Conocimiento
Fecha de Defensa
Publicación
São Paulo, 2007
Director
Tribunal
Wassermann, Renata (Presidente)
Benevides, Mario Roberto Folhadela
Finger, Marcelo
Título en portugués
Revisão de modelos formais de sistemas de estados finitos
Palabras clave en portugués
CTL
NuSMV
Revisão de Crenças. Verificação de Modelos
Resumen en portugués
Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas.
Título en inglés
Revision of formal models finite state systems
Palabras clave en inglés
Belief Revision
CTL
Model Checking
NuSMV
Resumen en inglés
In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.
 
ADVERTENCIA - La consulta de este documento queda condicionada a la aceptación de las siguientes condiciones de uso:
Este documento es únicamente para usos privados enmarcados en actividades de investigación y docencia. No se autoriza su reproducción con finalidades de lucro. Esta reserva de derechos afecta tanto los datos del documento como a sus contenidos. En la utilización o cita de partes del documento es obligado indicar el nombre de la persona autora.
disser_rev_thiago.pdf (568.20 Kbytes)
Fecha de Publicación
2014-03-17
 
ADVERTENCIA: Aprenda que son los trabajos derivados haciendo clic aquí.
Todos los derechos de la tesis/disertación pertenecen a los autores
CeTI-SC/STI
Biblioteca Digital de Tesis y Disertaciones de la USP. Copyright © 2001-2024. Todos los derechos reservados.