We present a formal modeling approach for the design and simulation of Multi-Unmanned Aerial Vehicle (multi-UAV) inspection scenarios, where planning is based on model checking. As demonstration, we formalize and simulate a compositional UAV inspection system of a solar park using bigraphical reactive systems, which introduce the notion of time-varying bigraphs. Specifically, the UAV system is modeled as a process-algebraic expression, whose semantics is a bigraph state in a labeled transition system. The underlying Multi-Agent Path Finding problem is solved model-theoretically using Planning-by-Model-Checking. It solves the inherently connected collision-free path planning problem for multiple UAVs subject to contexts and local conditions. First, a bigraph is constructed algebraically, which can be decomposed systematically into separate parts with interfaces. The layered composite model accounts for location, navigation, UAVs, and contexts, which enables simple configuration and extension (changeability). Second, the executable operational semantics of our formal bigraph model are given by bigraphical reactive systems, where rules constitute the behavioral component of our model. Rules reconfigure the bigraph to simulate state changes, i.e., they allow to alter the conditions under which UAVs are permitted to move. Properties can be attached to nodes of the bigraph and evaluated in a simulation over the traces of the transition system according to some cost-based policies. In essence, the inherent multi-UAV path planning problem of our scenario is formulated as a reachability problem and solved by model checking the generated transition system. The bigraph-algebraic expression also allows us to reason about potential parallelization opportunities when moving UAVs. Moreover, we sketch how to directly simulate the bigraph specification in a ROS-based Gazebo simulation by examining the inspection and monitoring of a solar park as an application. The reactive system specification provides the blueprint for analysis, simulation, implementation and execution. Thus, the same algorithm used for verification is used as well for the simulation in ROS/Gazebo to execute plans.:1 Introduction 2 Overview: Scenario Description and Formal Modeling Approach 3 Background: Bigraphs and Model Checking 4 Construction of the UAV System via Composition 5 Making the Drones Fly: Executable Model Semantics 6 Collision-Free Path Planning Problem 7 Prototypical Implementation 8 Discussion 9 Related Work 10 Conclusion A UAV State Machine B Bigraphical Reactive Systems C RPO/IPO Semantic

A Linguagem RS é destinada a programação de núcleos reativos centralizados. Tais núcleos são responsáveis por toda a lógica de um sistema reativo, manipulando os sinais de entrada, realizando as reações e gerando os sinais de saída. Sendo sua idéia inicial tratar apenas processos centralizados, não houve a preocupação com a distribuição. Este trabalho tem como principal objetivo apresentar os aspectos introduzidos de uma nova versão para a Linguagem e para o Compilador RS, que possibilitam a execução de programas distribuídos. Além da possibilidade de execução de sistemas reativos distribuídos, foi acrescentado à Linguagem RS extensões já previstas na sua criação, como sinais inibidores, regras de exclusão mútua e concomitância, a possibilidade de disparo de mais de uma regra em um mesmo instante e a limpeza léxica do código fonte RS. As modificações incorporadas nesta nova versão da linguagem, foram efetivadas através de um novo compilador, chamado de Compilador RS 5.0. O protótipo implementado oferece a geração de três formatos de código: o formato padrão da linguagem RS (os autômatos e as regras correspondentes), códigos na linguagem C para a simulação dos autômatos (tanto para programas distribuídos quanto não-distribuídos) e arquivos no formato portável OC, que é um formato de código objeto padrão para as linguagens reativas. Para a distribuição e implementação da Linguagem RS foi necessária a criação de um novo núcleo de comunicação do MDX, que é responsável pela comunicação dos autômatos RSD. Este núcleo é dividido em três partes. A primeira trata da definição de um modelo formal com as mudanças necessárias para que a linguagem RS consiga trabalhar de forma distribuída, a segunda mostra o projeto do novo núcleo MDX e a terceira apresenta a implementação em C e MDX dos autômatos gerados pelo Compilador RS 5.0. Por fim, exemplos de aplicação desta nova linguagem são apresentados, onde podem ser vistos a importância e o acréscimo proporcionado por este trabalho tanto à linguagem RS quanto à programação de sistemas reativos síncronos. / The RS language is intended to the programming of centralized reactive kernels. Such kernels are responsible for the logic of a reactive system, manipulating the input signals, carrying through the reactions and generating the output signals. Being its initial idea to treat only centered processes, it did not have the concern with the distribution. The main objective of this work is to describe the process of creation of a new version for the Language and Compiler RS, that make possible the execution of distributed programs. Beyond the possibility of execution distributed reactive systems, it was added to RS language foreseen extensions already in its creation, as inhibiting signals, rules of manual exclusion and concurrence, the possibility of detonation of more than a rule in one exactly instant and the lexical cleanness of the RS code source. The modifications incorporated in this new version of the language, had been accomplished through a new compiler, called Compiler RS 5.0. The implemented archetype offers the generation of three formats of code: the standard format of RS language (the corresponding automatons and rules), codes in the language C for the simulation of the automatons and archives in OC portable format, that is a object format code standard for the reactive languages. For the distribution and implementation of Language RS was necessary the creation of a new kernel of communication of the MDX, that is responsible for the communication of RSD automatons. It is divided in three parts. The first one deals with the definition of a formal model that defines the necessary changes so that RS language obtains to work of distributed form, the second shows the design of new MDX kernel and third presents the implementation in C and MDX of the automatons generated for Compiler RS 5.0. Finally, examples of application of this new language are presented, where the importance and the proportionate upgrade for this work to RS language how to the programming of synchronous reactive systems can in such a way be seen.

A Linguagem RS é destinada a programação de núcleos reativos centralizados. Tais núcleos são responsáveis por toda a lógica de um sistema reativo, manipulando os sinais de entrada, realizando as reações e gerando os sinais de saída. Sendo sua idéia inicial tratar apenas processos centralizados, não houve a preocupação com a distribuição. Este trabalho tem como principal objetivo apresentar os aspectos introduzidos de uma nova versão para a Linguagem e para o Compilador RS, que possibilitam a execução de programas distribuídos. Além da possibilidade de execução de sistemas reativos distribuídos, foi acrescentado à Linguagem RS extensões já previstas na sua criação, como sinais inibidores, regras de exclusão mútua e concomitância, a possibilidade de disparo de mais de uma regra em um mesmo instante e a limpeza léxica do código fonte RS. As modificações incorporadas nesta nova versão da linguagem, foram efetivadas através de um novo compilador, chamado de Compilador RS 5.0. O protótipo implementado oferece a geração de três formatos de código: o formato padrão da linguagem RS (os autômatos e as regras correspondentes), códigos na linguagem C para a simulação dos autômatos (tanto para programas distribuídos quanto não-distribuídos) e arquivos no formato portável OC, que é um formato de código objeto padrão para as linguagens reativas. Para a distribuição e implementação da Linguagem RS foi necessária a criação de um novo núcleo de comunicação do MDX, que é responsável pela comunicação dos autômatos RSD. Este núcleo é dividido em três partes. A primeira trata da definição de um modelo formal com as mudanças necessárias para que a linguagem RS consiga trabalhar de forma distribuída, a segunda mostra o projeto do novo núcleo MDX e a terceira apresenta a implementação em C e MDX dos autômatos gerados pelo Compilador RS 5.0. Por fim, exemplos de aplicação desta nova linguagem são apresentados, onde podem ser vistos a importância e o acréscimo proporcionado por este trabalho tanto à linguagem RS quanto à programação de sistemas reativos síncronos. / The RS language is intended to the programming of centralized reactive kernels. Such kernels are responsible for the logic of a reactive system, manipulating the input signals, carrying through the reactions and generating the output signals. Being its initial idea to treat only centered processes, it did not have the concern with the distribution. The main objective of this work is to describe the process of creation of a new version for the Language and Compiler RS, that make possible the execution of distributed programs. Beyond the possibility of execution distributed reactive systems, it was added to RS language foreseen extensions already in its creation, as inhibiting signals, rules of manual exclusion and concurrence, the possibility of detonation of more than a rule in one exactly instant and the lexical cleanness of the RS code source. The modifications incorporated in this new version of the language, had been accomplished through a new compiler, called Compiler RS 5.0. The implemented archetype offers the generation of three formats of code: the standard format of RS language (the corresponding automatons and rules), codes in the language C for the simulation of the automatons and archives in OC portable format, that is a object format code standard for the reactive languages. For the distribution and implementation of Language RS was necessary the creation of a new kernel of communication of the MDX, that is responsible for the communication of RSD automatons. It is divided in three parts. The first one deals with the definition of a formal model that defines the necessary changes so that RS language obtains to work of distributed form, the second shows the design of new MDX kernel and third presents the implementation in C and MDX of the automatons generated for Compiler RS 5.0. Finally, examples of application of this new language are presented, where the importance and the proportionate upgrade for this work to RS language how to the programming of synchronous reactive systems can in such a way be seen.

A Linguagem RS é destinada a programação de núcleos reativos centralizados. Tais núcleos são responsáveis por toda a lógica de um sistema reativo, manipulando os sinais de entrada, realizando as reações e gerando os sinais de saída. Sendo sua idéia inicial tratar apenas processos centralizados, não houve a preocupação com a distribuição. Este trabalho tem como principal objetivo apresentar os aspectos introduzidos de uma nova versão para a Linguagem e para o Compilador RS, que possibilitam a execução de programas distribuídos. Além da possibilidade de execução de sistemas reativos distribuídos, foi acrescentado à Linguagem RS extensões já previstas na sua criação, como sinais inibidores, regras de exclusão mútua e concomitância, a possibilidade de disparo de mais de uma regra em um mesmo instante e a limpeza léxica do código fonte RS. As modificações incorporadas nesta nova versão da linguagem, foram efetivadas através de um novo compilador, chamado de Compilador RS 5.0. O protótipo implementado oferece a geração de três formatos de código: o formato padrão da linguagem RS (os autômatos e as regras correspondentes), códigos na linguagem C para a simulação dos autômatos (tanto para programas distribuídos quanto não-distribuídos) e arquivos no formato portável OC, que é um formato de código objeto padrão para as linguagens reativas. Para a distribuição e implementação da Linguagem RS foi necessária a criação de um novo núcleo de comunicação do MDX, que é responsável pela comunicação dos autômatos RSD. Este núcleo é dividido em três partes. A primeira trata da definição de um modelo formal com as mudanças necessárias para que a linguagem RS consiga trabalhar de forma distribuída, a segunda mostra o projeto do novo núcleo MDX e a terceira apresenta a implementação em C e MDX dos autômatos gerados pelo Compilador RS 5.0. Por fim, exemplos de aplicação desta nova linguagem são apresentados, onde podem ser vistos a importância e o acréscimo proporcionado por este trabalho tanto à linguagem RS quanto à programação de sistemas reativos síncronos. / The RS language is intended to the programming of centralized reactive kernels. Such kernels are responsible for the logic of a reactive system, manipulating the input signals, carrying through the reactions and generating the output signals. Being its initial idea to treat only centered processes, it did not have the concern with the distribution. The main objective of this work is to describe the process of creation of a new version for the Language and Compiler RS, that make possible the execution of distributed programs. Beyond the possibility of execution distributed reactive systems, it was added to RS language foreseen extensions already in its creation, as inhibiting signals, rules of manual exclusion and concurrence, the possibility of detonation of more than a rule in one exactly instant and the lexical cleanness of the RS code source. The modifications incorporated in this new version of the language, had been accomplished through a new compiler, called Compiler RS 5.0. The implemented archetype offers the generation of three formats of code: the standard format of RS language (the corresponding automatons and rules), codes in the language C for the simulation of the automatons and archives in OC portable format, that is a object format code standard for the reactive languages. For the distribution and implementation of Language RS was necessary the creation of a new kernel of communication of the MDX, that is responsible for the communication of RSD automatons. It is divided in three parts. The first one deals with the definition of a formal model that defines the necessary changes so that RS language obtains to work of distributed form, the second shows the design of new MDX kernel and third presents the implementation in C and MDX of the automatons generated for Compiler RS 5.0. Finally, examples of application of this new language are presented, where the importance and the proportionate upgrade for this work to RS language how to the programming of synchronous reactive systems can in such a way be seen.

The purpose of the study is to identify problems with existing fraud prevention systems that deals with Wangiri fraud. We also intend to identify how it is possible to reduce the detection time of Wangiri fraud using reactive systems. The aim of the study is to find out if reactive solutions can be used in the development of fraud prevention systems.  The conclusion reached in the study is that reactive systems can be used to detect Wangiri fraud faster for telecom companies that have a similar process for handling call data. / Syftet med undersökningen är att identifiera problem med existerande bedrägerisystem som hanterar Wangiri bedrägerier. Vi avser också att identifiera på vilket sätt det är möjligt att minska upptäckstiden av Wangiri bedrägerier med hjälp av reaktiva system. Målet med undersökningen är att ta reda på om reaktiva lösningar kan användas inom utvecklingen av bedrägerisystem. Slutsatsen som framkommit i studien är att reaktiva system är möjliga att använda för att snabbare upptäcka Wangiri bedrägerier för telekombolag som har en liknande process för hantering av samtalsuppgifter

The advances in mobile telecommunication networks as well as in mobile device technology have stimulated the development of a wide range of mobile applications. While it is sensible to install at least some components of applications on mobile devices to gain independence of rather unreliable mobile network connections, it is difficult to decide about the suitable application components and the amount of data to be provided. Because the environment of a mobile device can change and mobile business processes evolve over time, the mobile system should adapt to these changes dynamically to ensure productivity. In this paper, we present a mobile middleware that targets typical problems of mobile applications and dynamically adapts to context changes at runtime by utilizing reconfiguration triggers.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-23T13:23:08Z No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) / Made available in DSpace on 2018-08-23T13:23:08Z (GMT). No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) Previous issue date: 2006-05-26 / Técnicas e ferramentas de testes formais baseados em modelos têm sido desenvolvidas para tornar mais rigoroso e eficiente o processo de teste de sistemas reativos com características de distribuição e concorrência. O não-determinismo inerente a estes sistemas torna os difíceis de serem testados, devido à alta complexidade de obtenção das configurações necessárias para execução dos casos de teste. As propriedades especificadas para estes sistemas são a base para a geração dos casos de teste de conformidade, que devem avaliar a correspondência entre modelo e código. Estas propriedades, denominadas objetivos de teste, devem ser especificadas de maneira a guiar a geração dos casos de teste. Entretanto, a especificação dos objetivos de teste a partir de modelos complexos como os destes sistemas ainda carece de técnicas e ferramentas apropriadas, tornando esta atividade propensa a erros. Os casos de teste podem assim, ter efetividade afetada em caso de erros na especificação dos objetivosdeteste. Comoobjetivodecontribuirparaasoluçãodesteproblema,estetrabalho apresenta técnica de geração de objetivos de teste para sistemas reativos, baseando-se na técnica de verificação de modelos CTL. A técnica proposta visa usufruir da eficiência dos algoritmos da verificação de modelos, por meio de sua adaptação para a análise destes, para a geração dos objetivos de teste. / Techniques and tools for model based testing have been developed to make the process of testing distributed concurrent reactive systems more efficient and rigorous. The inherent nondeterminism of these systems can make it difficult to test them due to the complex process of obtaining test cases configurations from models. To better guide the testing process, properties specified to these systems are used as basis for the test case generation. Such properties, called test purposes, shall be exhibitedby the implementation under test through test case execution. However, specifying test purposes from the common complex and large models of these systems suffers from the lack of appropriated tools and techniques, making it error-prone and inadequate. Thus, test cases based on such test purposes may be affected, getting no desirable soundness. Aiming at solving this problem, we present a technique for test purpose generation for reactive systems based on the CTL model checking technique. We aim at taking benefit from the efficiency of model checking algorithms to better analyze the models to generate the test purposes.

Orientador: Arnaldo Vieira Moura / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-15T05:28:23Z (GMT). No. of bitstreams: 1 Bonifacio_AdilsonLuiz_D.pdf: 1228504 bytes, checksum: 62db4b0286cfd1c735336e429629b3de (MD5) Previous issue date: 2009 / Resumo: O objetivo deste trabalho é prover métodos eficientes de geração de casos de teste para sistemas reativos críticos. Sistemas dessa natureza compreendem sistemas de tempo real e com transformações de contexto. Uma das técnicas mais usadas na geração de conjuntos de teste tem sido a abordagem baseada em modelos formais. Neste caso, os formalismos fornecem uma base sólida para que a atividade de teste seja efetuada de forma precisa e segura. Este trabalho propõe a construção de modelos formais, métodos e técnicas, bem como estratégias de teste, para dar suporte ao processo de geração automática de conjuntos de teste, aplicáveis a sistemas complexos. Porém, o processo de geração de testes baseado em modelos se torna, muitas vezes, impraticável em aplicações reais, devido ao problema da explosão combinatória de estados. Daí a necessidade de se encontrar modelos adequados que capturem o comportamento desejado dos sistemas a serem testados, bem como a importância de se construir métodos que contornem o problema da explosão do espaço de estado, de maneira razoável, permitindo que a geração de testes seja um processo aplicável a sistemas complexos. Entre os modelos abordados neste trabalho estão: (i) as tradicionais Máquinas de Estados Finito (FSM); (ii) uma extensão das FSMusando variáveis de contexto, as Máquinas de Estados Finito Estendida (EFSM); (iii) a extensão temporizada de EFSM (TEFSM), que possui, não apenas variáveis de contexto, mas também variáveis relógio; (iv) os modelos temporizados com entradas e saídas independentes, conhecidos como Timed I/O Automata (TIOA); e (v) uma extensão proposta para TIOA, denominado Timed I/O Context Automata (TIOCA), para compreender a evolução contínua de tempo e também as transformações de contexto. Com relação a geração de testes baseada em tais modelos, foi proposto, primeiramente, uma técnica de derivação de sequências de confirmação para TEFSM, usando model-checking. Em seguida, foi proposta uma generalização para um método de geração de conjuntos completos de teste usando FSM. Também foi desenvolvido um novo método de discretização do modelo TIOA, provendo a base necessária para a geração de casos de teste usando os conceitos de proposta de teste e produto síncrono. Por fim, foi desenvolvida uma extensão do método de discretização para TIOA também proposto neste trabalho, aplicado ao modelo TIOCA, permitindo a geração de testes em sistemas com evolução contínua de tempo e fluxo de dados, usando os conceitos de proposta de teste e produto de TIOCA / Abstract: This work aims to provide efficient test case generation methods for reactive and critical systems. In general, reactive and critical systems are real-time systems with context transformations. One of the most promising techniques for generating test suites is model-based testing. The formalisms supply the basis to perform a precise and dependable testing activity. In this scenery, our work proposes a construction of formal models, methods and techniques, as well as testing strategies, to support the process of automatically generating test suites for complex systems. However, the test generation process using formal models is usually infeasible in real applications, due to the state space explosion. Therefore, we need to find out suitable models to capture the system behaviors, and also to construct methods that can overcome the explosion problem, in a reasonable way, allowing the generation of test suites for complex systems. In this work we treat the following formal models: the conventional FSM; an extension of FSM using context variables (EFSM); the proposed extension of EFSM (TEFSM) to capture context variables and also clock variables; timed models, with disassociated input and output actions, called TIOA; and the proposed extension for TIOA, so-called TIOCA, to capture continuous time evolution and context transformations. In a first step of this work we proposed a technique to derive confirming sequences for TEFSM, using model-checking. Next, a classical method to generate complete test suites was generalized for FSM.We also proposed a new discretizationmethod for TIOA models, allowing the test case generation using test purpose and the synchronous product. Lastly, we extended the discretization method for TIOA to obtain more compact grid automata for TIOCA models, allowing the test case generation for systems with continuous time evolution and data flow transformations, using the notion of test purpose and the product of TIOCA / Doutorado / Teoria da Computação e Teste de Sistemas / Doutor em Ciência da Computação

It is well-recognized among computer scientists that prospective informatics systems will become more and more complex and will increasingly accumulate non-linear behaviour that is difficult to orchestrate, to configure, and to reason about. Certainly, large-scale mobile computing systems will challenge our understanding, similar to climate systems, bio-chemical systems, physical systems, or social networks. This suggests a rigorous formalization and study of non-trivial computational systems. In this regard, bigraphs are a groundbreaking novel theory for distributed and parallel systems, treating mobile locality and mobile interaction as first-class citizens. The theory was devised by Robin Milner as a process algebra with rewrite capabilities based on graph equations and an algebraic type system. Bigraphs have been the subject of extensive investigation from various perspectives, including agent-based modelling, cyber-physical games, language construction, graph rewriting, and as a unifying metamodel for other rewrite theories and process calculi, but particularly in the context of the categorical reactive system approach. In this approach, a labelled transition system, over which bisimilarity is a congruent equivalence relation, is generated from reduction semantics that can be freely specified. The bigraph theory treats two-dimensional graphs as arrows and their interfaces as objects while category theory provides the underlying mathematical framework for their axiomatization. Fortunately, category theory makes the theory future-proof, competitive and extensible. The recently developed categorical concepts of relative and idempotent pushouts facilitate the categorical construction of minimal context labels enabling the development of a behavioural theory, where bisimulation is a congruence. The metamodel character of bigraphs enables the comparison of other formalisms and algebraic theories of concurrent computation at a very abstract level, thus, regaining their behavioural theory and computational notion, with the ultimate goal of exploiting synergies. Indeed, bigraphs are much more than a computational model for understanding, analysing, and verifying systems. They provide both a formal and practical foundation for context-oriented reactive system modelling and programming languages. Consequently, the development of software solutions based on the bigraph theory necessitates suitable tools, frameworks, and languages for putting bigraphs into practice. These tools are essential for evaluating the model’s effectiveness in both academic research and the software industry. Only this permits rigorous testing of the theory. But moreover, reaching this goal is the result of the motivation to lower the barrier to entry for model-driven context-adaptive programming using the bigraph theory. So far, several tools and libraries have been developed to model and simulate bigraphical reactive systems. These tools can roughly be referred to as bigraphical calculators and are meant for experimentation and comprehension of the theory. Without them, this work could not have been written. However, we elevate the initial efforts to a level more conducive to enable advanced bigraphical software engineering practises. Therefore, the Bigraph Toolkit Suite was developed—a collection of tools and methods for the research and development of reactive systems for real-world applications. The suite consists of model-based integration frameworks, architectural guidelines, integrated development environments, command-line tools, and an uncomplicated language engineering workbench with an extensible grammar and interpreter. Each product of the Bigraph Toolkit Suite serves a distinct function, ranging from the manipulation and simulation of bigraphs to bigraphical language engineering and distributed storage of bigraph models. The tools are finely tuned to each other via a common metamodel, which facilitates implementation of novel bigraphical tool chains as well as the integration of arbitrary tools and public programming interfaces. Certainly, the following ambient question paved the path of this research: Is there a formalism or theory that supports context modelling, computation and verification, and that can be used as a programming language? The work shows that bigraphs can be used to lay such a foundation to regain the understanding of new informatics systems, with model-driven engineering contributing to this. According to this, the latent objective of this work is the cross-fertilization process of model-driven engineering and bigraphical reactive systems on a practical basis. A discussion is developed of whether there is evidence to support the view that the presence of MDE-related model operations and practices may be related to bigraph operations and vice versa. A relation can be established by a consistent and complete canonical mapping on the x-axis based on a systematic four-layer metamodelling framework; and on the y-axis between three different yet interoperable technical spaces. Thus, the result of this thesis is developed along two axes from a strict software engineering perspective. On the one hand, practical observations of the bigraph theory are provided about other graph structures, categories and model-driven operations. On the other, a novel software ecosystem for bigraphical reactive systems is provided together with several generic experimental approaches such as event-based execution of sub-bigraphical reactive systems. The theory already stimulated much other research works and therefore advancing fundamental computer science, this work may additionally—hopefully, the reader will agree—solidify and advance bigraphical research.:1 Introduction 1.1 Background and Motivation 1.1.1 Typical Application Scenarios 1.1.2 The Dilemma of Complex Reactive Systems 1.2 Field of Work 1.2.1 Reactive Systems 1.2.2 Model-driven Engineering 1.2.3 Context Adoption in Software: A Novel Taxonomy 1.3 Research Project 1.3.1 Hypothesis 1.3.2 Research Aim 1.3.3 Research Objectives 1.3.4 Contributions 1.4 Outline 2 The Theory of Bigraphical Reactive Systems for Software Engineers 2.1 Graph Theory: Basic Notation 2.2 Categories for Context-adaptive Software 2.2.1 Elementary Category Theory 2.2.2 Reactive System Categories: s-category and spm category 2.2.3 Type Graphs and Type Morphisms 2.2.4 Observations 2.3 On the Static Structure of Bigraphs 2.3.1 Signatures 2.3.2 Pure Bigraphs: Place Graphs and Link Graphs 2.3.3 Compositional Structures: Interfaces and Operators 2.3.4 Algebra of Bigraphs 2.3.5 Graphical s-categories 2.4 Type Systems and Sortings 2.4.1 Basic Terminology 2.4.2 Sortings and Bigraphs 2.5 Dynamics of Reactive Systems 2.5.1 Operational Semantics of Reactive Systems 2.5.2 Reactive System Theory: General Categories 2.5.3 Bigraphical Reactive Systems 2.5.4 Labelled Transition Systems 2.5.5 Behavioural Equivalences 2.5.6 Observations 2.6 Formal Verification 2.6.1 Model Checking in Detail 2.6.2 Properties of Sequential and Parallel Programs 2.6.3 State-Space Explosion Problem 3 Model-driven Concepts in Bigraphs 3.1 A Canonical Mapping: From Bigraphs to Ecore 3.1.1 The Four-layer Metamodelling Framework Revisited 3.1.2 Formal Relations between Bigraphs, Type Graphs and Ecore 3.1.3 Model Constraints at the 𝑀1 and 𝑀0 layer 3.1.4 Design Level Variability and Extensibility 3.2 Bigraphical Models: Specification and Generation 3.2.1 Typing and Subtyping via (Un-)Sorted Signatures and their Instantiation from Metamodels 3.2.2 Bigraphs and their Instantiation from Metamodels 3.2.3 Observations 3.3 Modelling Techniques: A Bigraphical Perspective 3.3.1 Bigraphs and UML Class Diagrams 3.3.2 Signature Operations 3.3.3 Abstraction 3.3.4 View Modelling with Place Graphs 3.4 Design Patterns for Implementing Variation Points 3.5 Summary 4 Bigraph Toolkit Suite: A Complete Software Development Ecosystem 4.1 The Bigraphical Tool Landscape 4.1.1 High-level Architecture 4.1.2 Overview of the Constituents 4.1.3 Design Qualities 4.1.4 Project Organisation 4.2 Modelling and Visualization 4.2.1 Programmatic Approach: Builders and Operators 4.2.2 Domain-specific Language 4.2.3 Converters: Model Translations 4.2.4 Visual Modelling: Bigellor 4.3 Simulation and Verification 4.3.1 Specification of BRSs 4.3.2 Implementation Aspects: Entity Classes 4.3.3 Implementation Aspects: Business Classes 4.3.4 Model Checking Algorithm 4.3.5 Coordination of BRSs: Higher-order Execution Strategies 4.3.6 Error Handling: Chain of Responsibility and Exceptions 4.4 Bigraphical Domain-specific Language 4.4.1 Overview of BDSL’s Grammar 4.4.2 Language Features 4.4.3 Interpreter: Decoupling the Grammar from Application-Specific Code 4.4.4 BDSL-CLI: A Command-line Interpreter Tool for BDSL 4.4.5 Theia: An Integrated Development Environment for BDSL 4.5 Persistence: Distributed Model Storage 4.5.1 Basic Filesystem Storage Facilities 4.5.2 Spring Data CDO: Spring Data and Connected Data Objects 4.5.3 Arbitrary Hierarchical Layouts for Bigraphical Models 4.5.4 Event Listeners 4.6 Performance and Quality Analysis 4.6.1 Functional Tests 4.6.2 Dependency Analysis 4.6.3 Runtime Analysis 4.7 Summary 5 Related Work: The Bigraphical Tool Landscape 5.1 A Lightweight Qualitative Comparison Framework 5.1.1 Conceptual Foundations 5.1.2 Considerations 5.2 Method and Tool Candidates 5.2.1 Selection Process 5.2.2 Excluded Tool Candidates 5.2.3 Tool Overview 5.3 Results 5.3.1 jLibBig 5.3.2 bigraphspace 5.3.3 BigRED 5.3.4 BigM 5.3.5 BigraphER 5.3.6 BigMC 5.3.7 BPL Tool 5.3.8 BiGMTE 5.3.9 DBtk 5.4 Evaluation and Discussion 5.4.1 Assessment Criteria 5.4.2 Comparison of Non-Functional Aspects 5.4.3 Comparison of Functional Aspects 5.4.4 Term Language 5.4.5 Interoperability 5.4.6 Accessibility 5.5 Summary 6 Conclusion List of Figures List of Tables List of Listings Bibliography Online Resources Appendices A Theoretical Addendum B Design Patterns, Techniques and Technologies C Code Listings: Related Work Abbreviations

Com a crescente complexidade das aplicações e sistemas computacionais, atualmente tem se tornado importante o uso de formalismos de várias naturezas na representação e modelagem de problemas complexos, como os sistemas reativos e concorrentes. Este trabalho apresenta uma contribuição na Tecnologia Adaptativa e uma nova técnica no desenvolvimento de uma aplicação para execução de alguns tipos de jogos, (General Game Playing), cuja característica está associada à capacidade de o sistema tomar conhecimento das regras do jogo apenas em tempo de execução. Com esse trabalho, amplia-se a classe de problemas que podem ser estudados e analisados sob a perspectiva da Tecnologia Adaptativa, através dos Dispositivos Adaptativos Cooperantes. A aplicação desenvolvida como exemplo neste trabalho introduz uma nova ótica no desenvolvimento de aplicações para jogos gerais (GGP) e abre novos horizontes para a aplicação da Tecnologia Adaptativa, como a utilização das regras para extração de informação e inferência. / The complexity of computer applications has grown so much that several formalisms of different kinds became important nowadays. Many systems (e.g. reactive and concurrent ones) employ such formalisms to represent and model actual complex problems. This work contributes to the field of Adaptive Technology, and proposes a new approach for developing general game playing system, whose feature is the capability to play a game by acknowledging the game rules only at run time. This work expands the set of problems that can be studied and analyzed under the Adaptive Technology perspective, by means of cooperating adaptive devices. The developed application used a new approach for general game playing development bringing and widens the application field of Adaptive Technology with subjects related to information extraction and inference based in the devices rules.