Análise de invariantes é uma das formas de verificação de propriedades em redes de Petri. Faz parte dos chamados métodos estruturais de análise, pois depende apenas da estrutura da rede e não da sua marcação inicial. As vantagens da análise de invariantes sobre outras formas de análise são a possibilidade de se estudar o comportamento de subredes, sem a necessidade de se conhecer o comportamento da rede como um todo, e a utilização de algoritmos conhecidos de Álgebra Linear facilitando os cálculos. A rede estendida Ghenesys é baseada na metodologia PFS/MFG com a introdução de conceitos de orientação a objetos. Entre outras modificações, a rede Ghenesys possui uma equação de estado, o que permite a sua simulação em qualquer nível de abstração e, como é mostrado neste trabalho, permite também a aplicação da análise de invariantes. É mostrado também que, devido à forma estruturada e hierárquica da rede Ghenesys, é possível fazer-se a análise de forma estruturada também, o que é uma vantagem deste método, tanto em termos de desenvolvimento e interpretação como em termos computacionais. Finalmente, o cálculo de invariantes é aplicado num exemplo de rede Ghenesys para validar o método proposto.

Invariant Analysis is one of the methods to verify properties o fone Petri net. It belongs to the group of structural methods, because it is based only on the net structure and is independent of the initial marking. The advantages of Invariant Analysis over other analyzing methods are that analysis can be performed on subnets while ignoring how the whole system behaves and the utilization of known Linear Algebra algorithms to calculate the invariants. Ghenesys is an extended Petri net, based on the PFS/MFG methodology, with the introduction of object-oriented concepts. Among other modifications, Ghenesys has a State Equation, what enables its simulation in any abstraction level and, as it is shown in this work, also enables the application of invariant analysis. Due to the structured and hierarchical formo f Ghenesys, the invariant analysis can be done in a structured way, too, what is an advantage of this method, in the development interpretation and computation of the invariants. Finally, the calculation of invariants is applied in a Ghenesys example to validate the proposed method.