Os sistemas computacionais estão tomando proporções cada vez maiores envolvendo situações bastante complexas, onde muitas vezes erros são inaceitáveis, como em sistemas bancários, sistemas de controle de tráfego aéreo, etc... Para obter software confiável e com desempenho aceitável, pode-se aliar técnicas de desenvolvimento formal de software a técnicas de simulação de sistemas. O ambiente PLATUS reúne essas duas áreas: modelos de simulação são descritos usando gramáticas de grafos uma linguagem de especificação formal. Gramáticas de grafos são uma generalização de gramáticas de Chomsky, substituindo strings por grafos. Neste trabalho, serão tratadas gramáticas de grafos baseados em objetos, um modelo onde vértices e arcos são tipados, e as especificações são modulares (a especificação de um sistema consiste em várias gramáticas de grafos combinadas). Assim, o modelo de um sistema pode ser descrito de forma precisa, e a linguagem de especificação é bastante abstrata e expressiva. Num ambiente de simulação a questão da recuperação de dados merece uma atenção especial, uma vez que a eficiência do simulador está diretamente ligada a agilidade na obtenção das informações. Neste trabalho, o objetivo principal é definir uma representação para gramáticas de grafos que facilite o armazenamento, a recuperação e análise das estruturas identificadas no ambiente PLATUS, ou seja, gramáticas de grafos baseadas em objetos. São definidas também funções que implementam os procedimentos necessários, para a recuperação de dados durante a simulação. A eficiência dessas funções é demonstrada através do cálculo de sua ordem de complexidade. As estruturas são validadas através da implementação de um protótipo de banco de dados.

Das Hauptziel dieser Arbeit ist es, einen Ansatz fur die parallele Komposition von Graph- Grammatiken und eine Unfolding-Semantik genannte Semantik fiir Graph-Grammatiken bereitzustcllen, in der die Aspekte Nebenlaufigkeit und Kompositionalitat bzgl. der parallelen Komposition eine zentrale Rolle einnehmen. Die parallele Komposition von Graph-Grammatiken erlaubt die Komposition von Grammatiken bzgl. eines gemeinsamen (moglicherweise leeren) Anteils und basiert auf der parallelen und amalgamierten Komposition von Regeln der komponierten Grammtiken. Dariiber hinaus ist das Kompositionsergebnis syntaktisch und semantisch in geeigneter Weise mit den komponierten Grammatiken verkniipft. Die Unfolding-Semantik einer Graph-Grammatik ist eine echt nebenldufige, verzweigende Semantik, in der sowohl Zustande (Graphen) als auch Zustandsanderungen (Ableitungen) reprasentiert sind. Das Unfolding kann inkrementell konstruiert werden und es wird gezeigt, daß dies das gleiche Result liefert wie die Verklebung der deterministischen Berechnungen einer Grammatik Dartiberhinaus ist das Unfolding einer Graph-Grammatik selbst eine Graph- Grammatik, die einer speziellen Klasse von Graph-Grammatiken angehOrt: den Occurrence- Grammatiken. Hier wird diese Klasse axiomatisch definiert und die Elemente dieser Klasse kOnnen als Grammatiken gesehen werden, die (deterministische und nicht-deterministische) Berechnungen einer anderen Grammatik reprdsentieren. Die Semantik einer Grammatik, die aus der parallelen Komposition anderer Grammatiken entstanden ist, ist isomorph zur Komposition der Semantiken der komponierten Grammatiken. Dieses Kompatibilitatsresultat verbindet die parallele Komposition und die Unfolding Semantik in enger Weise. Da der Zweck der parallelen Komposition die Komposition nebenldufiger Systeme ist, stellt die Kompatibiliat von Komposition und Nebenlaufigkeitssemantik ein attraktives Ergebnis dar. / The main aims of this thesis are to provide an approach to the parallel composition of graph grammars and a semantics for graph grammars, called the unfolding semantics, in which the aspects of concurrency and compositionality with respect to the parallel composition play a central role. The parallel composition of graph grammar allows the composition of grammars with respect to a shared part (that may be empty), and is based on parallel and amalgamated composition of the rules of the component grammars. Moreover, the result of the composition is suitably syntactically and semantically related to the component grammars. The unfolding semantics of a graph grammar is a true concurrent, branching structure semantics in which states (graphs) as well as changes of states (derivations) are represented. The unfolding can be constructed incrementally, and we show that this yields the same result as a construction based on gluing of the deterministic computations of a grammar. Moreover, the unfolding of a graph grammar is itself a graph grammar that belong to a special class of graph grammars: the occurrence graph grammars. Here this class is defined axiomatically, and the members of this class can be seen as grammars that represent (deterministic and non-deterministic) computations of another grammars. The semantics of a grammar obtained as the parallel composition of other grammars is isomorphic to the composition of the semantics of the component grammars. As the purpose of the parallel composition is to be a composition for concurrent and reactive systems, the fact that this composition is compatible with a true concurrency semantics is an attractive result.

Das Hauptziel dieser Arbeit ist es, einen Ansatz fur die parallele Komposition von Graph- Grammatiken und eine Unfolding-Semantik genannte Semantik fiir Graph-Grammatiken bereitzustcllen, in der die Aspekte Nebenlaufigkeit und Kompositionalitat bzgl. der parallelen Komposition eine zentrale Rolle einnehmen. Die parallele Komposition von Graph-Grammatiken erlaubt die Komposition von Grammatiken bzgl. eines gemeinsamen (moglicherweise leeren) Anteils und basiert auf der parallelen und amalgamierten Komposition von Regeln der komponierten Grammtiken. Dariiber hinaus ist das Kompositionsergebnis syntaktisch und semantisch in geeigneter Weise mit den komponierten Grammatiken verkniipft. Die Unfolding-Semantik einer Graph-Grammatik ist eine echt nebenldufige, verzweigende Semantik, in der sowohl Zustande (Graphen) als auch Zustandsanderungen (Ableitungen) reprasentiert sind. Das Unfolding kann inkrementell konstruiert werden und es wird gezeigt, daß dies das gleiche Result liefert wie die Verklebung der deterministischen Berechnungen einer Grammatik Dartiberhinaus ist das Unfolding einer Graph-Grammatik selbst eine Graph- Grammatik, die einer speziellen Klasse von Graph-Grammatiken angehOrt: den Occurrence- Grammatiken. Hier wird diese Klasse axiomatisch definiert und die Elemente dieser Klasse kOnnen als Grammatiken gesehen werden, die (deterministische und nicht-deterministische) Berechnungen einer anderen Grammatik reprdsentieren. Die Semantik einer Grammatik, die aus der parallelen Komposition anderer Grammatiken entstanden ist, ist isomorph zur Komposition der Semantiken der komponierten Grammatiken. Dieses Kompatibilitatsresultat verbindet die parallele Komposition und die Unfolding Semantik in enger Weise. Da der Zweck der parallelen Komposition die Komposition nebenldufiger Systeme ist, stellt die Kompatibiliat von Komposition und Nebenlaufigkeitssemantik ein attraktives Ergebnis dar. / The main aims of this thesis are to provide an approach to the parallel composition of graph grammars and a semantics for graph grammars, called the unfolding semantics, in which the aspects of concurrency and compositionality with respect to the parallel composition play a central role. The parallel composition of graph grammar allows the composition of grammars with respect to a shared part (that may be empty), and is based on parallel and amalgamated composition of the rules of the component grammars. Moreover, the result of the composition is suitably syntactically and semantically related to the component grammars. The unfolding semantics of a graph grammar is a true concurrent, branching structure semantics in which states (graphs) as well as changes of states (derivations) are represented. The unfolding can be constructed incrementally, and we show that this yields the same result as a construction based on gluing of the deterministic computations of a grammar. Moreover, the unfolding of a graph grammar is itself a graph grammar that belong to a special class of graph grammars: the occurrence graph grammars. Here this class is defined axiomatically, and the members of this class can be seen as grammars that represent (deterministic and non-deterministic) computations of another grammars. The semantics of a grammar obtained as the parallel composition of other grammars is isomorphic to the composition of the semantics of the component grammars. As the purpose of the parallel composition is to be a composition for concurrent and reactive systems, the fact that this composition is compatible with a true concurrency semantics is an attractive result.

Os sistemas computacionais estão tomando proporções cada vez maiores envolvendo situações bastante complexas, onde muitas vezes erros são inaceitáveis, como em sistemas bancários, sistemas de controle de tráfego aéreo, etc... Para obter software confiável e com desempenho aceitável, pode-se aliar técnicas de desenvolvimento formal de software a técnicas de simulação de sistemas. O ambiente PLATUS reúne essas duas áreas: modelos de simulação são descritos usando gramáticas de grafos uma linguagem de especificação formal. Gramáticas de grafos são uma generalização de gramáticas de Chomsky, substituindo strings por grafos. Neste trabalho, serão tratadas gramáticas de grafos baseados em objetos, um modelo onde vértices e arcos são tipados, e as especificações são modulares (a especificação de um sistema consiste em várias gramáticas de grafos combinadas). Assim, o modelo de um sistema pode ser descrito de forma precisa, e a linguagem de especificação é bastante abstrata e expressiva. Num ambiente de simulação a questão da recuperação de dados merece uma atenção especial, uma vez que a eficiência do simulador está diretamente ligada a agilidade na obtenção das informações. Neste trabalho, o objetivo principal é definir uma representação para gramáticas de grafos que facilite o armazenamento, a recuperação e análise das estruturas identificadas no ambiente PLATUS, ou seja, gramáticas de grafos baseadas em objetos. São definidas também funções que implementam os procedimentos necessários, para a recuperação de dados durante a simulação. A eficiência dessas funções é demonstrada através do cálculo de sua ordem de complexidade. As estruturas são validadas através da implementação de um protótipo de banco de dados.

Os sistemas computacionais estão tomando proporções cada vez maiores envolvendo situações bastante complexas, onde muitas vezes erros são inaceitáveis, como em sistemas bancários, sistemas de controle de tráfego aéreo, etc... Para obter software confiável e com desempenho aceitável, pode-se aliar técnicas de desenvolvimento formal de software a técnicas de simulação de sistemas. O ambiente PLATUS reúne essas duas áreas: modelos de simulação são descritos usando gramáticas de grafos uma linguagem de especificação formal. Gramáticas de grafos são uma generalização de gramáticas de Chomsky, substituindo strings por grafos. Neste trabalho, serão tratadas gramáticas de grafos baseados em objetos, um modelo onde vértices e arcos são tipados, e as especificações são modulares (a especificação de um sistema consiste em várias gramáticas de grafos combinadas). Assim, o modelo de um sistema pode ser descrito de forma precisa, e a linguagem de especificação é bastante abstrata e expressiva. Num ambiente de simulação a questão da recuperação de dados merece uma atenção especial, uma vez que a eficiência do simulador está diretamente ligada a agilidade na obtenção das informações. Neste trabalho, o objetivo principal é definir uma representação para gramáticas de grafos que facilite o armazenamento, a recuperação e análise das estruturas identificadas no ambiente PLATUS, ou seja, gramáticas de grafos baseadas em objetos. São definidas também funções que implementam os procedimentos necessários, para a recuperação de dados durante a simulação. A eficiência dessas funções é demonstrada através do cálculo de sua ordem de complexidade. As estruturas são validadas através da implementação de um protótipo de banco de dados.

Das Hauptziel dieser Arbeit ist es, einen Ansatz fur die parallele Komposition von Graph- Grammatiken und eine Unfolding-Semantik genannte Semantik fiir Graph-Grammatiken bereitzustcllen, in der die Aspekte Nebenlaufigkeit und Kompositionalitat bzgl. der parallelen Komposition eine zentrale Rolle einnehmen. Die parallele Komposition von Graph-Grammatiken erlaubt die Komposition von Grammatiken bzgl. eines gemeinsamen (moglicherweise leeren) Anteils und basiert auf der parallelen und amalgamierten Komposition von Regeln der komponierten Grammtiken. Dariiber hinaus ist das Kompositionsergebnis syntaktisch und semantisch in geeigneter Weise mit den komponierten Grammatiken verkniipft. Die Unfolding-Semantik einer Graph-Grammatik ist eine echt nebenldufige, verzweigende Semantik, in der sowohl Zustande (Graphen) als auch Zustandsanderungen (Ableitungen) reprasentiert sind. Das Unfolding kann inkrementell konstruiert werden und es wird gezeigt, daß dies das gleiche Result liefert wie die Verklebung der deterministischen Berechnungen einer Grammatik Dartiberhinaus ist das Unfolding einer Graph-Grammatik selbst eine Graph- Grammatik, die einer speziellen Klasse von Graph-Grammatiken angehOrt: den Occurrence- Grammatiken. Hier wird diese Klasse axiomatisch definiert und die Elemente dieser Klasse kOnnen als Grammatiken gesehen werden, die (deterministische und nicht-deterministische) Berechnungen einer anderen Grammatik reprdsentieren. Die Semantik einer Grammatik, die aus der parallelen Komposition anderer Grammatiken entstanden ist, ist isomorph zur Komposition der Semantiken der komponierten Grammatiken. Dieses Kompatibilitatsresultat verbindet die parallele Komposition und die Unfolding Semantik in enger Weise. Da der Zweck der parallelen Komposition die Komposition nebenldufiger Systeme ist, stellt die Kompatibiliat von Komposition und Nebenlaufigkeitssemantik ein attraktives Ergebnis dar. / The main aims of this thesis are to provide an approach to the parallel composition of graph grammars and a semantics for graph grammars, called the unfolding semantics, in which the aspects of concurrency and compositionality with respect to the parallel composition play a central role. The parallel composition of graph grammar allows the composition of grammars with respect to a shared part (that may be empty), and is based on parallel and amalgamated composition of the rules of the component grammars. Moreover, the result of the composition is suitably syntactically and semantically related to the component grammars. The unfolding semantics of a graph grammar is a true concurrent, branching structure semantics in which states (graphs) as well as changes of states (derivations) are represented. The unfolding can be constructed incrementally, and we show that this yields the same result as a construction based on gluing of the deterministic computations of a grammar. Moreover, the unfolding of a graph grammar is itself a graph grammar that belong to a special class of graph grammars: the occurrence graph grammars. Here this class is defined axiomatically, and the members of this class can be seen as grammars that represent (deterministic and non-deterministic) computations of another grammars. The semantics of a grammar obtained as the parallel composition of other grammars is isomorphic to the composition of the semantics of the component grammars. As the purpose of the parallel composition is to be a composition for concurrent and reactive systems, the fact that this composition is compatible with a true concurrency semantics is an attractive result.

O aumento da escala e funcionalidade dos sistemas de computação e sua crescente complexidade envolvem um aumento significante de custos e exigem recursos humanos altamente qualificados para o desenvolvimento de software. Integrando-se o uso de métodos formais ao desenvolvimento de sistemas complexos, permite-se realizar análises e verificações destes sistemas, garantindo assim sua correção. Existem diversos formalismos que permitem descrever sistemas, cada qual com diferentes níveis de abstração. Quando consideramos sistemas complexos, surge a necessidade de um modelo que forneça construções abstratas que facilitem o entendimento e a especificação destes sistemas. Um modelo baseado em objetos fornece um nível de abstração que tem sido muito aplicado na prática, onde os dados e os processos que os manipulam são descritos juntos em um objeto. Gramática de Grafos Baseada em Objetos (GGBO) é um modelo baseado em objetos, que além de ser uma linguagem visual, apresenta a vantagem de as especificações adquirirem um estilo baseado em objetos, que é bastante familiar à maioria dos desenvolvedores. Porém, as GGBOs não possuem ainda ferramentas para verificação automática de propriedades desejadas nos sistemas modelados. Uma alternativa para resolver isso é definir uma tradução (que preserve a semântica) desta linguagem para outra, para a qual existam verificadores automáticos. Um formalismo bastante conhecido e estabelecido para descrição de sistemas concorrentes, para o qual existem verificadores automáticos, é o cálculo-π. Porém, sob o aspecto de especificação de sistemas complexos, GGBOs parecem ser mais adequadas como linguagem de especificação que o cálculo-π, pois são visuais, mais intuitivas e possuem um estilo baseado em objetos. Neste trabalho foi definido um formalismo (baseado nas GGBOs), denominado Gramática de Hipergrafos Baseada em Objetos e uma tradução deste formalismo para o cálculo-π, aliando assim as vantagens desses dois métodos. Além disso, para validar a tradução definida, foram feitas provas de que a semântica das gramáticas de hipergrafos baseadas em objetos é preservada na tradução.

O aumento da escala e funcionalidade dos sistemas de computação e sua crescente complexidade envolvem um aumento significante de custos e exigem recursos humanos altamente qualificados para o desenvolvimento de software. Integrando-se o uso de métodos formais ao desenvolvimento de sistemas complexos, permite-se realizar análises e verificações destes sistemas, garantindo assim sua correção. Existem diversos formalismos que permitem descrever sistemas, cada qual com diferentes níveis de abstração. Quando consideramos sistemas complexos, surge a necessidade de um modelo que forneça construções abstratas que facilitem o entendimento e a especificação destes sistemas. Um modelo baseado em objetos fornece um nível de abstração que tem sido muito aplicado na prática, onde os dados e os processos que os manipulam são descritos juntos em um objeto. Gramática de Grafos Baseada em Objetos (GGBO) é um modelo baseado em objetos, que além de ser uma linguagem visual, apresenta a vantagem de as especificações adquirirem um estilo baseado em objetos, que é bastante familiar à maioria dos desenvolvedores. Porém, as GGBOs não possuem ainda ferramentas para verificação automática de propriedades desejadas nos sistemas modelados. Uma alternativa para resolver isso é definir uma tradução (que preserve a semântica) desta linguagem para outra, para a qual existam verificadores automáticos. Um formalismo bastante conhecido e estabelecido para descrição de sistemas concorrentes, para o qual existem verificadores automáticos, é o cálculo-π. Porém, sob o aspecto de especificação de sistemas complexos, GGBOs parecem ser mais adequadas como linguagem de especificação que o cálculo-π, pois são visuais, mais intuitivas e possuem um estilo baseado em objetos. Neste trabalho foi definido um formalismo (baseado nas GGBOs), denominado Gramática de Hipergrafos Baseada em Objetos e uma tradução deste formalismo para o cálculo-π, aliando assim as vantagens desses dois métodos. Além disso, para validar a tradução definida, foram feitas provas de que a semântica das gramáticas de hipergrafos baseadas em objetos é preservada na tradução.

O aumento da escala e funcionalidade dos sistemas de computação e sua crescente complexidade envolvem um aumento significante de custos e exigem recursos humanos altamente qualificados para o desenvolvimento de software. Integrando-se o uso de métodos formais ao desenvolvimento de sistemas complexos, permite-se realizar análises e verificações destes sistemas, garantindo assim sua correção. Existem diversos formalismos que permitem descrever sistemas, cada qual com diferentes níveis de abstração. Quando consideramos sistemas complexos, surge a necessidade de um modelo que forneça construções abstratas que facilitem o entendimento e a especificação destes sistemas. Um modelo baseado em objetos fornece um nível de abstração que tem sido muito aplicado na prática, onde os dados e os processos que os manipulam são descritos juntos em um objeto. Gramática de Grafos Baseada em Objetos (GGBO) é um modelo baseado em objetos, que além de ser uma linguagem visual, apresenta a vantagem de as especificações adquirirem um estilo baseado em objetos, que é bastante familiar à maioria dos desenvolvedores. Porém, as GGBOs não possuem ainda ferramentas para verificação automática de propriedades desejadas nos sistemas modelados. Uma alternativa para resolver isso é definir uma tradução (que preserve a semântica) desta linguagem para outra, para a qual existam verificadores automáticos. Um formalismo bastante conhecido e estabelecido para descrição de sistemas concorrentes, para o qual existem verificadores automáticos, é o cálculo-π. Porém, sob o aspecto de especificação de sistemas complexos, GGBOs parecem ser mais adequadas como linguagem de especificação que o cálculo-π, pois são visuais, mais intuitivas e possuem um estilo baseado em objetos. Neste trabalho foi definido um formalismo (baseado nas GGBOs), denominado Gramática de Hipergrafos Baseada em Objetos e uma tradução deste formalismo para o cálculo-π, aliando assim as vantagens desses dois métodos. Além disso, para validar a tradução definida, foram feitas provas de que a semântica das gramáticas de hipergrafos baseadas em objetos é preservada na tradução.

O crescimento da complexidade e do tamanho dos sistemas computacionais atuais suscitou um aumento na dificuldade de extração e especificação de modelos formais desses sistemas, tornando essa atividade cada vez mais dispendiosa, tanto em tempo quanto em custo. Modelos são utilizados em diversas técnicas da Engenharia de Software, com o intuito de auxiliar em processos que compreendem desde o desenvolvimento de novos softwares, até reconstrução de um sistema a partir de software legado, passando pela realização de manutenção de um software em operação. Portanto, é necessário que essas abstrações sejam confiáveis e representem fielmente o software real. Nesse sentido, a adoção de métodos formais para a construção e análise de modelos computacionais é crescente e motivada, principalmente, pela confiabilidade que os formalismos matemáticos agregam aos modelos. No entanto, a utilização de métodos formais geralmente demanda um alto investimento de recursos humanos e, consequentemente, financeiros, uma vez que a utilização de tais formalismos é condicionada ao estudo profundo de sua fundamentação matemática. Considerando-se a extensa aplicabilidade de modelos em diversas subáreas da Ciência da Computação e as vantagens advindas da utilização de métodos formais para especificar sistemas, é interessante identificar métodos e ferramentas existentes para automatizar os processos de extração e análises de modelos, em conjunto com a adoção de formalismos que possam ser utilizados por profissionais da computação que atuam na indústria de software. Dessa forma, é estimulada nesse trabalho a utilização do formalismo de Gramática de Grafos, um método formal que diferencia-se dos demais por ser intuitivo e possuir uma representação visual gráfica, o que facilita a sua compreensão e não exige um conhecimento avançado sobre o formalismo. Primeiramente, é proposta uma abordagem para a extração de modelos em Gramática de Grafos a partir de código-fonte, extraindo informações de execuções de código Java anotado. Em seguida, é apresentada uma metodologia existente para extração e análise de Gramática de Grafos a partir de Casos de Uso, juntamente com um estudo empírico realizado a fim de validar a metodologia. Por fim, são propostas possíveis verificações adicionais, a fim de extender as análises dessa metodologia. Com isso, busca-se a obtenção de modelos, descritos através do formalismo de grafos, a partir de artefatos criados nos dois pólos do processo de desenvolvimento de software, antes e depois da implementação, no sentido de viabilizar futuras comparações, no contexto de verificação de software. / The growing size and complexity of current computer systems leading to an increase in the difficulty of extraction and specification of formal models of such systems, making it increasingly expensive activity, both in time and in cost. Models are used in various techniques of software engineering in order to assist in processes that range from the development of new software, to rebuild a system from legacy software, passing for performing maintenance of software in operation. Therefore, it is necessary that these abstractions are reliable and faithfully represent the actual software. In this sense, the adoption of formal methods for the construction and analysis of models is growing and motivated mainly by the reliability that the mathematical formalism add to models. However, the use of formal methods generally demands a high investment in human resources and hence financial, since the use of such formalism is conditioned to the deep study of its mathematical foundation. Considering the extensive applicability of models in various subfields of computer science and the benefits arising from the use of formal methods for specifying systems, it is interesting to identify existing methods and tools to automate the process of extracting models, in addition to the adoption of formalism that can be used by computer professionals working in the software industry. Thus, we encourage the use of the Graph Grammar formalism, a formal method that differs from others because it is intuitive and has a graphical visual representation, making it easy to understand and does not require an advanced knowledge of the formalism. First, we propose an approach for extracting models from source code in Graph Grammar, getting information of executions of annotated Java code. Then an existing methodology for extraction and analysis of Graph Grammar from Use Cases is presented, along with an empirical study to validate the methodology. Finally, we propose possible additional checks in order to extend the analysis of this methodology. Thus, this work aims to extract models, described by the formalism of graphs, from artifacts created in the two poles of the software development process, before and after implementation, in order to allow future comparisons, in the context of software verification.