Modelo Formal em Redes de Petri para Verificao de Simulaes

Trabalho de Concluso de Curso

Engenharia da Computao

Renata Wanderley Medeiros Orientador: Prof. Dr. Ricardo Massa Ferreira Lima

Recife, junho de 2007

ESCOLA POLITCNICA

DE PERNAMBUCO

Este Projeto apresentado como requisito parcial para obteno do diploma de Bacharel em Engenharia da Computao pela Escola Politcnica de Pernambuco Universidade de Pernambuco.

Modelo Formal em Redes de Petri para Verificao de Simulaes

Trabalho de Concluso de Curso

Engenharia da Computao

Renata Wanderley Medeiros Orientador: Prof. Dr. Ricardo Massa Ferreira Lima

Recife, junho de 2007

ESCOLA POLITCNICA

DE PERNAMBUCO

Renata Wanderley Medeiros

Modelo Formal em Redes de Petri para Verificao de Simulaes

i

ESCOLA POLITCNICA

DE PERNAMBUCO

Resumo

Este trabalho trata de simuladores, gerados pelo MPhyScaS (Multi Physics and Multi Scale

Solver Environment), que envolve a simulaes de fenmenos multifsicos acoplados. Estes so

fenmenos que transformam a matria, mas no alteram sua composio qumica. Neste

contexto, a simulao de um problema real pode ser bastante complexa. Desta forma, os

simuladores devem auxiliar o usurio a fazer verificaes sobre os elementos inseridos e valid-

los antes de iniciar a simulao. Este trabalho prope uma representao das relaes entres os

dados de entrada dos simuladores gerados pelo MPhyScaS, bem como um modelo formal,

utilizando a tcnica de redes de Petri, baseado na representao definida. Este modelo justificar

o prosseguimento para a fase de simulao, removendo erros que podem ocorrer durante esta

fase.

ii

ESCOLA POLITCNICA

DE PERNAMBUCO

Abstract

This work is about simulators, generated by MPhyScaS (Multi Physics and Multi Scale Solver

Environment), that involve the simulation of coupled multiphysics phenomena. These are

phenomena that transform the material, but they dont modify its chemical composition. In this

context, the simulation of a real problem may be very complex. In this way, simulators must help

users making verifications on inserted elements and validating them before starting simulation.

This work proposes a representation to the relations of entry data for MPhyScaS simulators, in

addition to a formal model, using the Petri nets technique, based on defined representation. This

model will justify the passage to simulation phase, removing mistakes that may occur.

iii

ESCOLA POLITCNICA

DE PERNAMBUCO

Sumrio

ndice de Figuras iv

Tabela de Smbolos e Siglas v

1 Introduo 7 1.1 MPhyScaS 8 1.2 Viso Geral da Monografia 9

2 Redes de Petri 11

3 Representao das Relaes entre os Dados de Entrada do Simulador 14

4 Especificao Formal 21 4.1 O modelo formal 21 4.2 Anlises sobre o Modelo 28

4.2.1 Dependncia entre Quantias 29 4.2.2 Quantia ativada ou fenmeno criado no utilizado 30 4.2.3 Bloco ou Grupo criado no utilizado 32 4.2.4 Estado de um Grupo no utilizado 33

5 Estudo de Caso 35 5.1 A Simulao 35 5.2 O Modelo Criado 37 5.3 As Anlises 41

6 Concluses e Trabalhos Futuros 42 6.1 Contribuies 42 6.2 Trabalhos Futuros 43

iv

ESCOLA POLITCNICA

DE PERNAMBUCO

ndice de Figuras

Figura 1-1 Organizao do ambiente MPhyScaS. 9 Figura 2-1 Elementos das redes de Petri. 11 Figura 2-2 Exemplo de rede de Petri. 12 Figura 2-3 Representao de arco valorado. 12 Figura 2-4 Exemplo de disparo de uma transio. 13 Figura 3-1 Relao entre Kernel, Bloco, Grupo e Fenmeno. 15 Figura 3-2 Representao das relaes entre os dados de entrada. 16 Figura 3-3 Representao com as relaes de Kernel possui Blocos e Bloco possui Grupos. 17 Figura 3-4 Representao com as relaes de Grupo possui Fenmenos, GroupTasks e gerencia Estados. 18 Figura 3-5 Representao com as relaes de Quantia contribui para um Estado e GroupTasks solicita ao Fenmeno o clculo de uma Quantia. 19 Figura 3-6 Representao com as relaes de acoplamento. 20 Figura 4-1 Exemplo de especificao para Kernel, Bloco e Grupo e suas relaes. 22 Figura 4-2 Exemplo de especificao para Fenmenos e GroupTasks, e suas relaes com os Grupos. 23 Figura 4-3 Exemplo de especificao para Quantias e Estados, suas relaes entre si e com os Fenmenos. 24 Figura 4-4 Exemplo de especificao quando uma Quantia contribui para mais de um Estado. 25 Figura 4-5 Exemplo de especificao quando acontece acoplamento. 25 Figura 4-6 Exemplo de especificao para o relacionamento entre Grupo e Estado. 26 Figura 4-7 Exemplo de especificao para solicitao do clculo de uma Quantia pelo GroupTask. 27 Figura 4-8 Exemplo de um modelo completo. 28 Figura 4-9 Exemplo de rede de Petri com os Estados que auxiliaro as anlises. 29 Figura 4-10 Exemplo de dependncia entre Quantias. 30 Figura 4-11 Estado inicial para a anlise que verifica se existe Quantia ativa ou Fenmeno criado que no utilizado. 31 Figura 4-12 Rede de Petri durante a anlise, destacando as transies habilitadas. 32 Figura 4-13 Estado inicial da rede de Petri para a anlise que verifica se h algum grupo ou bloco criado que no utilizado. 33 Figura 4-14 Estado inicial da rede de Petri para a anlise que verifica se algum Estado criado no utilizado, destacando as transies que podero disparar quando o token chegar ao Grupo1. 34 Figura 5-1 Geometria do problema. 36 Figura 5-2 Resultado da simulao quando a concentrao do soluto varia no tempo. 37 Figura 5-3 Resultado da simulao quando a concentrao do soluto varia no tempo e no espao. 37 Figura 5-4 Parte do modelo que possui as relaes entre Kernel, Bloco, Grupo e Fenmeno. 38 Figura 5-5 Parte I do modelo que possui as relaes entre Fenmeno, Quantia e Estado. 38 Figura 5-6 Parte II do modelo que possui as relaes entre Fenmeno, Quantia e Estado. 39 Figura 5-7 Parte III do modelo que possui as relaes entre Fenmeno, Quantia e Estado. 39 Figura 5-8 Parte I do modelo que possui as relaes entre Grupo, GroupTask e Quantia. 40 Figura 5-9 Parte II do modelo que possui as relaes entre Grupo, GroupTask e Quantia. 40 Figura 5-10 Parte III do modelo que possui as relaes entre Grupo, GroupTask e Quantia. 40

v

ESCOLA POLITCNICA

DE PERNAMBUCO

Tabela de Smbolos e Siglas

MPhyScaS Multi Physics and Multi Scale Solver Environment. A.D.R. - Applied Data Research Inc. FEM - Finite Element Method. INA Integrated Net Analyzer. CRA Corrosion Resistant Alloys.

vi

ESCOLA POLITCNICA

DE PERNAMBUCO

Agradecimentos

Antes de tudo a Deus, com quem falo diariamente e, apesar de no obter respostas, sinto-o do meu lado, como fora, luz e amor.

Ao meu pai Olavio, minha me Ione, minha tia Orqudia, minha irm Roberta e meu cunhado Adriano, presena constantes em meu cotidiano, pela alegria, compreenso, estmulo e ajuda que me deram, permitindo-me concretizar esta tarefa que expressa um instante singular de minha vida.

Ao meu namorado William, por ter estado ao meu lado durante esta trajetria fazendo as figuras dessa monografia e me dando apoio e carinho sempre que precisei. E a seus familiares, pelo carinho e compreenso recebidos de cada um.

Aos meus amigos Tssia e Fernando, e aos outros queridos amigos e colegas, pelo companheirismo e esprito de luta, pois no sei, sinceramente, se, sem eles, teria terminado este trabalho.

Por fim, ao professor Ricardo Massa que, com eficcia de seus ensinamentos, contribui, de modo objetivo, para a minha formao. E, como no posso esquecer de ningum, a todos os outros que contriburam, direta ou indiretamente, para que este trabalho fosse finalizado.

7

ESCOLA POLITCNICA

DE PERNAMBUCO

1

Introduo

Em problemas do mundo real, desenvolver sistemas e a partir deles auferir informaes quantitativas e qualitativas sobre suas caractersticas pode acarretar em custos e riscos excessivos. Construir e implementar um modelo de simulao, por sua vez, uma alternativa que pode economizar recursos financeiros e de tempo, bem como minimizar o acontecimento de riscos. De posse desse modelo implementado, poder ser possvel realizar simulaes prximas ou equivalentes s funcionalidades do sistema real. Desta forma, a construo do sistema pode ser realizada ao final, tomando como base as informaes que forem extradas dessas simulaes.

Desenvolver e implementar um simulador uma tarefa complexa. Os simuladores, para serem eficientes, devem ser capazes de acompanhar o crescimento da complexidade dos sistemas a serem simulados. O MphyScaS (Multi Physics and Multi Scale Solver Environment) prope uma metodologia para dar assistncia construo automatizada de simuladores que envolvem fenmenos fsicos. Estes so fenmenos que transformam a matria, mas no alteram sua composio qumica.

Como os simuladores gerados pelo MPhyScaS analisam problemas reais, uma simulao que envolva vrios fenmenos que interagem durante sua evoluo pode ser bastante custosa, levando horas ou dias para ser realizada. Isto acontece porque h uma forte dependncia e compartilhamento de dados nas leis de comportamento nos quais os fenmenos so definidos [1]. Por isso, extremamente importante, para o usurio do simulador, verificar e validar se os dados inseridos esto corretos, ou seja, verificar sua simulao antes de inici-la.

Uma forma de facilitar o entendimento do funcionamento e comportamento, dos dados inseridos no simulador pelo usurio, criar um modelo formal. Este modelo deve justificar o prosseguimento para a fase de simulao, removendo erros que podem ocorrer durante esta fase.

Antes que esse modelo seja definido, necessrio que uma representao para as relaes entre os dados inseridos no simulador pelo usurio seja criada. Ela deve representar fielmente a estrutura e organizao dos dados de entrada do simulador e relaes existentes, constituindo uma abstrao do sistema [2]. esta representao que guiar a criao do modelo, que permitir responder questes prvias sobre a simulao.

Esta monografia define uma proposta de uma representao das relaes entre os dados inseridos no simulador. Define tambm um modelo formal, utilizando a tcnica de redes de Petri, baseado na representao definida. Este modelo permitir que verificaes quanto corretude dos dados sejam feitas, informando ao usurio seus resultados para que possam ser validados antes de iniciar a simulao.

Captulo

8

ESCOLA POLITCNICA

DE PERNAMBUCO

1.1 MPhyScaS Simulao um mtodo bastante relevante para resolver vrios problemas. usada para estudar o comportamento e reaes de um determinado sistema atravs de modelos que imitam, na totalidade ou em partes, propriedades e comportamentos desse sistema, permitindo sua manipulao e estudo detalhado [3].

Quando o desenvolvimento e implementao de um sistema real completamente invivel, devido a incertezas quanto aos custos e riscos que o sistema poderia causar, esta tcnica pode ser aplicada. Sistemas como a manuteno de dutos de cargas qumicas podem levar a perda de vidas se feitas de maneira inadequada, ou mesmo se no forem feitas em tempo estimado. Para este sistema, necessrio verificar a evoluo do desgaste do material no tempo, a fim de que danos no venham a ocorrer. Clculos como este so muito complexos, pois envolvem muitos fenmenos fsicos atuando em uma geometria contnua [4], tornando este um importante problema computacional. Isto se deve ao fato de haver uma forte dependncia e compartilhamento de dados nas leis de comportamento onde os fenmenos fsicos so definidos.

O projeto e implementao de simuladores para Fenmenos fsicos um problema computacionalmente impraticvel se no houver poderosas ferramentas para auxlio [5]. A utilizao de tcnicas de reuso [6] e a utilizao de componentes de software [7] tornariam o desenvolvimento desses simuladores mais eficiente.

O MPhyScaS (Multi Physics and Multi Scale Solver Environment) uma proposta de ambiente que d assistncia construo automatizada de simuladores multi-fsicos. Para resolver problemas desta natureza, ele se baseia no Mtodo do Elemento Finito (FEM Finite Element Method [8]). uma extenso do trabalho proposto por Cruz [9]. Os simuladores criados pelo MPhyScaS podero ser de vrias classes, sendo estipulado pelo engenheiro especialista no assunto, e no somente de uma nica espcie.

O MPhyScaS composto por trs sistemas distintos: i. Gerador/Configurador de Simuladores: responsvel por integrar os

componentes de software ao ncleo do simulador a fim de produzir simuladores especficos para propsitos diferentes, alm de gerenciar os componentes de software que fazem parte de um simulador existente;

ii. Simulador: produto gerado pelo Gerador/Configurador de Simuladores, responsvel por fazer simulaes utilizando os componentes de software disponveis.

iii. Sistema de Gerenciamento de Componentes: funciona como um banco de dados e responsvel por armazenar e gerenciar componentes de software, diferenciando suas utilidades e verificando a corretude de cada um deles.

A Figura 1-1 ilustra a organizao desses sistemas. Existem dois tipos de usurios para o sistema: (i) um especialista, que utiliza o

Gerador/Configurador de Simuladores para gerar um simulador especfico solicitado por um usurio; (ii) um usurio, que faz diversas simulaes, no simulador solicitado e criado pelo especialista, podendo configurar algumas partes desse simulador a partir de componentes disponveis.

O MPhyScaS construdo sobre uma linguagem de padres, permitindo assim a utilizao de diversos componentes de software [5], ou seja, se esse componentes forem construdos seguindo os padres definidos, eles so capazes de serem reconhecidos e utilizados tanto pelo Gerador/Configurador de Simuladores como pelo Simulador.

O Mphyscas possui um conjunto de abstraes, que so capazes de representar os Fenmenos e suas interaes (dependncia e compartilhamento de dados) e os algoritmos de soluo empregados pelo Simulador (clculo de Quantias e soluo de problemas auxiliares).

9

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 1-1 Organizao do ambiente MPhyScaS.

Para facilitar o entendimento sobre Quantias, ser feito uma analogia entre um Simulador e um sistema de equaes. Se estes fossem equivalentes, um Fenmeno seria equivalente a uma equao do sistema, e uma Quantia, a uma varivel de uma equao. O clculo de uma Quantia seria o mesmo que achar o valor da varivel, mas poderia ser necessrio que o valor de outra varivel j tivesse sido encontrado, o que representa o acoplamento entre Fenmenos.

1.2 Viso Geral da Monografia O Captulo 2 apresenta a conceituao de redes de Petri, tcnica que foi utilizada para criar

o modelo formal para verificaes dos dados de entrada. Identifica seus elementos, suas propriedades, limitaes e extenses existentes.

O Captulo 3 contextualiza o sistema MPhyScaS, ressaltando sua importncia, os sistemas que o compem e seus modos de utilizao. O captulo apresenta tambm a arquitetura de software criada para representar as interaes entre os dados de entrada do simulador.

O Captulo 4 explica como o modelo formal foi definido, detalhando como o mesmo deve ser criado de acordo com os dados de entrada do simulador inseridos pelo usurio. Define como cada componente deve ser especificado e como suas relaes devem ser modeladas para que seja possvel fazer as anlises que daro informaes sobre os dados. Mostra ainda como as anlises devem ser feitas no modelo em redes de Petri e como devem ser interpretados os resultados obtidos para fornecer informaes essenciais ao usurio.

10

ESCOLA POLITCNICA

DE PERNAMBUCO

O Captulo 5 exemplifica a utilizao deste trabalho em um estudo de caso realizado em um simulador real para simular a difuso de hidrognio em dutos de petrleo.

O Captulo 6 conclui o trabalho, ressaltando as contribuies obtidas, e identifica trabalhos futuros que contribuiro para extenso deste trabalho em outras partes do MPhyScaS.

11

ESCOLA POLITCNICA

DE PERNAMBUCO

2

Redes de Petri

As redes de Petri foram criadas a partir da tese de doutorado de Carl Adam Petri, intitulada Kommunication mit Automaten (Comunicao com Autmatos), apresentada, em 1962, faculdade de Matemtica e Fsica de Darmstadt na ento Alemanha Ocidental.

As primeiras aplicaes de redes de Petri aconteceram em 1968, no projeto norte-americano Information System Theory, da A.D.R. (Applied Data Research Inc.). Muito da teoria inicial, da notao e da representao de redes de Petri foram desenvolvidas nesse projeto e publicadas em seu relatrio final. Esse trabalho ressaltou como as redes de Petri poderiam ser aplicadas na anlise e na modelagem de sistemas com componentes concorrentes [10].

Redes de Petri uma tcnica de especificao formal bem estabelecida, largamente difundida e adequada para a modelagem de sistemas que tenham atividades paralelas, concorrentes, assncronas e no-determinsticas [11]. Hoje, possvel verificar sua abrangncia e aplicabilidade em diversas reas, tais como: na cincia da computao, engenharias eletrnica e qumica, administrao de empresas. A tcnica tem sido mais explorada para especificao de sistemas de hardware ou software, avaliao de desempenho, especificao de protocolos de comunicao, diagnstico de falhas e no projeto de software/hardware. Isto ocorre devido ao conjunto de elementos que possui ser capaz de descrever partes de sistemas com caractersticas de concorrncia, controle, conflito, sincronizao e compartilhamento [12].

A representao grfica das redes de Petri tem sido muito til por permitir a visualizao dos processos e a comunicao entre eles. As redes de Petri so compostas por dois elementos: um passivo denominado de lugar; e um ativo denominado de transio. Os lugares representam uma condio, uma atividade ou um recurso e so representados graficamente por crculos. As transies representam um evento (ao) realizado pelo sistema; graficamente, so representados por um trao ou uma barra. A Figura 2-1 mostra a representao grfica dos elementos das redes de Petri.

Figura 2-1 Elementos das redes de Petri.

Captulo

12

ESCOLA POLITCNICA

DE PERNAMBUCO

Esses dois elementos so os vrtices do grafo associado s redes de Petri. Os vrtices so interligados por arcos dirigidos, como pode ser visto na Figura 2-2. Os arcos que interligam lugares s transies correspondem relao entre as condies verdadeiras, que em um dado momento, possibilitam a execuo das aes, enquanto os arcos que interligam transies aos lugares representam a relao entre as aes e as condies que se tornam verdadeiras com a execuo das aes. Desta forma, uma rede de Petri um grafo direcionado com dois tipos de ns, no havendo arcos entre ns do mesmo tipo [13].

Figura 2-2 Exemplo de rede de Petri.

Os lugares podem armazenar marcas ou tokens, representados graficamente por pontos pretos. Uma distribuio de tokens na rede chamada de marcao e corresponde ao Estado da rede de Petri. Alm dos tokens, ainda possvel que os vrtices de um grafo sejam interligados por mltiplos arcos. A Figura 2-3 ilustra um exemplo, com que um lugar pode ser conectado a uma transio atravs de diversos arcos ou vice-versa. Por convenincia, os mltiplos arcos so substitudos por um nico arco valorado, onde o numeral associado ao arco corresponde ao nmero de arcos que interligam os vrtices.

Figura 2-3 Representao de arco valorado.

13

ESCOLA POLITCNICA

DE PERNAMBUCO

Pode-se dizer que uma transio est habilitada se todos os lugares de entrada, ou seja, lugares de onde partem arcos em direo a esta transio tm ao menos o nmero de tokens igual ou maior que o nmero de arcos que ligam o lugar a esta transio. Uma transio habilitada pode disparar e seu disparo, ou realizao de uma ao, est associado a algumas pr-condies, ou seja, existe uma relao entre os lugares e as transies, que possibilita a realizao de uma ao. De forma semelhante, aps a realizao de uma ao, alguns lugares tero suas informaes alteradas (ps-condies). A Figura 2-4(a) mostra uma rede de Petri com uma transio disponvel, que, quando disparada, causa mudanas na marcao, deixando-a como a Figura 2-4(b).

Figura 2-4 Exemplo de disparo de uma transio.

O Estado de uma rede, em um determinado instante, representado pela quantidade de tokens em cada lugar da rede de Petri. O Estado da rede alterado quando ocorre ao menos um disparo. Como exemplo dessa representao, tem-se que o Estado da rede da Figura 2-4(a) M(1, 2, 0), que representa a quantidade de tokens dos lugares p0, p1 e p2, respectivamente. Ao acontecer o disparo da transio t0, esse Estado alterado para M(0, 0, 3), que o Estado da Figura 2-4(b).

Desde o trabalho original de Carl Adam Petri tm surgido diversas variantes ao seu modelo de redes de Petri. Pode-se afirmar que a maior parte destas variantes nasceu da necessidade de adaptao especificidade da aplicao para as quais a sua utilizao era desejada. O modelo original das redes de Petri falha na representao de duas importantes caractersticas: aspectos funcionais complexos, tais como: condies que determinam o fluxo de controle, e os aspectos de temporizao [11]. Para enfrentar essas limitaes, extenses das redes de Petri foram desenvolvidas. Alguns exemplos delas so: as Redes de Petri Temporizadas [14], as Redes e Petri Coloridas [15], as Redes de Petri Estocsticas [16], as Redes de Petri Estocsticas Generalizadas [17].

14

ESCOLA POLITCNICA

DE PERNAMBUCO

3

Representao das Relaes entre os Dados de Entrada do Simulador

Criar um modelo que represente as relaes entre os dados inseridos no simulador guiar a definio do modelo formal. Este modelo importante, pois:

i. facilita a comunicao entre as partes interessadas no projeto, pois oferece uma representao com alto nvel de abstrao;

ii. permite tomada de decises antes de comear a implementao da criao do modelo formal e das anlises;

iii. possibilita que partes dessa representao sejam reutilizadas para outro sistema.

Estas razes influenciam diretamente na antecipao de decises em relao a estratgias utilizadas para o desenvolvimento do projeto. Isto acontece porque a tomada dessas decises um processo que requer experincia de quem o faz. Essas decises podem, se inadequadas, impossibilitar o projeto devido a gastos excessivos e ao tempo perdido para corrigir o que foi feito. Com a representao feita, essas decises podem ser tomadas de forma mais segura.

Para isto, a representao deve identificar os componentes e suas interaes. Alm disso, deve ser possvel entender os requisitos do sistema, a fim de que desenvolvedores e testadores entendam o trabalho que lhes foi atribudo e o gestor, as implicaes do planejamento estratgico. Os desenvolvedores devem se restringir s estruturas definidas na representao e os arquitetos devem supervisionar e verificar a adequao desse modelo, registrando impactos, riscos e dificuldades. As informaes obtidas com esse registro contribuem para a evoluo do modelo [1].

Para o melhor entendimento das dependncias entre os componentes Kernel, Bloco, Grupo e Fenmenos, que esto presentes na representao criada para o MPhyScaS, a Figura 3-1 representa a relao entre esses componentes, onde o de maior nvel possui componentes do nvel imediatamente inferior. Os nveis esto representados, na Figura 3-1, de forma que o componente mais acima da figura o de maior nvel.

Captulo

15

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-1 Relao entre Kernel, Bloco, Grupo e Fenmeno. O Kernel, componente de maior nvel na Figura 3-1, nico, pois representa o programa

principal, que inicia a execuo do simulador e o controla, verificando o seu trmino. Ele possui um ou mais Blocos, que por sua vez, cada um deles possui um ou mais Grupos. Cada Grupo possui um ou mais Fenmenos. No faz sentido haver um componente de um nvel se este no pertencer a um componente do nvel imediatamente superior. Como exemplo disso, tem-se que no faz sentido haver um Fenmeno que no pertena a um Grupo.

A Figura 3-2 mostra a representao das relaes dos dados inseridos no simulador do MPhyScaS, um dos objetivos deste trabalho. Nela esto representados seus componentes (Kernel, Bloco, Grupo, Fenmeno, Quantia, Estado, GroupTask tarefa do Grupo), suas interaes e dependncias.

16

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-2 Representao das relaes entre os dados de entrada. As relaes que indicam que o Kernel possui Blocos e cada Bloco possui Grupos j foram

mencionadas. Estas relaes esto presentes na arquitetura de software e podem ser identificadas mais facilmente na Figura 3-3, que destaca as relaes mencionadas.

17

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-3 Representao com as relaes de Kernel possui Blocos e Bloco possui Grupos. Os Estados so estruturas de dados, como matriz, vetor ou escalar, onde sero armazenados

os resultados obtidos nos clculos das Quantias. Uma Quantia pode contribuir com valores em mais de uma estrutura, ou seja, uma Quantia pode contribuir com mais de um Estado. Os GroupTasks so tarefas que sero executadas pelo Grupo. Uma tarefa do Grupo responsvel por solicitar a um Fenmeno desse Grupo que calcule uma de suas Quantias.

Como dito anteriormente, o Kernel representa o programa principal, que inicia a execuo do simulador e o controla, verificando o seu trmino. O Bloco est associado a um algoritmo de resoluo, o que significa que cada Bloco seguir esse algoritmo para resolver questes sobre os seus Grupos. O Grupo responsvel por gerenciar seus Fenmenos, Estados e GroupTasks. As relaes que indicam que um Grupo possui Fenmenos, GroupTasks e responsvel por gerenciar um conjunto de Estados esto destacadas na Figura 3-4.

18

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-4 Representao com as relaes de Grupo possui Fenmenos, GroupTasks e gerencia Estados.

Cada Fenmeno possui um conjunto de Quantias que podem ser calculadas por ele.

Calcular uma Quantia significa contribuir para o preenchimento, total ou parcial, de um Estado (matrizes, vetores ou escalares). Os GroupTasks solicitam aos Fenmenos que calculem uma determinada Quantia pertencente ao Fenmeno. Estas relaes so destacadas na representao mostrada na Figura 3-5.

19

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-5 Representao com as relaes de Quantia contribui para um Estado e GroupTasks solicita ao Fenmeno o clculo de uma Quantia.

Para uma Quantia ser calculada, a mesma pode precisar de dados produzidos por outros

Fenmenos, chamado de Fenmenos Acoplados. Quando h acoplamento entre Fenmenos, o GroupTask, ao solicitar o clculo de uma Quantia a um Fenmeno, j o informa que outros Fenmenos so acoplados a ele e estes sero necessrios para o clculo. A Figura 3-6 destaca as relaes referentes aos acoplamentos entre Fenmenos.

20

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 3-6 Representao com as relaes de acoplamento. Esta representao da arquitetura, em diagrama de classes, um primeiro passo para a

correta definio de uma arquitetura em redes de Petri para o ambiente MphyScaS.

21

ESCOLA POLITCNICA

DE PERNAMBUCO

4

Especificao Formal

O rpido avano tecnolgico requer, cada vez mais, formas mais rpidas e confiveis de desenvolver sistemas de software a fim de atender aos requisitos de usurios e sistema. , portanto, essencial a esses desenvolvedores utilizar tcnicas de especificao formal que ofeream suporte a corretude, completude, consistncia, conciso e clareza [18].

ainda de suma importncia que a tcnica de especificao formal possua um conjunto de conceitos bem definidos e base matemtica de modo a permitir a construo e uso de ferramentas computacionais para analisar e simular especificaes, bem como verificar a conformidade de implementaes com as respectivas especificaes.

Um dos principais desafios deparados o de assegurar a confiabilidade de sistemas projetados. Este objetivo torna-se ainda mais evidente quando o software empregado em sistemas cuja falha operacional pode ocasionar perdas humanas, econmicas ou causar degradao na prestao de servios.

Como os simuladores gerados pelo MPhyScaS analisam problemas reais, com diversos Fenmenos atuando sobre uma geometria contnua, esse processo de simulao pode ser bastante custoso, levando horas ou dias para ser realizado [1]. Por isto, extremamente importante, para o usurio do simulador, verificar e validar se os dados inseridos esto corretos. O modelo proposto neste captulo representa esses dados, permitindo que anlises sejam feitas a fim de auxiliar o usurio nesta tarefa.

4.1 O modelo formal O modelo formal para o problema apresentado deve garantir um nvel de abstrao dos dados de entrada do simulador que permitam que dvidas possam ser respondidas por anlises feitas sobre o modelo. Isto ajudar a validar os dados de entrada atravs de simulaes, detectando inconsistncias e ambigidades, quando houver.

Ao terminar de inserir os dados de entrada, o usurio solicitar o incio da simulao, mas antes que a simulao seja iniciada o simulador criar o modelo formal proposto e far todas as anlises definidas. Se nessas anlises no for encontrado nenhum erro, o simulador permitir que a simulao seja iniciada; caso contrrio, o simulador informar ao usurio sobre os erros encontrados. O modelo criado totalmente abstrato para o usurio, ou seja, ele no sabe de sua existncia, muito menos como criado e como so feitas as anlises.

Captulo

22

ESCOLA POLITCNICA

DE PERNAMBUCO

A tcnica de redes de Petri ser utilizada para a criao do modelo. O componente do Kernel ser representado por um lugar da rede de Petri. Cada Bloco criado tambm ser representado por um lugar da rede de Petri. Seguindo a metodologia, cada Grupo criado ser representado por um lugar. A Figura 4-1 mostra um exemplo dessa representao.

As relaes entre Kernel e Bloco, e Bloco e Grupo so representadas por uma transio que liga os componentes. Cada relao deve ser representada por uma transio, como podem ser identificadas na Figura 4-1. Um Bloco no deve estar relacionado com mais de um Grupo atravs da mesma transio. Isto no pode acontecer porque posteriormente ser preciso analisar se existe possibilidade de chegar um token a um determinado Grupo, e para isto seria necessrio fazer vrias verificaes. Esta anlise exige uma marcao inicial que possui apenas um token no lugar que representa o Kernel.

Para ilustrar utilizando o exemplo da Figura 4-1, deseja-se analisar se o Grupo0 est relacionado a algum Bloco pertencente ao Kernel. Para isto, precisa-se saber se o Estado M(0, 0, 0, 1, 0, 0, 0, 0) da rede pode ser alcanado. Este Estado significa a quantidade de tokens dos lugares Kernel, Bloco0, Bloco1, Grupo0, Grupo1, Grupo2, Grupo3 e Grupo4, respectivamente. Se os Blocos fossem relacionados aos Grupos por uma nica transio, seria necessrio verificar todas as combinaes de Estados, tendo que a quantidade de tokens do Grupo0 seria constante e igual a 1. Ou seja, seria necessrio verificar se os Estados M(0, 0, 0, 1, 1, 1, 1, 1), M(0, 0, 0, 1, 0, 1, 0, 1) ou alguma das demais possveis combinaes, com o quarto nmero igual a 1 (nmero de tokens que deve haver no Grupo0), pode ser alcanado. Por este motivo, o modelo melhor representado com uma transio para cada relao existente. Este mesmo motivo serve para as transies que ligam o Kernel aos Blocos.

Figura 4-1 Exemplo de especificao para Kernel, Bloco e Grupo e suas relaes. Como visto no captulo anterior, os Grupos possuem Fenmenos, GroupTasks e gerenciam

Estados. Os Estados sero explicados posteriormente. Cada componente desses (GroupTask e Fenmeno) ser representado por um lugar na rede de Petri. As relaes entre Grupo e GroupTask, e Grupo e Fenmeno seguem a metodologia e so representados, cada uma, por uma

23

ESCOLA POLITCNICA

DE PERNAMBUCO

transio, devido ao mesmo motivo j explicado. A Figura 4-2 exemplifica uma rede de Petri, que parte do modelo, que apresenta esses componentes e relaes.

Figura 4-2 Exemplo de especificao para Fenmenos e GroupTasks, e suas relaes com os Grupos.

Note que, na Figura 4-2, o Grupo0 possui o Fen0 e Fen1 e o Grupo1 tambm possui

Fenmenos com os mesmos identificadores, mas isso no quer dizer que esses Fenmenos so os mesmos. Cada Grupo gerencia os identificadores de seus Fenmenos, o que significa que o Fen0 do Grupo0 no o mesmo que o Fen0 do Grupo1. O mesmo acontece para os outros Fenmenos e para os GroupTasks de Grupos diferente.

Seguindo a metodologia para a criao do modelo, as Quantias e os Estados tambm so representados por um lugar na rede de Petri, como pode ser visto na Figura 4-3. As relaes entre os Fenmenos e as Quantias, e as Quantias e os Estados so representadas por transies que ligam os componentes. Pelo motivo j explicado anteriormente, cada relao deve ser representada por uma transio. A Figura 4-3 ilustra um exemplo de rede de Petri, que parte do modelo, com esses componentes e relaes.

24

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-3 Exemplo de especificao para Quantias e Estados, suas relaes entre si e com os Fenmenos.

possvel notar, na Figura 4-3, que Quantias de Fenmenos diferentes tambm podem

possuir mesmo identificador, isto tambm implica em serem Quantias diferentes. Quanto aos Estados, isto no pode acontecer, mesmo sendo gerenciados por Grupos diferentes, pois as Quantias podem ser acopladas a Estados que precisam de identificao nica para no serem confundidos.

Uma Quantia pode contribuir, total ou parcialmente, para mais de um Estado. Quando isso ocorre, o relacionamento entre a Quantia e os Estados aos quais ela contribui deve ser feito atravs de apenas uma transio. A Figura 4-4, que tambm parte do modelo formal a ser criado, ilustra esse tipo de relacionamento.

Esta representao deve ser feita apenas por uma transio porque, obrigatoriamente, a Quantia contribui com os dois Estados em uma mesma ocasio. Como exemplo disso, suponha que o Estado da rede da Figura 4-4 fosse M(1, 0, 0, 0), sendo esse Estado a quantidade de tokens dos lugares q1, q2, S1 e S2, respectivamente. O Estado M(0, 0, 1, 0) da rede no deve ser alcanado, pois representaria a contribuio da Quantia q1 apenas para o Estado S1. Se a representao desse tipo de relao fosse como a que acontece entre Blocos e Grupos, com uma transio para cada relao, esse Estado poderia ser alcanado. Desta forma, o modelo no representaria os dados corretamente.

25

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-4 Exemplo de especificao quando uma Quantia contribui para mais de um Estado. Quando ocorre um acoplamento entre Fenmenos, isto significa dizer que uma Quantia

necessitar de um Estado, produzido por outra Quantia, para contribuir com outro Estado. Este tipo de relacionamento deve ser representado apenas por um arco que ligue o Estado necessitado pela Quantia transio entre a Quantia e o Estado ao qual ela contribui. Isto exemplificado na Figura 4-5, que mostra o acoplamento entre o Fen0 e o Fen1, pois uma Quantia do Fen0 necessita de um Estado produzido por uma Quantia do Fen1 para ser calculada.

A representao desse tipo de relao feita apenas por um arco pois, ainda utilizando o exemplo da Figura 4-5, para o Estado S0 ser produzido, alm de ter sido solicitado o clculo da qauntia q0, o Estado S1 j deve ter sido produzido. A ligao que o arco faz, do Estado S1 transio entre q0 e S0, suficiente para representar essa dependncia. Outras representaes poderiam ser feitas, mas esta foi considerada por esse trabalho como a mais simples delas.

Figura 4-5 Exemplo de especificao quando acontece acoplamento. Voltando ao relacionamento entre Grupo e Estado, tem-se que este tipo de relao deve ser

representada por uma transio, para cada relao, entre estes dois componentes. A Figura 4-6 mostra este tipo de relacionamento em um exemplo.

26

ESCOLA POLITCNICA

DE PERNAMBUCO

Como visto no captulo anterior, um GroupTask solicita a um Fenmeno o clculo de uma determinada Quantia. Por questes de representao, pois no possvel diferenciar arcos em redes de Petri, no sero criadas relaes diretas entre o GroupTask e o Fenmeno. Ser criado, ento, uma transio que ligar o GroupTask diretamente a Quantia cujo clculo foi solicitado, como pode ser visto na Figura 4-7.

Figura 4-6 Exemplo de especificao para o relacionamento entre Grupo e Estado.

27

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-7 Exemplo de especificao para solicitao do clculo de uma Quantia pelo GroupTask.

Para ilustrar como ficaria um modelo completo da especificao formal dos dados inseridos

no simulador pelo usurio, a Figura 4-8 mostra um exemplo de todas as representaes vistas neste captulo.

28

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-8 Exemplo de um modelo completo.

4.2 Anlises sobre o Modelo Antes de iniciar as anlises sobre o modelo, ser necessrio criar trs lugares na rede de Petri que serviro apenas para auxiliar tais anlises. Um lugar, representado por aux0 na Figura 4-9, ser ligado a todas as transies entre Grupo e GroupTask; um segundo lugar, representado por aux1 na Figura 4-9, ser ligado a todas as transies entre Grupo e Fenmeno; e o ltimo lugar, representado por aux2 na Figura 4-9, ser ligado a todas as transies entre Grupo e Estado.

Estes lugares esto ligados apenas aos componentes que pertencem ao Grupo, pois serviro para restringir anlises que sejam direcionadas a um tipo de componentes. A anlise da seo 4.2.2 um exemplo de anlise direcionada aos GroupTasks, pois deseja-se saber se h uma seqncia de disparos, passando por um GroupTask, que leve a uma Quantia.

29

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-9 Exemplo de rede de Petri com os Estados que auxiliaro as anlises.

4.2.1 Dependncia entre Quantias

Esta anlise tem o objetivo de verificar se uma Quantia q0 necessita de um Estado S1 para ser calculada, mas a Quantia q1 que produz esse Estado necessita do Estado S0 produzido pela por q0. Estes relacionamentos esto representados na Figura 4-10.

30

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-10 Exemplo de dependncia entre Quantias. Este tipo de relacionamento pode travar a simulao. Isto ocorre caso o simulador esteja

sendo executado em uma arquitetura paralela, porque o processo de clculo da Quantia q0 estar sendo executado por um processador e o clculo da Quantia q1 por outro processador. Para este caso, um processador esperar o outro terminar de processar para utilizar seus resultados e vice-versa, o que acarretar em uma pausa infinita (deadlock).

Se o simulador estiver sendo executado em uma arquitetura seqencial, importante que isso seja informado ao usurio para que ele possa, caso o tenha feito inadvertidamente, modificar antes de comear a simular. Se tiver feito com um propsito, uma Quantia escolhida pelo usurio ser calculada primeiro com base em um Estado com valores iniciais, atribudos explicitamente pelo usurio.

Para realizar esta anlise de forma automatizada, utilizando a ferramenta INA (Integrated Net Analyzer [19]), basta executar a anlise que verifica a existncia de deadlock. Caso exista, esta dependncia entre Quantias aconteceu; caso contrrio, no h dependncias deste tipo.

4.2.2 Quantia ativada ou fenmeno criado no utilizado

Esta anlise tem o objetivo de informar ao usurio se ele criou algum Fenmeno que nunca ser utilizado na simulao, ou ainda, se ele ativou uma Quantia de um Fenmeno e seu clculo no ser solicitado. Esta anlise importante porque pode indicar uma falha de configurao do simulador.

Para identificar isso na rede de Petri montada, necessrio verificar se h alguma Quantia cujo clculo no solicitado por algum GroupTask. Ao encontrar Quantias com essa caracterstica, deve-se verificar se elas so necessrias para calcular o Estado de algum Fenmeno, ou seja, se elas totalizam conjunto de Quantias de um Fenmeno. Se isto ocorrer, significa dizer que este Fenmeno foi criado e no utilizado durante a simulao.

Com a utilizao do INA possvel automatizar esta anlise, verificando se existe uma seqncia de disparos que gere uma marcao em uma Quantia, a partir de uma marcao inicial. Esta marcao inicial definida pela presena de um token no lugar que representa o Kernel e um token no lugar auxiliar ligado s transies entre Grupo e GroupTask, como est representado na Figura 4-11.

31

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-11 Estado inicial para a anlise que verifica se existe Quantia ativa ou Fenmeno criado que no utilizado.

Isto implicar em, quando um token chegar a um Grupo, este seja direcionado apenas aos

GroupTasks, mostrando caminhos possveis apenas se passar por um deles. A Figura 4-12 mostra o estado da rede neste momento e destaca as transies habilitadas para disparo. Desta forma, possvel verificar que os caminhos encontrados devem passar por ao menos um GroupTask. Esta anlise deve ser realizada para todas as Quantias.

32

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-12 Rede de Petri durante a anlise, destacando as transies habilitadas.

4.2.3 Bloco ou Grupo criado no utilizado

Semelhante anlise anterior, esta anlise tem o objetivo de informar ao usurio se ele criou um Bloco ou Grupo que nunca ser utilizado na simulao. Esta situao identificada quando h Grupos que no esto associados a algum Bloco e se h Blocos que no esto associados ao Kernel. Caso seja encontrado um Bloco que no est associado ao Kernel, os Grupos que ele possui tambm no sero considerados na simulao.

Para a automatizao desta anlise com a ferramenta INA, utiliza-se a mesma estratgia da anlise anterior de verificar se existe uma seqncia de disparos que leve a aparecer um token a cada um dos Blocos e a cada um dos Grupos, a partir de uma marcao inicial. Esta marcao inicial seria apenas um token no lugar que representa o Kernel, pois no h necessidade de utilizar os lugares auxiliares. A Figura 4-13 mostra o estado inicial da rede para esta anlise, no havendo necessidade de utilizar os estados auxiliares, pois a anlise considera apenas a parte destacada da rede.

33

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 4-13 Estado inicial da rede de Petri para a anlise que verifica se h algum grupo ou bloco criado que no utilizado.

4.2.4 Estado de um Grupo no utilizado

Esta anlise tem o objetivo de verificar se um Estado de um Grupo foi criado e no ser utilizado pela simulao. O usurio deve ser informado quando isto acontecer, porque o Estado pode ser criado para ser utilizado como auxiliar. Neste caso, o Estado armazena os valores de outro Estado em um determinado instante de tempo a fim de ser utilizado posteriormente.

Para realizar esta anlise na ferramenta INA, verificado se existe uma seqncia de disparos que leve a aparecer um token a cada um dos Estados, a partir de uma marcao inicial. Esta marcao deve ser definida por um token no lugar que representa o Kernel e um token no lugar auxiliar ligado s transies entre Grupo e Fenmeno, porque deseja-se verificar se o Estado no produzido por alguma Quantia. Isto implicar em, quando um token chegar a um Grupo, este seja direcionado apenas aos Fenmenos, mostrando caminhos possveis apenas se

34

ESCOLA POLITCNICA

DE PERNAMBUCO

passar por um deles. A Figura 4-14 mostra o estado inicial da rede de Petri para esta anlise, destacando as transies que ficaro habilitadas quando o token chegar ao Grupo1.

Figura 4-14 Estado inicial da rede de Petri para a anlise que verifica se algum Estado criado no utilizado, destacando as transies que podero disparar quando o token chegar ao Grupo1.

35

ESCOLA POLITCNICA

DE PERNAMBUCO

5

Estudo de Caso

No comeo da produo de petrleo, os tubos de produo utilizados eram fabricados, em sua totalidade, com ao carbono. O petrleo deixa uma camada de resduos na parede dos tubos, que sofrem corroso [20]. No incio da extrao os poos de petrleo no apresentam corroso, mas, com o passar do tempo, estes poos tendem a produzir gua em quantidade e gradualmente retira os resduos de leo da parede dos tubos, e assim os poos com grande produo de gua tendem a ser altamente corrosivos.

Para evitar a corroso nos tubos de petrleo, as indstrias passaram a utilizar tubos de material do tipo Liga Resistente a Corroso (CRA Corrosion Resistant Alloys). O fator negativo deste material que possui um coeficiente de difuso baixo, possibilitando a ocorrncia de danos por hidrognio, como trincas durante o seu processo de fabricao ou durante seu uso.

O fenmeno de difuso consiste no movimento de partculas de uma rea de maior concentrao para uma rea de menos concentrao, buscando o equilbrio. No momento em que a concentrao de hidrognio aumenta na composio do ao e este hidrognio se aglomera em um ponto, ocorre trincas no material.

A ocorrncia de uma trinca durante o processo de fabricao algo custoso, mas possvel ser descoberto antes de colocar o tubo defeituoso para o uso. J a ocorrncia de um trincamento durante o uso pode ocasionar o rompimento do tubo antes da devida manuteno, j que estes tubos geralmente so subterrneos, e pode vir a causar enormes prejuzos financeiros e ao meio ambiente.

Para tentar prever o momento de realizar a manuteno em tubos de petrleo foi gerado um simulador nos moldes do MPhyScaS, para analisar o desgaste de tubos a ataques devido a presena de hidrognio. O simulador gerado resolve problemas de difuso acoplado com elasticidade.

5.1 A Simulao Para simular o problema de corroso nos tubos de petrleo necessrio inicialmente definir a geometria que sofrer a ao dos Fenmenos. A geometria do problema pode ser vista na Figura 5-1, onde R0 = 1.0 e R1 = 2.0. Tambm preciso que sejam informadas as condies de contorno para o problema. Desta forma, poder haver Quantias definidas no domnio, ou seja, na geometria, ou no contorno.

Captulo

36

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 5-1 Geometria do problema.

Com o objetivo tornar a simulao o mais real possvel, foram necessrios cinco

Fenmenos atuando sobre a geometria e/ou no contorno. Cada Fenmeno responsvel por resolver uma parte do sistema e, por isso, atuam de maneiras diferentes. Os Fenmenos utilizados so:

1. Deslocamento: possui Quantias que atuam no domnio e no contorno. responsvel por calcular a rigidez e a fora elstica sofrida pelo material. Tambm gerencia as condies de contorno.

2. Deformao: possui apenas uma Quantia que atua no domnio. Calcula a deformao sofrida pelo material.

3. Elasticidade: possui apenas uma Quantia que atua no domnio. Esta Quantia monta a matriz de elasticidade.

4. Tenso: possui apenas Quantias que atuam no domnio. responsvel por calcular as tenses nos elementos, definir o trao das tenses nodais e calcular essas tenses.

5. Difuso: possui Quantias que atuam no domnio e no contorno. responsvel por calcular o termo de fonte do soluto, que, para o problema estudado, o hidrognio, alm de gerenciar as condies do contorno.

Foram feitas duas simulaes para este problema. A primeira delas variou a concentrao do soluto (hidrognio) no tempo. A segunda simulao variou esta concentrao no tempo e no espao. Os resultados para as duas simulaes foram diferentes, como podem ser vistos nas Figura 5-2 e Figura 5-3, respectivamente.

37

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 5-2 Resultado da simulao quando a concentrao do soluto varia no tempo.

Figura 5-3 Resultado da simulao quando a concentrao do soluto varia no tempo e no espao.

possvel verificar, atravs da comparao da Figura 5-2 e da Figura 5-3, que o material

dos tubos de petrleo sofreu maior deformao na segunda simulao. A escala de cores mostra isso, pois uma escala aproximada da regio da geometria. Quanto mais profunda for essa deformao, maior a variao de cores, seguindo a variao da escala.

5.2 O Modelo Criado Para que fosse possvel fazer verificaes sobre os dados de entrada inseridos no simulador para estas simulaes, foi necessrio criar o modelo formal seguindo a metodologia vista nesta monografia. Os componentes e suas relaes foram fornecidos por um especialista na rea da simulao.

Como descrito na seo anterior, participaram da simulao cinco Fenmenos. Estes podem ser encontrados na Figura 5-4. Cada Fenmeno pertence a um Grupo diferente, tendo um total de cinco Grupos. Todos os Grupos pertencem ao mesmo Bloco, havendo apenas um relacionado ao Kernel. Essas relaes tambm podem ser identificadas na Figura 5-4.

38

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 5-4 Parte do modelo que possui as relaes entre Kernel, Bloco, Grupo e Fenmeno.

Cada Fenmenos possui uma quantidade de Quantias diferentes, cada uma delas tem uma

funcionalidade especfica. Cada Quantia contribui, total ou parcialmente, para algum Estado. A representao das Quantias e seus relacionamentos com os Fenmenos, bem como a representao dos Estados e seus relacionamentos com as Quantias esto representados nas Figura 5-5, Figura 5-6 e Figura 5-7.

Figura 5-5 Parte I do modelo que possui as relaes entre Fenmeno, Quantia e Estado.

39

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 5-6 Parte II do modelo que possui as relaes entre Fenmeno, Quantia e Estado.

Figura 5-7 Parte III do modelo que possui as relaes entre Fenmeno, Quantia e Estado. A representao dos GroupTasks definidos pelo especialista pode ser encontrada nas Figura

5-8, Figura 5-9 e Figura 5-10. Nela tambm possvel visualizar os relacionamentos entre GroupTasks e Quantias, que representam a relao de solicitao, por parte do GroupTask, a um Fenmeno o clculo de uma determinada Quantia.

40

ESCOLA POLITCNICA

DE PERNAMBUCO

Figura 5-8 Parte I do modelo que possui as relaes entre Grupo, GroupTask e Quantia.

Figura 5-9 Parte II do modelo que possui as relaes entre Grupo, GroupTask e Quantia.

Figura 5-10 Parte III do modelo que possui as relaes entre Grupo, GroupTask e Quantia.

Os modelos criados para as duas simulaes citadas so iguais. Isto aconteceu porque a

variao das simulaes se encontra na mudana de valores dos atributos dos Fenmenos. Algumas constantes da simulao tambm tiveram seus valores alterados para satisfazer condies especficas de cada uma delas.

41

ESCOLA POLITCNICA

DE PERNAMBUCO

Devido complexidade no entendimento da rede de Petri completa, foram apresentados apenas alguns componentes e relaes pertencentes aos dados inseridos no simulador pelo especialista. A rede de Petri completa pode ser encontrada no Apndice A.

5.3 As Anlises Quanto anlise de dependncia entre Quantias, foi encontrado que a Quantia q4 do Fenmeno Fen4 necessita do Estado S9 para contribuir com o Estado S8. A Quantia q1 do Fenmeno Fen4, por sua vez, necessita do Estado S8 para produzir o Estado S9. Isto ocasionaria uma dependncia mtua das Quantias.

No caso das simulaes realizadas, isso no ocasiona um erro e foi feito propositalmente. Isto aconteceu porque foi desejado que a Quantia q1 do Fenmeno Fen4 produzisse o Estado S9 com o valor do Estado S8. Este ltimo produzido pela contribuio de mais de uma Quantia, incluindo a Quantia q4.

Por serem simulaes complexas, o especialista no utilizou alguns elementos definidos como dados de entrada para estas simulaes. Com o auxilio do modelo esses elementos foram identificados facilmente, permitindo que o especialista alterasse os dados de entrada para que os elementos pudessem ser utilizados. A rede de Petri mostrada no Apndice A representa os dados de entrada aps as modificaes feitas pelo especialista.

Verificou-se ainda que no havia Quantia contribuindo para a produo do Estado S10, que necessrio para calcular o valor da Quantia q1. Consultando o especialista, identificou-se que este um Estado que, em seu algoritmo de simulao, empregado para guardar o valor de outro Estado. Desta maneira, o Estado S10 estaria sendo utilizado pelo simulador para representar um instante anterior de outro Estado do sistema.

Seria difcil, para o especialista, identificar esses casos sem a ajuda do modelo. Este proporcionou ao especialista verificar que haviam erros cometidos por ele mesmo, embora o prprio especialista no os tenha detectado.

42

ESCOLA POLITCNICA

DE PERNAMBUCO

6

Concluses e Trabalhos Futuros

Com o rpido avano da tecnologia, um importante desafio no desenvolvimento de sistemas assegurar a confiabilidade de sistemas projetados. Isto se torna mais evidente quando estes sistemas so custosos e podem acarretar grandes riscos, inclusive riscos vida humana, podendo levar morte.

Para resolver este problema, necessrio que esses sistemas sejam especificados formalmente por uma tcnica que d suporte a analisar questes como sua corretude, completude, consistncia, conciso e clareza [18].

O desenvolvimento deste trabalho resultou, principalmente, na definio de uma especificao formal em redes de Petri que representa, de forma abstrata, os dados de entrada para uma simulao. O modelo foi criado especificamente para os dados inseridos em simuladores criados pelo MPhyScaS.

Esta especificao importante, pois permite ao usurio verificar e validar sua simulao antes de inici-la, justificando o prosseguimento para a etapa de simulao e garantindo que erros no aconteam nesta fase.

6.1 Contribuies As principais contribuies apresentadas nesta monografia foram:

1. A definio de um modelo que busca representar, de forma fiel, a maioria dos componentes encontrados nos dados que podem ser inseridos como entrada para uma simulao, suas interaes e dependncias.

2. A criao de uma especificao formal que represente, de forma abstrata, os dados de entrada inseridos pelo usurio. O modelo e sua metodologia, para serem criados, foram baseados na arquitetura de software. Estes foram definidos de forma a facilitar as anlises que sero realizadas.

3. Foram definidas algumas anlises que podem ser feitas sobre o modelo a fim de dar informaes ao usurio sobre possveis erros nos dados inseridos por ele. Desta forma, o usurio pode verificar e validar esses dados.

Captulo

43

ESCOLA POLITCNICA

DE PERNAMBUCO

6.2 Trabalhos Futuros O modelo formal definido nesta monografia ainda no considera todos os componentes encontrados nos dados que podem ser inseridos como entrada dos simuladores criados pelo MPhyScaS. sugerido que, posteriormente, o modelo seja expandido de forma a tratar todos eles. Como exemplo desses componentes, podem ser citados a geometria, a malha geomtrica e operaes realizadas no algoritmo do Kernel e nos algoritmos de resoluo dos Blocos. Este ltimo componente evitaria que Estados auxiliares, como o encontrado no estudo de caso, pudessem ser confundidos com Estados no utilizados.

A proposio de outras anlises que envolvessem os componentes j definidos e componentes inseridos aps este trabalho devem ser realizadas. Isto permitir ao usurio fazer a verificao e validao dos dados quanto a outros tipos de erros.

A automatizao da criao de modelos seguindo a metodologia do Captulo 3 pode ser desenvolvida a fim de diminuir o tempo gasto para esta atividade.

Por fim, outras partes ou sistemas do MPhyScaS podem ser especificados formalmente com o objetivo de verificar a corretude e confiabilidade dos mesmos. Para isto, a arquitetura de software definida deve ser expandida, ou mesmo, outra arquitetura de software pode ser definida para esta parte ou sistema.

de suma importncia que, para um projeto complexo como o MPhyScaS, todo o sistema seja verificado e validado junto a todas as partes interessadas. Isto permitir uma melhor comunicao entre as partes, permitir que decises sejam tomadas antes de comear a implementao do sistema e aumenta o reuso de software.

44

ESCOLA POLITCNICA

DE PERNAMBUCO

Bibliografia

[1] WILKINS, Mark L. Computer Simulation of Dynamic Phenomena. First Edition. London: Springer, 1999.

[2] BASS, Len; CLEMENTS, Paul; KAZMAN, Rick. Software Architecture in Practice. Second Edition. Addison Wesley, 1998.

[3] O que Simulao. Disponvel em: . Acesso em: 16 de junho de 2007.

[4] SANTOS, F. C. G., BARBOSA, J. M. A., BRITO Jr., E. R. de, SILVA, J. M. B. Transfer and sharing of data between coupled multi-physics phenomena during simulations: the

Phenomenon Computational Pattern. In: World Conference on Computer Science International Conference on Modeling, Simulation & Visualization Methods, 2006, Las Vegas, pages 49-55.

[5] SANTOS, F. C. G., BARBOSA, J. M. A., BRITO Jr., E. R. de, SILVA, J. M. B. Dealing with Coupled Phenomena in the Finite Element Method. In: XXVII CILAMCE Iberian Latin American Congress of Computational Methods in Engineering, 2006, Blem.

[6] BOSCH, Jan. Software Reuse: Methods, Techniques, and Tools. In: 8th International Conference - ICSR, 2004, Madrid, Spain.

[7] HEINEMAN, George T., et al. Component-Based Software Engineering. In: 8th International Symposium CBSE, 2005, St. Louis, USA.

[8] LOGAN, Daryl L. A First Course in the Finite Element Method. Third Edition. Califrnia: Brooks/Cole, 2002.

[9] CRUZ, Maria L. P. M. Conceptualisation of an Environment for the Development os Simulators based on the Finite Element Method. 2004. 181 f. Tese de Doutorado em Cincia da Computao, Universidade Federal de Pernambuco, Pernambuco.

[10] HEUSER, C. A. Modelagem Conceitual de Sistemas: Redes de Petri. In: V EBAI, 1990. [11] MACIEL, Paulo R. M.; LINS, Rafael D.; CUNHA, Paulo R. F. Introduo s Redes de

Petri e Aplicaes. X Escola de Computao, Campinas SP, 1996. [12] PENHA, Dulcinia O. de; FREITAS, Henrique C. de; MARTINS, Carlos A. P. da S.

Modelagem de Sistemas Computacionais usando Redes de Petri: Aplicao em Projeto,

Anlise e Avaliao. In: Escola Regional de Informtica Rio de Janeiro Esprito Santo. 2004.

[13] DESEL, Jrg; ESPARZA, Javier. Free Choice Petri Nets. Pbk Version. Cambridge: Cambridge University Press, 2005.

[14] WANG, Jiacun. Timed Petri Nets: Theory and Application. 1 edition. London: Springer, 2002.

[15] JENSEN, Kurt. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Second Edition. London: Springer, 1996.

[16] HAAS, Peter J. Stochastic Petri Nets: Modelling, Stability, Simulation. London: Springer, 2002.

45

ESCOLA POLITCNICA

DE PERNAMBUCO

[17] MARSAN, M. A., et al. Modelling with Generalized Stochastic Petri Nets. New York: Wiley, 1995.

[18] FILHO, Antonio M. da S. O Papel da Especificao Formal no Desenvolvimento de Sistemas de Software. In: Revista Espao Acadmico, 2004.

[19] INA Integrated Net Analyzer. Disponvel em: < http://www2.informatik.hu-berlin.de/~starke/ina.html>. Acesso em: 23 de maio de 2007.

[20] MENEZES, Carlos. Caracterizao de Dano por Hidrognio em Aos API 5CT L80 13Cr por Meio de Ondas Ultra-Snicas. 2006. 130 f. Dissertao de Mestrado em Engenharia Metalrgica e de Materiais, Universidade Federal do Rio de Janeiro, Rio de Janeiro.

46

ESCOLA POLITCNICA

DE PERNAMBUCO

Modelo do Estudo de Caso

Representa o modelo em redes de Petri do Estudo de Caso, Captulo 5, seo 5.2

Apndice A