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.

Distributed Energy Production in the North-West Region of Russia

The energy system of Russia is the world's fourth largest measured by installed power. The largest are that of the the United States of America, China and Japan. After 1990, the electricity consumption decreased as a result of the Russian industry crisis. The vivid economic growth during the latest few years explains the new increase in the demand for energy resources within the State. In 2005 the consumption of electricity achieved the maximum level of 1990 and continues to growth. In the 1980's, the renewal of power facilities was already very slow and practically stopped in the 1990's. At present, the energy system can be very much characterized as outdated, inefficient and uneconomic because of the old equipment, non-effective structure and large losses in the transmission lines. The aim of Russia's energy reform, which was started in 2001, is to achieve a market based energy policy by 2011. This would thus remove the significantly state-controlled monopoly in Russia's energy policy. The reform will stimulateto decrease losses, improve the energy system and employ energy-saving technologies. The Russian energy system today is still based on the use of fossil fuels, and it almost totally ignores the efficient use of renewable sources such as wind, solar, small hydro and biomass, despite of their significant resources in Russia. The main target of this project is to consider opportunities to apply renewable energy production in the North-West Federal Region of Russia to partly solve the above mentioned problems in the energy system.

Protection of publicly distributed software components

The nature of client-server architecture implies that some modules are delivered to customers. These publicly distributed commercial software components are under risk, because users (and simultaneously potential malefactors) have physical access to some components of the distributed system. The problem becomes even worse if interpreted programming languages are used for creation of client side modules. The language Java, which was designed to be compiled into platform independent byte-code is not an exception and runs the additional risk. Along with advantages like verifying the code before execution (to ensure that program does not produce some illegal operations)Java has some disadvantages. On a stage of byte-code a java program still contains comments, line numbers and some other instructions, which can be used for reverse-engineering. This Master's thesis focuses on protection of Java code based client-server applications. I present a mixture of methods to protect software from tortious acts. Then I shall realize all the theoretical assumptions in a practice and examine their efficiency in examples of Java code. One of the criteria's to evaluate the system is that my product is used for specialized area of interactive television.

Global Distributed Delivery Model for Internet Service Provider

Globaalin talouden rakenteet muuttuvat jatkuvasti. Yritykset toimivat kansainvälisillä markkinoilla aiempaa enemmän. Tuotannon lisäämiseksi monet yritykset ovat ulkoistaneet tuotteidensa tuki- ja ylläpitotoiminnot halvan työvoiman maihin. Yritykset voivat tällöin keskittää toimintansa ydinosamiseensa. Vapautuneita resursseja voidaan käyttää yrityksen sisäisessä tuotekehityksessä ja panostaa seuraavan sukupolven tuotteiden ja teknologioiden kehittämiseen. Diplomityö esittelee Globaalisti hajautetun toimitusmallin Internet-palveluntarjoajalle jossa tuotteiden tuki- ja ylläpito on ulkoistettu Intiaan. Teoriaosassa esitellään erilaisia toimitusmalleja ja keskitytään erityisesti hajautettuun toimitusmalliin. Tämän lisäksi luetellaan valintakriteerejä joilla voidaan arvioida projektin soveltuvuutta ulkoistettavaksi sekä esitellään mahdollisuuksia ja uhkia jotka sisältyvät globaaliin ulkoistusprosessiin. Käytäntöosassa esitellään globaali palvelun toimittamisprosessi joka on kehitetty Internet-palveluntarjoajan tarpeisiin.

Data-parallel computation in parallel and distributed environments

The past few decades have seen a considerable increase in the number of parallel and distributed systems. With the development of more complex applications, the need for more powerful systems has emerged and various parallel and distributed environments have been designed and implemented. Each of the environments, including hardware and software, has unique strengths and weaknesses. There is no single parallel environment that can be identified as the best environment for all applications with respect to hardware and software properties. The main goal of this thesis is to provide a novel way of performing data-parallel computation in parallel and distributed environments by utilizing the best characteristics of difference aspects of parallel computing. For the purpose of this thesis, three aspects of parallel computing were identified and studied. First, three parallel environments (shared memory, distributed memory, and a network of workstations) are evaluated to quantify theirsuitability for different parallel applications. Due to the parallel and distributed nature of the environments, networks connecting the processors in these environments were investigated with respect to their performance characteristics. Second, scheduling algorithms are studied in order to make them more efficient and effective. A concept of application-specific information scheduling is introduced. The application- specific information is data about the workload extractedfrom an application, which is provided to a scheduling algorithm. Three scheduling algorithms are enhanced to utilize the application-specific information to further refine their scheduling properties. A more accurate description of the workload is especially important in cases where the workunits are heterogeneous and the parallel environment is heterogeneous and/or non-dedicated. The results obtained show that the additional information regarding the workload has a positive impact on the performance of applications. Third, a programming paradigm for networks of symmetric multiprocessor (SMP) workstations is introduced. The MPIT programming paradigm incorporates the Message Passing Interface (MPI) with threads to provide a methodology to write parallel applications that efficiently utilize the available resources and minimize the overhead. The MPIT allows for communication and computation to overlap by deploying a dedicated thread for communication. Furthermore, the programming paradigm implements an application-specific scheduling algorithm. The scheduling algorithm is executed by the communication thread. Thus, the scheduling does not affect the execution of the parallel application. Performance results achieved from the MPIT show that considerable improvements over conventional MPI applications are achieved.

Improving distributed simulation in a workstation environment

Technological development brings more and more complex systems to the consumer markets. The time required for bringing a new product to market is crucial for the competitive edge of a company. Simulation is used as a tool to model these products and their operation before actual live systems are built. The complexity of these systems can easily require large amounts of memory and computing power. Distributed simulation can be used to meet these demands. Distributed simulation has its problems. Diworse, a distributed simulation environment, was used in this study to analyze the different factors that affect the time required for the simulation of a system. Examples of these factors are the simulation algorithm, communication protocols, partitioning of the problem, distributionof the problem, capabilities of the computing and communications equipment and the external load. Offices offer vast amounts of unused capabilities in the formof idle workstations. The use of this computing power for distributed simulation requires the simulation to adapt to a changing load situation. This requires all or part of the simulation work to be removed from a workstation when the owner wishes to use the workstation again. If load balancing is not performed, the simulation suffers from the workstation's reduced performance, which also hampers the owner's work. Operation of load balancing in Diworse is studied and it is shown to perform better than no load balancing, as well as which different approaches for load balancing are discussed.

The role of trust and its evolution in distributed teams in a multinational organisation

Tutkimuksen päätavoitteena on ollut selvittää miten kansallinen ja organisaatiokulttuuri, niihin liittyvät normit ja arvot edesauttavat tai vaikeuttavat luottamuksen kehittymistä monikulttuurisissa tiimeissä maailmanlaajuisessa organisaatiossa. Tutkimuksen avulla haluttiin myös selvittää miten luottamus kehittyy hajautetuissa monikansallisissa tiimeissä WorldCom Internationalissa. Empiirinen tutkimusmenetelmä perustuu kvalitatiivisiin teemahaastatteluihin, jotka tehtiin WorldComin työntekijöille. Tutkimuksessa havaittiin, ettei yhteisten sosiaalisten normien merkitys luottamuksen syntymiselle ole niin merkittävä, koska WorldComin yhtenäiset toimintatavat sekä hallitseva amerikkalaisen emoyhtiön "kotikulttuuri" muodostavat yhtenäiset toimintalinjat tiimeissä. Tietokonevälitteisen kommunikoinnin jatkuva käyttö on edesauttanut työntekijöiden ns. sosiaalisen älyn kehittymistä, sillä henkilökohtaisen tapaamisen puuttuminen kehittää vastaavasti taitoja aistia ja tulkita sähköpostien tai puhelinneuvotteluiden aikana välittyviä vastapuolen "näkymättömiä" vihjeitä.

Building distributed high availability system

Today’s commercial web sites are under heavy user load and they are expected to be operational and available at all times. Distributed system architectures have been developed to provide a scalable and failure tolerant high availability platform for these web based services. The focus on this thesis was to specify and implement resilient and scalable locally distributed high availability system architecture for a web based service. Theory part concentrates on the fundamental characteristics of distributed systems and presents common scalable high availability server architectures that are used in web based services. In the practical part of the thesis the implemented new system architecture is explained. Practical part also includes two different test cases that were done to test the system's performance capacity.

Development a distributed simulation environment on a cluster of workstations

Simulation has traditionally been used for analyzing the behavior of complex real world problems. Even though only some features of the problems are considered, simulation time tends to become quite high even for common simulation problems. Parallel and distributed simulation is a viable technique for accelerating the simulations. The success of parallel simulation depends heavily on the combination of the simulation application, algorithm and message population in the simulation is sufficient, no additional delay is caused by this environment. In this thesis a conservative, parallel simulation algorithm is applied to the simulation of a cellular network application in a distributed workstation environment. This thesis presents a distributed simulation environment, Diworse, which is based on the use of networked workstations. The distributed environment is considered especially hard for conservative simulation algorithms due to the high cost of communication. In this thesis, however, the distributed environment is shown to be a viable alternative if the amount of communication is kept reasonable. Novel ideas of multiple message simulation and channel reduction enable efficient use of this environment for the simulation of a cellular network application. The distribution of the simulation is based on a modification of the well known Chandy-Misra deadlock avoidance algorithm with null messages. The basic Chandy Misra algorithm is modified by using the null message cancellation and multiple message simulation techniques. The modifications reduce the amount of null messages and the time required for their execution, thus reducing the simulation time required. The null message cancellation technique reduces the processing time of null messages as the arriving null message cancels other non processed null messages. The multiple message simulation forms groups of messages as it simulates several messages before it releases the new created messages. If the message population in the simulation is suffiecient, no additional delay is caused by this operation A new technique for considering the simulation application is also presented. The performance is improved by establishing a neighborhood for the simulation elements. The neighborhood concept is based on a channel reduction technique, where the properties of the application exclusively determine which connections are necessary when a certain accuracy for simulation results is required. Distributed simulation is also analyzed in order to find out the effect of the different elements in the implemented simulation environment. This analysis is performed by using critical path analysis. Critical path analysis allows determination of a lower bound for the simulation time. In this thesis critical times are computed for sequential and parallel traces. The analysis based on sequential traces reveals the parallel properties of the application whereas the analysis based on parallel traces reveals the properties of the environment and the distribution.

Integrating distributed generation and Smart Grids into single-family house

This study examines Smart Grids and distributed generation, which is connected to a single-family house. The distributed generation comprises small wind power plant and solar panels. The study is done from the consumer point of view and it is divided into two parts. The first part presents the theoretical part and the second part presents the research part. The theoretical part consists of the definition of distributed generation, wind power, solar energy and Smart Grids. The study examines what the Smart Grids will enable. New technology concerning Smart Grids is also examined. The research part introduces wind and sun conditions from two countries. The countries are Finland and Germany. According to the wind and sun conditions of these two countries, the annual electricity production from wind power plant and solar panels will be calculated. The costs of generating electricity from wind and solar energy are calculated from the results of annual electricity productions. The study will also deal with feed-in tariffs, which are supporting systems for renewable energy resources. It is examined in the study, if it is cost-effective for the consumers to use the produced electricity by themselves or sell it to the grid. Finally, figures for both countries are formed. The figures include the calculated cost of generating electricity from wind power plant and solar panels, retail and wholesale prices and feed-in tariffs. In Finland, it is not cost-effective to sell the produced electricity to the grid, before there are support systems. In Germany, it is cost-effective to sell the produced electricity from solar panels to the grid because of feed-in tariffs. On the other hand, in Germany it is cost-effective to produce electricity from wind to own use because the retail price is higher than the produced electricity from wind.

Sustainable Waste-to-Energy Production: Performance Evaluation of Distributed Generation fuelled by Landfill Gas

The environmental impact of landfill is a growing concern in waste management practices. Thus, assessing the effectiveness of the solutions implemented to alter the issue is of importance. The objectives of the study were to provide an insight of landfill advantages, and to consolidate landfill gas importance among others alternative fuels. Finally, a case study examining the performances of energy production from a land disposal at Ylivieska was carried out to ascertain the viability of waste to energy project. Both qualitative and quantitative methods were applied. The study was conducted in two parts; the first was the review of literatures focused on landfill gas developments. Specific considerations were the conception of mechanism governing the variability of gas production and the investigation of mathematical models often used in landfill gas modeling. Furthermore, the analysis of two main distributed generation technologies used to generate energy from landfill was carried out. The review of literature revealed a high influence of waste segregation and high level of moisture content for waste stabilization process. It was found that the enhancement in accuracy for forecasting gas rate generation can be done with both mathematical modeling and field test measurements. The result of the case study mainly indicated the close dependence of the power output with the landfill gas quality and the fuel inlet pressure.

Magnetic Resonance Experiments with Atomic Hydrogen

In this thesis three experiments with atomic hydrogen (H) at low temperatures T<1 K are presented. Experiments were carried out with two- (2D) and three-dimensional (3D) H gas, and with H atoms trapped in solid H2 matrix. The main focus of this work is on interatomic interactions, which have certain specific features in these three systems considered. A common feature is the very high density of atomic hydrogen, the systems are close to quantum degeneracy. Short range interactions in collisions between atoms are important in gaseous H. The system of H in H₂ differ dramatically because atoms remain fixed in the H₂ lattice and properties are governed by long-range interactions with the solid matrix and with H atoms. The main tools in our studies were the methods of magnetic resonance, with electron spin resonance (ESR) at 128 GHz being used as the principal detection method. For the first time in experiments with H in high magnetic fields and at low temperatures we combined ESR and NMR to perform electron-nuclear double resonance (ENDOR) as well as coherent two-photon spectroscopy. This allowed to distinguish between different types of interactions in the magnetic resonance spectra. Experiments with 2D H gas utilized the thermal compression method in homogeneous magnetic field, developed in our laboratory. In this work methods were developed for direct studies of 3D H at high density, and for creating high density samples of H in H₂. We measured magnetic resonance line shifts due to collisions in the 2D and 3D H gases. First we observed that the cold collision shift in 2D H gas composed of atoms in a single hyperfine state is much smaller than predicted by the mean-field theory. This motivated us to carry out similar experiments with 3D H. In 3D H the cold collision shift was found to be an order of magnitude smaller for atoms in a single hyperfine state than that for a mixture of atoms in two different hyperfine states. The collisional shifts were found to be in fair agreement with the theory, which takes into account symmetrization of the wave functions of the colliding atoms. The origin of the small shift in the 2D H composed of single hyperfine state atoms is not yet understood. The measurement of the shift in 3D H provides experimental determination for the difference of the scattering lengths of ground state atoms. The experiment with H atoms captured in H2 matrix at temperatures below 1 K originated from our work with H gas. We found out that samples of H in H2 were formed during recombination of gas phase H, enabling sample preparation at temperatures below 0.5 K. Alternatively, we created the samples by electron impact dissociation of H₂ molecules in situ in the solid. By the latter method we reached highest densities of H atoms reported so far, 3.5(5)x10¹⁹ cm^-3. The H atoms were found to be stable for weeks at temperatures below 0.5 K. The observation of dipolar interaction effects provides a verification for the density measurement. Our results point to two different sites for H atoms in H2 lattice. The steady-state nuclear polarizations of the atoms were found to be non-thermal. The possibility for further increase of the impurity H density is considered. At higher densities and lower temperatures it might be possible to observe phenomena related to quantum degeneracy in solid.

Distributed ControlArchitecture of Power Electronics Building-Block-Based Frequency Converters

The increasing power demand and emerging applications drive the design of electrical power converters into modularization. Despite the wide use of modularized power stage structures, the control schemes that are used are often traditional, in other words, centralized. The flexibility and re-usability of these controllers are typically poor. With a dedicated distributed control scheme, the flexibility and re-usability of the system parts, building blocks, can be increased. Only a few distributed control schemes have been introduced for this purpose, but their breakthrough has not yet taken place. A demand for the further development offlexible control schemes for building-block-based applications clearly exists. The control topology, communication, synchronization, and functionality allocationaspects of building-block-based converters are studied in this doctoral thesis. A distributed control scheme that can be easily adapted to building-block-based power converter designs is developed. The example applications are a parallel and series connection of building blocks. The building block that is used in the implementations of both the applications is a commercial off-the-shelf two-level three-phase frequency converter with a custom-designed controller card. The major challenge with the parallel connection of power stages is the synchronization of the building blocks. The effect of synchronization accuracy on the system performance is studied. The functionality allocation and control scheme design are challenging in the seriesconnected multilevel converters, mainly because of the large number of modules. Various multilevel modulation schemes are analyzed with respect to the implementation, and this information is used to develop a flexible control scheme for modular multilevel inverters.

Cluster structure of atomic nuclei

Kirjallisuusarvostelu

Atomic level phenomena on transition metal surfaces

In this study we discuss the atomic level phenomena on transition metal surfaces. Transition metals are widely used as catalysts in industry. Therefore, reactions occuring on transition metal surfaces have large industrial intrest. This study addresses problems in very small size and time scales, which is an important part in the overall understanding of these phenomena. The publications of this study can be roughly divided into two categories: The adsorption of an O2 molecule to a surface, and surface structures of preadsorbed atoms. These two categories complement each other, because in the realistic case there are always some preadsorbed atoms at the catalytically active surfaces. However, all transition metals have an active d-band, and this study is also a study of the in uence of the active d-band on other atoms. At the rst part of this study we discuss the adsorption and dissociation of an O2 molecule on a clean stepped palladium surface and a smooth palladium surface precovered with sulphur and oxygen atoms. We show how the reactivity of the surface against the oxygen molecule varies due to the geometry of the surface and preadsorbed atoms. We also show how the molecular orbitals of the oxygen molecule evolve when it approaches the di erent sites on the surface. In the second part we discuss the surface structures of transition metal surfaces. We study the structures that are intresting on account of the Rashba e ect and charge density waves. We also study the adsorption of suphur on a gold surface, and surface structures of it. In this study we use ab-initio based density functional theory methods to simulate the results. We also compare the results of our methods to the results obtained with the Low-Energy-Electron-Difraction method.