• 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
 
 
Tese de Doutorado
DOI
10.11606/T.3.2009.tde-11082010-164641
Documento
Autor
Nome completo
Pedro Manuel González Del Foyo
E-mail
Unidade da USP
Área do Conhecimento
Data de Defesa
Imprenta
São Paulo, 2009
Orientador
Banca examinadora
Silva, José Reinaldo (Presidente)
Dórea, Carlos Eduardo Trabuco
Maruyama, Newton
Perkusich, Angelo
Santos Filho, Diolino José dos
Título em português
Verificação formal de sistemas discretos distribuídos.
Palavras-chave em português
Redes de Petri temporizadas
Sistemas discretos
Verificação de modelos
Verificação formal
Resumo em 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 em inglês
Formal verification of distribuited discrete systems.
Palavras-chave em inglês
Discrete event systems
Formal verification
Model-checking
Time Petri nets
Resumo em 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.
 
AVISO - A consulta a este documento fica condicionada na aceitação das seguintes condições de uso:
Este trabalho é somente para uso privado de atividades de pesquisa e ensino. Não é autorizada sua reprodução para quaisquer fins lucrativos. Esta reserva de direitos abrange a todos os dados do documento bem como seu conteúdo. Na utilização ou citação de partes do documento é obrigatório mencionar nome da pessoa autora do trabalho.
Data de Publicação
2010-09-08
 
AVISO: O material descrito abaixo refere-se a trabalhos decorrentes desta tese ou dissertação. O conteúdo desses trabalhos é de inteira responsabilidade do autor da tese ou dissertação.
  • 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 os direitos da tese/dissertação são de seus autores
Centro de Informática de São Carlos
Biblioteca Digital de Teses e Dissertações da USP. Copyright © 2001-2018. Todos os direitos reservados.