• 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
 
 
Doctoral Thesis
DOI
10.11606/T.3.2009.tde-11082010-164641
Document
Author
Full name
Pedro Manuel González Del Foyo
E-mail
Institute/School/College
Knowledge Area
Date of Defense
Published
São Paulo, 2009
Supervisor
Committee
Silva, José Reinaldo (President)
Dórea, Carlos Eduardo Trabuco
Maruyama, Newton
Perkusich, Angelo
Santos Filho, Diolino José dos
Title in Portuguese
Verificação formal de sistemas discretos distribuídos.
Keywords in Portuguese
Redes de Petri temporizadas
Sistemas discretos
Verificação de modelos
Verificação formal
Abstract in Portuguese
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.
Title in English
Formal verification of distribuited discrete systems.
Keywords in English
Discrete event systems
Formal verification
Model-checking
Time Petri nets
Abstract in English
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.
 
WARNING - Viewing this document is conditioned on your acceptance of the following terms of use:
This document is only for private use for research and teaching activities. Reproduction for commercial use is forbidden. This rights cover the whole data about this document as well as its contents. Any uses or copies of this document in whole or in part must include the author's name.
Publishing Date
2010-09-08
 
WARNING: The material described below relates to works resulting from this thesis or dissertation. The contents of these works are the author's responsibility.
  • 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/
All rights of the thesis/dissertation are from the authors
Centro de Informática de São Carlos
Digital Library of Theses and Dissertations of USP. Copyright © 2001-2020. All rights reserved.