• 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
 
 
Tesis Doctoral
DOI
10.11606/T.3.2009.tde-11082010-164641
Documento
Autor
Nombre completo
Pedro Manuel González Del Foyo
Dirección Electrónica
Instituto/Escuela/Facultad
Área de Conocimiento
Fecha de Defensa
Publicación
São Paulo, 2009
Director
Tribunal
Silva, José Reinaldo (Presidente)
Dórea, Carlos Eduardo Trabuco
Maruyama, Newton
Perkusich, Angelo
Santos Filho, Diolino José dos
Título en portugués
Verificação formal de sistemas discretos distribuídos.
Palabras clave en portugués
Redes de Petri temporizadas
Sistemas discretos
Verificação de modelos
Verificação formal
Resumen en portugués
O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL.
Título en inglés
Formal verification of distribuited discrete systems.
Palabras clave en inglés
Discrete event systems
Formal verification
Model-checking
Time Petri nets
Resumen en inglés
This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.
 
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.
Fecha de Publicación
2010-09-08
 
ADVERTENCIA: El material descrito abajo se refiere a los trabajos derivados de esta tesis o disertación. El contenido de estos documentos es responsabilidad del autor de la tesis o disertación.
  • FOYO, P. M. G., and SILVA, J. R. Some Issues in Real Time Systems Verification Using Time Petri Nets. Journal of the Brazilian Society of Mechanical Sciences and Engineering , 2011, vol. 33, p. 467-474.
  • FOYO, P. M. G. D., and SILVA, J. R. The Verification of Real Time Systems Using the TINA Tool. In 17th IFAC World Congress, Seul, 2008. Proceedings of the 17th IFAC World Congress., 2008.
  • FOYO, P. M. G., and SILVA, J. R. Using Time Petri Nets for Modeling and Verification of Timed Constrained Workflow Systems. In 19th Int. Congress of Mechanical Engineering, Brasilia, 2007. Procc. of 19th Int. Congress of Mechanical Engineering.Brasilia : Universidade de Brasilia, 2007.
  • FOYO, P. M. G., Miralles, J.A.SP., e SILVA, J. R. Um Verificador Formal Eficiente para Sistemas de Tempo Real. In Simpósio Brasileiro de Autumação Inteligente, São João del Rei, 2011. Proceedings do X SBAI., 2011. Dispon?vel em: http://www.sbai2011.ufsj.edu.br/.
  • FOYO, P. M. G., Salmon, A.O., and SILVA, J. R. Requirement Analysis of Automated Projects Using UML/Petri Nets. In Congresso Brasileiro de Engenharia Mecânica, Natal, 2011. Proceedings of COBEM 2011., 2011. Available from: http://www.ufrn.br/cobem2011natal/programme.php.
  • Gonzalez, E.A., et al. Informatic System for Supervision and Control of Processes with Mobile Devices. In Conferencia Brasileira de Dinâmmica, Controle e Aplicações, Fortaleza, 2013. Anais do DINCON 2013., 2013. Available from: http://www.sbai2013.ufc.br.
  • Salmon, A.O., et al. Towards a Unified View of Modeling and Design with GHENeSys. In Congresso Brasileiro de Engenharia Mecânica, Natal, 2011. Proceedings of COBEM 2011., 2011. Available from: http://www.ufrn.br/cobem2011natal/programme.php.
  • SILVA, J. R., et al. Introducing Object-orientation in Unified Petri Net Approach. In 20th Int. Congress of Mechanical Engineering, Gramado, 2009. Procc. of 20th Int. Congress of Mechanical Engineering., 2009.
  • SILVA, J. R., and FOYO, P. M. G. Timed Petri Nets [doi:10.5772/50117]. In Pawel Pawlewski. Petri Nets [online]. Organizador. Rijeka, Croacia : Intech, 2012{Volume}, p. 359-378.http://www.teses.usp.br/teses/disponiveis/3/3152/tde-11082010-164641/
Todos los derechos de la tesis/disertación pertenecen a los autores
Centro de Informática de São Carlos
Biblioteca Digital de Tesis y Disertaciones de la USP. Copyright © 2001-2021. Todos los derechos reservados.