A bigraph-driven vending machine is implemented. The application is realized as a Spring-based webservice. Actions can be initiated by REST endpoints. The system follows a rule-based architecture, where possible operations are grounded on a rule set. Bigraphical Reactive Systems are used for the specification and execution. The actual state of the application is a bigraph stored in a database, which can be viewed and altered directly in the database. A history of states is kept - the application can be transferred to any prior state. The application can be updated or extended by merely changing the bigraphical database model.:First Part: A system of a vending machine is specified and analyzed using BDSL. This concerns the static and dynamic aspects of the system. Second Part: The analysis results are re-used for the implementation using Bigraph Framework. The application is realized as a webservice that is built using the Spring framework. / Ein bigraph-gesteuerter Verkaufsautomat wird implementiert. Die Anwendung ist als Spring-basierter Webservice realisiert. Aktionen können über REST-Endpunkte initiiert werden. Das System folgt einer regelbasierten Architektur, bei der die möglichen Operationen auf einem Regelsatz beruhen. Für die Spezifikation und Ausführung werden Bigraphical Reactive Systems verwendet. Der aktuelle Zustand der Anwendung ist ein in einer Datenbank gespeicherter Bigraph, der direkt in der Datenbank eingesehen und verändert werden kann. Es wird eine Historie der Zustände geführt - die Anwendung kann in einen beliebigen früheren Zustand überführt werden. Die Anwendung kann aktualisiert oder erweitert werden, indem lediglich das bigraphische Datenbankmodell geändert wird.:First Part: A system of a vending machine is specified and analyzed using BDSL. This concerns the static and dynamic aspects of the system. Second Part: The analysis results are re-used for the implementation using Bigraph Framework. The application is realized as a webservice that is built using the Spring framework.

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

L'élasticité est une propriété qui permet aux systèmes Cloud de s'auto-adapter à leur charge de travail en provisionnant et en libérant des ressources informatiques, de manière autonomique, lorsque la demande augmente et diminue. En raison de la nature imprévisible de la charge de travail et des nombreux facteurs déterminant l'élasticité, fournir des plans d'action précis pour gérer l'élasticité d'un système cloud, tout en respectant des politiques de haut niveau (performances, cout, etc.) est une tâche particulièrement difficile.Les travaux de cette thèse visent à proposer, en utilisant le formalisme des bigraphes comme modèle formel, une spécification et une implémentation des systèmes Cloud Computing élastiques sur deux aspects : structurel et comportemental.Du point de vue structurel, le but est de définir et de modéliser une structure correcte des systèmes Cloud du côté " backend ". Cette partie est supportée par les capacités de spécification fournies par le formalisme des Bigraphes, à savoir : le principe de "sorting" et de règles de construction permettant de définir les desiderata du concepteur. Concernant l'aspect comportemental, il s'agit de modéliser, valider et implémenter des stratégies génériques de mise à l'échelle automatique en vue de décrire les différents mécanismes d'auto-adaptation élastiques des systèmes cloud (mise à l'échelle horizontale, verticale, migration, etc.), en multi-couches (i.e., aux niveaux service et infrastructure). Ces tâches sont prises en charge par les aspects dynamiques propres aux Systèmes Réactifs Bigraphiques (BRS) notamment par le biais des règles de réaction.Les stratégies d'élasticité introduites visent à guider le déclenchement conditionnel des différentes règles de réaction définies, afin de décrire les comportements d'auto-adaptation des systèmes Cloud au niveau service et infrastructure. L'encodage de ces spécifications et leurs implémentations sont définis en logique de réécriture via le langage Maude. Leur bon fonctionnement est vérifié formellement à travers une technique de model-checking supportée par la logique temporelle linéaire LTL.Afin de valider ces contributions d'un point de vue quantitatif, nous proposons une approche à base de file d'attente pour analyser, évaluer et discuter les stratégies d'élasticité d'un système Cloud à travers différents scénarios simulés. Dans nos travaux, nous explorons la définition d'une "bonne" stratégie en prenant en compte une étude de cas qui repose sur la nature changeante de la charge de travail. Nous proposons une manière originale de composer plusieurs stratégies d'élasticité à plusieurs niveaux afin de garantir différentes politiques de haut-niveau. / Elasticity property allows Cloud systems to adapt to their incoming workload by provisioning and de-provisioning computing resources in an autonomic manner, as the demand rises and drops. Due to the unpredictable nature of the workload and the numerous factors that impact elasticity, providing accurate action plans to insure a Cloud system's elasticity while preserving high level policies (performance, costs, etc.) is a particularly challenging task. This thesis aims at providing a thorough specification and implementation of Cloud systems, by relying on bigraphs as a formal model, over two aspects: structural and behavioral.Structurally, the goal is to define a correct modeling of Cloud systems' "back-end" structure. This part is supported by the specification capabilities of Bigraph formalism. Specifically, via "sorting" mechanisms and construction rules that allow defining the designer's desiderata. As for the behavioral part, it consists of model, implement and validate generic elasticity strategies in order to describe Cloud systems' auto-adaptive behaviors (i.e., horizontal and vertical scaling, migration, etc.) in a cross-layer manner (i.e., at service and infrastructure levels). These tasks are supported by the dynamic aspects of Bigraphical Reactive Systems (BRS) formalism (through reaction rules).The introduced elasticity strategies aim at guiding the conditional triggering of the defined reaction rules, to describe Cloud systems' auto-scaling behaviors in a cross-layered manner. The encoding of these specifications and their implementation are defined in Rewrite Logic via Maude language. Their correctness is formally verified through a model-checking technique supported by the linear temporal logic LTL.In order to quantitatively validate these contributions, we propose a queuing-based approach in order to evaluate, analyze and discuss elasticity strategies in Cloud systems through different simulated execution scenarios. In this work, we explore the definition of a “good” strategy through a case study which considers the changing nature of the input workload. We propose an original way de compose different cross-layer elasticity strategies to guarantee different high-level policies.