Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.

Embedded Service Bus for Internet of Things Interoperability

Internet of Things (IoT) technologies are developing rapidly, and therefore there exist several standards of interconnection protocols and platforms. The existence of heterogeneous protocols and platforms has become a critical challenge for IoT system developers. To mitigate this challenge, few alliances and organizations have taken the initiative to build a framework that helps to integrate application silos. Some of these frameworks focus only on a specific domain like home automation. However, the resource constraints in the large proportion of connected devices make it difficult to build an interoperable system using such frameworks. Therefore, a general purpose, lightweight interoperability framework that can be used for a range of devices is required. To tackle the heterogeneous nature, this work introduces an embedded, distributed and lightweight service bus, Lightweight IoT Service bus Architecture (LISA), which fits inside the network stack of a small real-time operating system for constrained nodes. LISA provides a uniform application programming interface for an IoT system on a range of devices with variable resource constraints. It hides platform and protocol variations underneath it, thus facilitating interoperability in IoT implementations. LISA is inspired by the Network on Terminal Architecture, a service centric open architecture by Nokia Research Center. Unlike many other interoperability frameworks, LISA is designed specifically for resource constrained nodes and it provides essential features of a service bus for easy service oriented architecture implementation. The presented architecture utilizes an intermediate computing layer, a Fog layer, between the small nodes and the cloud, thereby facilitating the federation of constrained nodes into subnetworks. As a result of a modular and distributed design, the part of LISA running in the Fog layer handles the heavy lifting to assist the lightweight portion of LISA inside the resource constrained nodes. Furthermore, LISA introduces a new networking paradigm, Node Centric Networking, to route messages across protocol boundaries to facilitate interoperability. This thesis presents a concept implementation of the architecture and creates a foundation for future extension towards a comprehensive interoperability framework for IoT.

Effect of genotype, finishing system, and sex on physiochemical characteristics of goat meat

Seventy-eight kids of both sexes and five genotypes were used: Alpine, ½ Boer + ½ Alpine (½ BA), ¾ Boer + ¼ Alpine, ½ Anglo-nubian + ½ Alpine and "tricross" (½ Anglo-nubian + ¼ Boer + ¼ Alpine) with initial average weight of 14.1 ± 2.5. The objective was to evaluate the effect of genotype, finishing system, and sex on the physiochemical characteristics of goat meat. Finishing systems were: ST1 - kid + dam in pasture and ST2 - weaned kid and feedlot. Kids in ST1 were kept in an area with Panicum maximum cv. Tanzania, and after grazing, water and mineral salt/mix were fed ad libitum to the animals. The animals in ST2 were confined in collective pens distributed according to genotypes and received diet with 16% CP and 73% TDN. The values of pH, a* (red content), Cooking Loss (CL), and Ether Extract (EE) percentage were influenced by genotype. Values for red content (a*) and L* (brightness), CL and percentages of moisture, protein, EE, and ash were influenced by the finishing system. Longissimus dorsi muscle from animals ½ BA exhibited better physiochemical characteristics. For greater tenderness and higher percentages of fat, consumers should choose female kid goat meat.

BotCloud Detection System

Leveraging cloud services, companies and organizations can significantly improve their efficiency, as well as building novel business opportunities. Cloud computing offers various advantages to companies while having some risks for them too. Advantages offered by service providers are mostly about efficiency and reliability while risks of cloud computing are mostly about security problems. Problems with security of the cloud still demand significant attention in order to tackle the potential problems. Security problems in the cloud as security problems in any area of computing, can not be fully tackled. However creating novel and new solutions can be used by service providers to mitigate the potential threats to a large extent. Looking at the security problem from a very high perspective, there are two focus directions. Security problems that threaten service user’s security and privacy are at one side. On the other hand, security problems that threaten service provider’s security and privacy are on the other side. Both kinds of threats should mostly be detected and mitigated by service providers. Looking a bit closer to the problem, mitigating security problems that target providers can protect both service provider and the user. However, the focus of research community mostly is to provide solutions to protect cloud users. A significant research effort has been put in protecting cloud tenants against external attacks. However, attacks that are originated from elastic, on-demand and legitimate cloud resources should still be considered seriously. The cloud-based botnet or botcloud is one of the prevalent cases of cloud resource misuses. Unfortunately, some of the cloud’s essential characteristics enable criminals to form reliable and low cost botclouds in a short time. In this paper, we present a system that helps to detect distributed infected Virtual Machines (VMs) acting as elements of botclouds. Based on a set of botnet related system level symptoms, our system groups VMs. Grouping VMs helps to separate infected VMs from others and narrows down the target group under inspection. Our system takes advantages of Virtual Machine Introspection (VMI) and data mining techniques.

Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.

Energy Management System for LVDC Island Networks

Recent developments in power electronics technology have made it possible to develop competitive and reliable low-voltage DC (LVDC) distribution networks. Further, islanded microgrids—isolated small-scale localized distribution networks— have been proposed to reliably supply power using distributed generations. However, islanded operations face many issues such as power quality, voltage regulation, network stability, and protection. In this thesis, an energy management system (EMS) that ensures efficient energy and power balancing and voltage regulation has been proposed for an LVDC island network utilizing solar panels for electricity production and lead-acid batteries for energy storage. The EMS uses the master/slave method with robust communication infrastructure to control the production, storage, and loads. The logical basis for the EMS operations has been established by proposing functionalities of the network components as well as by defining appropriate operation modes that encompass all situations. During loss-of-powersupply periods, load prioritizations and disconnections are employed to maintain the power supply to at least some loads. The proposed EMS ensures optimal energy balance in the network. A sizing method based on discrete-event simulations has also been proposed to obtain reliable capacities of the photovoltaic array and battery. In addition, an algorithm to determine the number of hours of electric power supply that can be guaranteed to the customers at any given location has been developed. The successful performances of all the proposed algorithms have been demonstrated by simulations.

Development of a Control System for a Tele Operated Mobile Robot

Mobile robots are capable of performing spatial displacement motions in different environments. This motions can be calculated based on sensorial data (autonomous robot) or given by an operator (tele operated robot). This thesis is focused on the latter providing the control architecture which bridges the tele operator and the robot’s locomotion system and end effectors. Such a task might prove overwhelming in cases where the robot comprises a wide variety of sensors and actuators hence a relatively new option was selected: Robot Operating System (ROS). The control system of a new robot will be sketched and tested in a simulation model using ROS together with Gazebo in order to determine the viability of such a system. The simulated model will be based on the projected shape and main features of the real machine. A stability analysis will be performed first theoretically and afterwards using the developed model. This thesis concluded that both the physical properties and the control architecture are feasible and stable settling up the ground for further work with the same robot.

Emerging markets and the international financial architecture: a blueprint for reform

If emerging markets are to achieve their objective of joining the ranks of industrialized, developed countries, they must use their economic and political influence to support radical change in the international financial system. This working paper recommends John Maynard Keynes's "clearing union" as a blueprint for reform of the international financial architecture that could address emerging market grievances more effectively than current approaches. Keynes's proposal for the postwar international system sought to remedy some of the same problems currently facing emerging market economies. It was based on the idea that financial stability was predicated on a balance between imports and exports over time, with any divergence from balance providing automatic financing of the debit countries by the creditor countries via a global clearinghouse or settlement system for trade and payments on current account. This eliminated national currency payments for imports and exports; countries received credits or debits in a notional unit of account fixed to national currency. Since the unit of account could not be traded, bought, or sold, it would not be an international reserve currency. The credits with the clearinghouse could only be used to offset debits by buying imports, and if not used for this purpose they would eventually be extinguished; hence the burden of adjustment would be shared equally - credit generated by surpluses would have to be used to buy imports from the countries with debit balances. Emerging market economies could improve upon current schemes for regionally governed financial institutions by using this proposal as a template for the creation of regional clearing unions using a notional unit of account.

A human-centric service approach for architecting and reengineering global system

Production of a new system in any range is expanding dramatically and new ideas are there upon introduced, the logic stands behind the matter is the growth of application of the internet and granting web-based systems. Before producing a system and distribute to the customer, various aspects should be studied which multiple the profit of the system. The process of productizing a new system from being unprocessed idea until delivers to the final user has been unambiguous. In this thesis, the systematize service in a way that benefits both the customer and provider, along with an effort to establish trust and diminish customer’s risk and increase service productivity are in detail presented. Characteristics of Servitization and Productization as two faces of one coin have been interpreted. Apart from the abovementioned issues state of art, service-oriented architecture (SOA) and New Service Development (NSD) has been included in this report for solving the problem of gradually decline in value of companies.

Implementation of hospital-wide computer information system :a case study of this change process

This case study examines the impact of a computer information system as it was being implemented in one Ontario hospital. The attitudes of a cross section of the hospital staff acted as a barometer to measure their perceptions of the implementation process. With The Mississauga Hospital in the early stages of an extensive computer implementation project, the opportunity existed to identify staff attitudes about the computer system, overall knowledge and compare the findings with the literature. The goal of the study was to develop a greater base about the affective domain in the relationship between people and the computer system. Eight exploratory questions shaped the focus of the investigation. Data were collected from three sources: a survey questionnaire, focused interviews, and internal hospital documents. Both quantitative and qualitative data were analyzed. Instrumentation in the study consisted of a survey distributed at two points in time to randomly selected hospital employees who represented all staff levels.Other sources of data included hospital documents, and twenty-five focused interviews with staff who replied to both surveys. Leavitt's socio-technical system, with its four subsystems: task, structure, technology, and people was used to classify staff responses to the research questions. The study findings revealed that the majority of respondents felt positive about using the computer as part of their jobs. No apparent correlations were found between sex, age, or staff group and feelings about using the computer. Differences in attitudes, and attitude changes were found in potential relationship to the element of time. Another difference was found in staff group and perception of being involved in the decision making process. These findings and other evidence about the role of change agents in this change process help to emphasize that planning change is one thing, managing the transition is another.

Enabling and Measuring Complexity in Evolving Designs using Generative Representations for Artificial Architecture

As the complexity of evolutionary design problems grow, so too must the quality of solutions scale to that complexity. In this research, we develop a genetic programming system with individuals encoded as tree-based generative representations to address scalability. This system is capable of multi-objective evaluation using a ranked sum scoring strategy. We examine Hornby's features and measures of modularity, reuse and hierarchy in evolutionary design problems. Experiments are carried out, using the system to generate three-dimensional forms, and analyses of feature characteristics such as modularity, reuse and hierarchy were performed. This work expands on that of Hornby's, by examining a new and more difficult problem domain. The results from these experiments show that individuals encoded with those three features performed best overall. It is also seen, that the measures of complexity conform to the results of Hornby. Moving forward with only this best performing encoding, the system was applied to the generation of three-dimensional external building architecture. One objective considered was passive solar performance, in which the system was challenged with generating forms that optimize exposure to the Sun. The results from these and other experiments satisfied the requirements. The system was shown to scale well to the architectural problems studied.

The cumate gene-switch: a system for regulated expression in mammalian cells

Affiliation: Sophie Broussau, Amelie Pilotte & Bernard Massie : Départment de microbiologie et immunologie, Faculté de médecine, Université de Montréal

L’archivage numérique des projets « Europan » comme situation d’analyse scientifique du concours d’idées en architecture

Il existe somme toute peu de théories du projet offrant une modélisation construite à partir de la complexité et de la diversité du projet d’architecture. Pourtant,certaines situations rassemblant parfois plusieurs dizaines de projets s’offrent d’elles-mêmes comme des situations comparatives et expérimentales : les concours d’architecture, d’urbanisme et de paysage. Le Laboratoire d’étude de l’architecture potentielle de l’Université de Montréal (Aménagement), après avoir développé un système d’archivage numérique des concours canadiens, a entrepris, avec le soutien du Groupement d’intérêt public « Europe des projets architecturaux et urbains », de développer la base de données documentaire des concours d’idées Europan. Au-delà des questions d’archivage numérique, se profilent clairement des possibilités de théorisation s’appuyant sur les logiques d’une base de données, en particulier sur la constitution du diagramme entités et relations, modélisation indispensable à sa traduction informatique. Cette recherche entreprend une première mise à jour de ces éléments conceptuels et tend à montrer que la base de données est un véritable modèle théorique du projet ouvrant sur de nouvelles avenues de recherche et de connaissance.

Significations et perceptions en architecture dans l’œuvre de Christian Norberg-Schulz

L’architecture au sens strict, qui renvoie à la construction, n’est pas indépendante des déterminations mentales, des images et des valeurs esthétiques, comme références, amenées par divers champs d’intérêt au problème du sens. Elle est, de par ce fait, un objet d’interprétation. Ce qu’on appelle communément « signification architecturale », est un univers vaste dans lequel sont constellées des constructions hypothétiques. En ce qui nous concerne, il s’agit non seulement de mouler la signification architecturale selon un cadre et des matières spécifiques de référence, mais aussi, de voir de près la relation de cette question avec l’attitude de perception de l’homme. Dans l’étude de la signification architecturale, on ne peut donc se détacher du problème de la perception. Au fond, notre travail montrera leur interaction, les moyens de sa mise en œuvre et ce qui est en jeu selon les pratiques théoriques qui la commandent. En posant la question de l’origine de l’acte de perception, qui n’est ni un simple acte de voir, ni un acte contemplatif, mais une forme d’interaction active avec la forme architecturale ou la forme d’art en général, on trouve dans les écrits de l’historien Christian Norberg-Schulz deux types de travaux, et donc deux types de réponses dont nous pouvons d’emblée souligner le caractère antinomique l’une par rapport à l’autre. C’est qu’il traite, dans le premier livre qu’il a écrit, Intentions in architecture (1962), connu dans sa version française sous le titre Système logique de l’architecture (1974, ci-après SLA), de l’expression architecturale et des modes de vie en société comme un continuum, défendant ainsi une approche culturelle de la question en jeu : la signification architecturale et ses temporalités. SLA désigne et représente un système théorique influencé, à bien des égards, par les travaux de l’épistémologie de Jean Piaget et par les contributions de la sémiotique au développement de l’étude de la signification architecturale. Le second type de réponse sur l’origine de l’acte de perception que formule Norberg-Schulz, basé sur sur les réflexions du philosophe Martin Heidegger, se rapporte à un terrain d’étude qui se situe à la dérive de la revendication du fondement social et culturel du langage architectural. Il lie, plus précisément, l’étude de la signification à l’étude de l’être. Reconnaissant ainsi la primauté, voire la prééminence, d’une recherche ontologique, qui consiste à soutenir les questionnements sur l’être en tant qu’être, il devrait amener avec régularité, à partir de son livre Existence, Space and Architecture (1971), des questions sur le fondement universel et historique de l’expression architecturale. Aux deux mouvements théoriques caractéristiques de ses écrits correspond le mouvement que prend la construction de notre thèse que nous séparons en deux parties. La première partie sera ainsi consacrée à l’étude de SLA avec l’objectif de déceler les ambiguïtés qui entourent le cadre de son élaboration et à montrer les types de legs que son auteur laisse à la théorie architecturale. Notre étude va montrer l’aspect controversé de ce livre, lié aux influences qu’exerce la pragmatique sur l’étude de la signification. Il s’agit dans cette première partie de présenter les modèles théoriques dont il débat et de les mettre en relation avec les différentes échelles qui y sont proposées pour l’étude du langage architectural, notamment avec l’échelle sociale. Celle-ci implique l’étude de la fonctionnalité de l’architecture et des moyens de recherche sur la typologie de la forme architecturale et sur sa schématisation. Notre approche critique de cet ouvrage prend le point de vue de la recherche historique chez Manfredo Tafuri. La seconde partie de notre thèse porte, elle, sur les fondements de l’intérêt chez Norberg-Schulz à partager avec Heidegger la question de l’Être qui contribuent à fonder une forme d’investigation existentielle sur la signification architecturale et du problème de la perception . L’éclairage de ces fondements exige, toutefois, de montrer l’enracinement de la question de l’Être dans l’essence de la pratique herméneutique chez Heidegger, mais aussi chez H. G. Gadamer, dont se réclame aussi directement Norberg-Schulz, et de dévoiler, par conséquent, la primauté établie de l’image comme champ permettant d’instaurer la question de l’Être au sein de la recherche architecturale. Sa recherche conséquente sur des valeurs esthétiques transculturelles a ainsi permis de réduire les échelles d’étude de la signification à l’unique échelle d’étude de l’Être. C’est en empruntant cette direction que Norberg-Schulz constitue, au fond, suivant Heidegger, une approche qui a pour tâche d’aborder l’« habiter » et le « bâtir » à titre de solutions au problème existentiel de l’Être. Notre étude révèle, cependant, une interaction entre la question de l’Être et la critique de la technique moderne par laquelle l’architecture est directement concernée, centrée sur son attrait le plus marquant : la reproductibilité des formes. Entre les écrits de Norberg-Schulz et les analyses spécifiques de Heidegger sur le problème de l’art, il existe un contexte de rupture avec le langage de la théorie qu’il s’agit pour nous de dégager et de ramener aux exigences du travail herméneutique, une approche que nous avons nous-même adoptée. Notre méthode est donc essentiellement qualitative. Elle s’inspire notamment des méthodes d’interprétation, de là aussi notre recours à un corpus constitué des travaux de Gilles Deleuze et de Jacques Derrida ainsi qu’à d’autres travaux associés à ce type d’analyse. Notre recherche demeure cependant attentive à des questions d’ordre épistémologique concernant la relation entre la discipline architecturale et les sciences qui se prêtent à l’étude du langage architectural. Notre thèse propose non seulement une compréhension approfondie des réflexions de Norberg-Schulz, mais aussi une démonstration de l’incompatibilité de la phénoménologie de Heidegger et des sciences du langage, notamment la sémiotique.

Une architecture parallèle distribuée et tolérante aux pannes pour le protocole interdomaine BGP au cœur de l’Internet

L’augmentation du nombre d’usagers de l’Internet a entraîné une croissance exponentielle dans les tables de routage. Cette taille prévoit l’atteinte d’un million de préfixes dans les prochaines années. De même, les routeurs au cœur de l’Internet peuvent facilement atteindre plusieurs centaines de connexions BGP simultanées avec des routeurs voisins. Dans une architecture classique des routeurs, le protocole BGP s’exécute comme une entité unique au sein du routeur. Cette architecture comporte deux inconvénients majeurs : l’extensibilité (scalabilité) et la fiabilité. D’un côté, la scalabilité de BGP est mesurable en termes de nombre de connexions et aussi par la taille maximale de la table de routage que l’interface de contrôle puisse supporter. De l’autre côté, la fiabilité est un sujet critique dans les routeurs au cœur de l’Internet. Si l’instance BGP s’arrête, toutes les connexions seront perdues et le nouvel état de la table de routage sera propagé tout au long de l’Internet dans un délai de convergence non trivial. Malgré la haute fiabilité des routeurs au cœur de l’Internet, leur résilience aux pannes est augmentée considérablement et celle-ci est implantée dans la majorité des cas via une redondance passive qui peut limiter la scalabilité du routeur. Dans cette thèse, on traite les deux inconvénients en proposant une nouvelle approche distribuée de BGP pour augmenter sa scalabilité ainsi que sa fiabilité sans changer la sémantique du protocole. L’architecture distribuée de BGP proposée dans la première contribution est faite pour satisfaire les deux contraintes : scalabilité et fiabilité. Ceci est accompli en exploitant adéquatement le parallélisme et la distribution des modules de BGP sur plusieurs cartes de contrôle. Dans cette contribution, les fonctionnalités de BGP sont divisées selon le paradigme « maître-esclave » et le RIB (Routing Information Base) est dupliqué sur plusieurs cartes de contrôle. Dans la deuxième contribution, on traite la tolérance aux pannes dans l’architecture élaborée dans la première contribution en proposant un mécanisme qui augmente la fiabilité. De plus, nous prouvons analytiquement dans cette contribution qu’en adoptant une telle architecture distribuée, la disponibilité de BGP sera augmentée considérablement versus une architecture monolithique. Dans la troisième contribution, on propose une méthode de partitionnement de la table de routage que nous avons appelé DRTP pour diviser la table de BGP sur plusieurs cartes de contrôle. Cette contribution vise à augmenter la scalabilité de la table de routage et la parallélisation de l’algorithme de recherche (Best Match Prefix) en partitionnant la table de routage sur plusieurs nœuds physiquement distribués.