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.

Digital Exhaustion in relation to Video Games – The Consumer Perspective

This thesis regards exhaustion of copyright’s distribution right in intangible transfers of video games. It analyses whether, under the current law of the European Union, the phenomenon of digital exhaustion, especially in relation to games exists. The thesis analyses the consumers’ position in the market for copyright protected goods. It uses video games market as an example of the wider phenomenon of the effect of latest technological developments on consumers. The research conducted for the thesis is mostly legal dogmatic, although also comparative analysis, law and economics and law and technology methods are utilised. The thesis evaluates the effects of the most recent case law of the European Court of Justice to analyse the current state of digital exhaustion. In the analysis of effects that the existence of digital exhaustion has, the thesis uses the consumers’ point of view. The thesis introduces the current state of technology in the field of video games from a legal perspective. Furthermore the thesis analyses the effects on consumers of a scenario that no digital exhaustion exists in the future. Such scenario under the recent European case law at the moment seems realistic. The conclusion of my research is most importantly that the consumer position in the market for digital goods has deteriorated and that the probable exclusion of the exhaustion for digital goods is another piece of evidence of this development. Most importantly however, the state of affairs where no certainty prevails on whether digital exhaustion exists, creates injustice from the consumers’ point of view. Accordingly, acts by EU legislators of the Court of Justice of the European Union are required to clarify the issue.

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.

Heat Demand Forecasting Models’ Development: Use of Data Mining Tools in SQL Server Analysis Services

This thesis introduces heat demand forecasting models which are generated by using data mining algorithms. The forecast spans one full day and this forecast can be used in regulating heat consumption of buildings. For training the data mining models, two years of heat consumption data from a case building and weather measurement data from Finnish Meteorological Institute are used. The thesis utilizes Microsoft SQL Server Analysis Services data mining tools in generating the data mining models and CRISP-DM process framework to implement the research. Results show that the built models can predict heat demand at best with mean average percentage errors of 3.8% for 24-h profile and 5.9% for full day. A deployment model for integrating the generated data mining models into an existing building energy management system is also discussed.

A software engineering approach to distributed systems for composite modeling

The goal of this thesis is to define and validate a software engineering approach for the development of a distributed system for the modeling of composite materials, based on the analysis of various existing software development methods. We reviewed the main features of: (1) software engineering methodologies; (2) distributed system characteristics and their effect on software development; (3) composite materials modeling activities and the requirements for the software development. Using the design science as a research methodology, the distributed system for creating models of composite materials is created and evaluated. Empirical experiments which we conducted showed good convergence of modeled and real processes. During the study, we paid attention to the matter of complexity and importance of distributed system and a deep understanding of modern software engineering methods and tools.

Distributed energy resources in an electricity retailer’s short-term profit optimization

Liberalization of electricity markets has resulted in a competed Nordic electricity market, in which electricity retailers play a key role as electricity suppliers, market intermediaries, and service providers. Although these roles may remain unchanged in the near future, the retailers’ operation may change fundamentally as a result of the emerging smart grid environment. Especially the increasing amount of distributed energy resources (DER), and improving opportunities for their control, are reshaping the operating environment of the retailers. This requires that the retailers’ operation models are developed to match the operating environment, in which the active use of DER plays a major role. Electricity retailers have a clientele, and they operate actively in the electricity markets, which makes them a natural market party to offer new services for end-users aiming at an efficient and market-based use of DER. From the retailer’s point of view, the active use of DER can provide means to adapt the operation to meet the challenges posed by the smart grid environment, and to pursue the ultimate objective of the retailer, which is to maximize the profit of operation. This doctoral dissertation introduces a methodology for the comprehensive use of DER in an electricity retailer’s short-term profit optimization that covers operation in a variety of marketplaces including day-ahead, intra-day, and reserve markets. The analysis results provide data of the key profit-making opportunities and the risks associated with different types of DER use. Therefore, the methodology may serve as an efficient tool for an experienced operator in the planning of the optimal market-based DER use. The key contributions of this doctoral dissertation lie in the analysis and development of the model that allows the retailer to benefit from profit-making opportunities brought by the use of DER in different marketplaces, but also to manage the major risks involved in the active use of DER. In addition, the dissertation introduces an analysis of the economic potential of DER control actions in different marketplaces including the day-ahead Elspot market, balancing power market, and the hourly market of Frequency Containment Reserve for Disturbances (FCR-D).

TEHOHOITAJIEN KIVUN ARVIOINNIN OSAAMINEN – Tehohoitopotilaille kehitetyn kivunarviointimittarin käytön oppiminen video-opetuksen avulla.

Tehohoitopotilaan kivun arvioiminen on usein haastavaa, johtuen potilaan kyvyttömyydestä kommunikoida. Kivun arvioinnin avuksi onkin tästä syystä kehitetty käyttäytymiseen perustuvia kipumittareita. Tehohoitajilla on keskeinen asema kivun arvioinnissa, mutta tutkimusten perusteella tehohoitajien kivun arvioinnin osaaminen on puutteellista niin tietojen kuin taitojen osalta ja heillä on ennakkoasenteita kivun arviointiin liittyen. Tehohoitajien kouluttaminen kivun arviointiin liittyen on tärkeä keino tehohoitopotilaan kivun arvioinnin edistämisessä. Koulutuksen tulee kuitenkin olla helposti saatavilla, ottaen huomioon hoitotodellisuuden siihen tuomat haasteet. Tutkimuksen tarkoituksena oli arvioida video-opetuksen vaikutusta tehohoitajien tietoihin ja taitoihin tehohoitopotilaalle kehitetyn Critical-Care Pain Observation Tool (CPOT)-kipumittarin käyttöön liittyen, sekä kuvailla tehohoitajien kokemuksia video-opetuksesta oppimismenetelmänä. Yhdeltä teho-osastolta 48 tehohoitajaa katsoi tutkimusta varten kehitetyn CPOT-opetusvideon, jonka jälkeen he arvioivat kahden potilaan kipua CPOT-kipumittarilla, tutkijan tehdessä samanaikaisesti rinnakkaisarvioinnit potilaista. Arviointien jälkeen tehohoitajat tekivät tietotestin ja täyttivät CPOT-arviointilomakkeen. Tehohoitajien CPOT-kipumittarin käyttötaitoja arvioitiin tarkastelemalla tehohoitajien ja tutkijan tekemien kivunarviointien yhdenmukaisuutta interrater reliabiliteettilaskelmin. Kaksikymmentä tehohoitajaa haastateltiin heidän kokemuksista oppimismenetelmään liittyen. Haastattelut analysoitiin deduktiivisella temaattisella analyysillä. Tehohoitajat oppivat CPOT-kipumittarin käytön periaatteet ja kokivat oppineensa mittarin käytön, mutta interrater reliabiliteetti suhteessa tutkijan tekemiin kivun arviointeihin oli keskinkertainen. Video-opetus koettiin positiivisena, vaikkakin vuorovaikutuksellisuutta kaivattiin. Tutkimus osoitti video-opetuksen olevan käyttökelpoinen oppimismenetelmä CPOT-kipumittarin käytön periaatteiden oppimiseen, mutta parempien käyttötaitojen saavuttaminen vaatii lisäharjoittelua. Koska tehohoitajien subjektiivinen arvio käyttötaidoista ei välttämättä vastaa todellisia käyttötaitoja, oleellista olisi varmistaa myös objektiivisesti mittarin käyttötaidot koulutuksen jälkeen. Jatkossa tulisi tutkia käytäntöön soveltuvia keinoja varmistaa mittarin käyttötaidot, sekä teho-osastojen oppimiskulttuuria ja tehohoitajien motivaatiota ja asenteita työhön liittyvään oppimiseen.