Verificação formal de sistemas discretos distribuídos (2009)
- Authors:
- Autor USP: FOYO, PEDRO MANUEL GONZÁLEZ DEL - EP
- Unidade: EP
- Sigla do Departamento: PME
- Subjects: REDES DE PETRI; SISTEMAS DISCRETOS; SISTEMAS DISTRIBUÍDOS
- Language: Português
- Abstract: 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 em 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 (delays) e prazos como é 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 mostrar o desempenho dos algoritmos e um estudo decaso real finaliza a apresentação, onde se pode contrastar os algoritmos propostos com outros de uso comercial no sistema UPPAAL
- Imprenta:
- Data da defesa: 07.12.2009
-
ABNT
GONZÁLEZ DEL FOYO, Pedro Manuel. Verificação formal de sistemas discretos distribuídos. 2009. Tese (Doutorado) – Universidade de São Paulo, São Paulo, 2009. Disponível em: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-11082010-164641/. Acesso em: 24 abr. 2024. -
APA
González Del Foyo, P. M. (2009). Verificação formal de sistemas discretos distribuídos (Tese (Doutorado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/3/3152/tde-11082010-164641/ -
NLM
González Del Foyo PM. Verificação formal de sistemas discretos distribuídos [Internet]. 2009 ;[citado 2024 abr. 24 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-11082010-164641/ -
Vancouver
González Del Foyo PM. Verificação formal de sistemas discretos distribuídos [Internet]. 2009 ;[citado 2024 abr. 24 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-11082010-164641/
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
