Teknologiaohjelma DENSY -Hajautetun energiantuotannon tulevaisuusskenaariot ja vaikutukset liiketoimintamalleihin

Tutkimuksen tavoitteena oli selvittää miten hajautettu energiantuotanto ja siihen liittyvä liiketoiminta tulee muuttumaan tulevaisuudessaja mitä mahdollisuuksia se voisi tarjota suomalaiselle osaamiselle. Työssä käydään läpi lyhyesti hajautetun energiantuotannon teknologian nykytilaa ja tehdään teknis-taloudellista vertailua eri tuotantoteknologioiden välillä. Tämän jälkeenon muodostettu asiantuntijoiden ja aktoreiden kanssa liiketoimin-taympäristöskenaarioita, jotka kuvaavat tulevaisuuden muutossuuntia hajautetun energian-tuotannon liiketoiminnassa. Skenaarioistunnoissa löydettiin muutosta ajavat voimat ja pohdittiin niiden vaikutusta alan kehitykseen. Työn tuloksena määriteltiin skenaarioiden kehitystä vahvimmin ohjaaviksi tekijöiksi infrastruktuurin kehittyneisyys ja toisaalta myös yhteiskunnan ohjaustoimet. Niiden pohjalta luotiin lopulliset neljä skenaariota ja niille kaikille liiketoimintakuvaukset. Skenaarioiden avulla suomalaisen toimijan näkökulmasta arvioitiin houkuttelevimmiksi markkina-alueiksi EU-15, Venäjä, Intia ja Kiina. Moninaisista liiketoimintaa estävistä te-kijöistä huolimatta markkinoilta löytyi suuri potentiaali hajautetun energiantuotannon jär-jestelmille. Potentiaalisimmiksi teknologioiksi suomalaisten yritysten kannalta nähtiin puolestaan diesel- ja kaasumoottorit, tuulivoima, pienvesivoima sekä bioenergia. Yhdessä markkina- ja teknologiatutkimuksien sekä skenaariotyön avulla luotiin uusia liiketoimin-takonseptikuvauksia tulevaisuuden hajautetun energiantuotannon markkinoille suomalai-sen toimijan näkökulmasta.

STACK OVERWRITING ATTACKS AND DEFENCES IN UNIX ENVIRONMENT

Työn tarkoituksena on tutkia pinon ylikirjoitukseen perustuvien hyökkäysten toimintaa ja osoittaa kokeellisesti nykyisten suojaustekniikoiden olevan riittämättömiä. Tutkimus suoritetaan testaamalla miten valitut tietoturvatuotteet toimivat eri testitilanteissa. Testatut tuotteet ovat Openwall, PaX, Libsafe 2.0 ja Immunix 6.2. Testaus suoritetaan pääasiassa RedHat 7.0 ympäristössä testiohjelman avulla. Testeissä mitataan sekä tuotteiden kyky havaita hyökkäyksiä että niiden nopeusvaikutukset. Myös erityyppisten hyökkäysten ja niitä vastaan kehitettyjen metodien toimintaperiaatteet esitellään seikkaperäisesti ja havainnollistetaan yksinkertaistetuilla esimerkeillä. Esitellyt tekniikat sisältävät puskurin ylivuodot, laittomat muotoiluparametrit, loppumerkittömät merkkijonot ja taulukoiden ylivuodot. Testit osoittavat, etteivät valitut tuotteet estä kaikkia hyökkäyksiä, joten lopuksi perehdytään myös vahinkojen minimointiin onnistuneiden hyökkäysten varalta.

EPC-projektin hallinta ja johtaminen

Tämän diplomityön tavoitteena oli tutkia erään projektiliiketoimintaa harjoittavan yrityksen toimintajärjestelmää. Työn lähtökohtana oli yrityksen toimittamien projektien laajuuden nopea kasvu lähivuosien aikana. Työssä tutkittiin yrityksen nykyistä toimintajärjestelmää ja sen ohjeistusta nimen omaan EPC (engineering procurement construction) projekteissa. Toimintajärjestelmän ohjeistusta tutkittiin yrityksessä tehdyillä henkilöhaastatteluilla sekä vertaamalla olemassa olevia ohjeita ja kuvauksia projektin hallinnan ja johtamisen teorioihin. Teoriat, joihin yrityksen toimintajärjestelmää työssä verrattiin olivat Project Management Institute:n, Project Management Body of Knowledge ja International standard ISO 10006, Quality Management guidelines to quality in project management. Työn teoriaosassa käsiteltiin projektin hallintaa ja johtamista, projektin eri vaiheita, projektin organisointia ja ositusta sekä projektikulttuuria. Työn tuloksena luotiin käsitys siitä, mitä osaprosesseja EPC-projektin hallintaan ja johtamiseen kohdeyrityksessä liittyy. Prosesseja tutkimalla muodostettiin käsitys yrityksen toimintajärjestelmän ohjeistuksen tasosta ja esitettiin tältä pohjalta mahdollisuuksia toimintajärjestelmän kehittämiseksi. Yhtenä työn keskeisimmistä tuloksista esitettiin EPC-projektin projektikuvaus.

Myynnin raportoinnin kehittäminen kassajärjestelmähankkeen yhteydessä

Raportointi liittyy kiinteänä osana yrityksen jokapäiväiseen toimintaan. Raportoinnin sisältö ja muoto vaihtelevat organisaatiotasosta riippuen päivittäisen toiminnan tarkkailusta kuukausittaiseen tulosraportointiin. Raportointi voidaan toteuttaa operatiivisten järjestelmien kautta tai nykyisin entistä suositumpana vaihtoehtona on keskitetty raportointi. Uuden raportointijärjestelmän hankintaprojekti on usein koko yritystä koskeva investointi. Jos raportointijärjestelmällä on tarkoitus raportoida sekä operatiivista toimintaa että johdon tarpeita, on sen mukauduttava moneen tarkoitukseen. Aluksi on tärkeää määritellä tietotarpeet ja tavoitteet projektille unohtamatta riskien- ja projektinhallintaa sekä investointilaskelmia. Jos raportoidaan myös yrityksen ulkopuolelle, tulee ottaa huomioon mahdolliset säädökset sekä tietoturvallisuusnäkökulmat. Myös yrityksen toimintatapoja ja – prosesseja on syytä tarkastella kriittisesti ennen järjestelmähankintaa jolloin voidaan havaita uusia raportointikohteita, tai toimintatapoja voidaan uudelleen organisoida parhaan toimintatavan saavuttamiseksi. Raportointijärjestelmää hankittaessa turvaudutaan usein ulkopuoliseen ohjelmistotoimittajaan, joka integroi ja räätälöi järjestelmän yrityksen omiin tarpeisiin soveltuvaksi. Raportointijärjestelmän hankintaprojekti ei lopu käyttöönottoon vaan projektin alussa on huomioitava myös järjestelmän huomattavasti pisin elinkaari eli käyttö ja ylläpito. Raportointi-, kuten ei moni muukaan tietojärjestelmä, ole ikinä valmis sillä tarpeet ja toimintatavat muuttuvat ajan kuluessa ja käyttäjien tietoisuus lisääntyy.

Monialustaiset avoimen lähdekoodin ikkunointikirjastot

Tämän tutkimuksen tavoitteena oli löytää vastauksia siihen, mikä on tärkeimpien avoimen lähdekoodin kirjastojen toteutuksen tämän hetkinen taso. Työssä tutkittiin WxWidgetsin, GTK+:n ja Qt:n toteutuksen tasoa käytämällä hyväksi McCaben, Henry&Kafuran ja Chidamberin & Kemererin esittelemiä staattisia menetelmiä. Lisäksi ikkunointikirjastojen lähdekoodin käännetty koko mitattiin eri käyttöjärjestelmissä. Tutkimuksessa esitellään valittujen kirjastojen arkkitehtuuri ja vertaillaan esiteltävien kirjastojen arkkitehtuurisia ratkaisuja toisiinsa. Tämän jälkeen arvioidaan staattisten menetelmien tuottamien tuloksien merkitystä kahdesta näkökulmasta: mitä tulokset kertovat kirjastoista kun niitä verrataan toisiinsa ja mitä silloin kun niitä verrataan kyseisen kirjaston ja muiden kirjastojen arkkitehtuurisiin ratkaisuihin. Tutkimuksessa havaittiin Qt:n sisältävän kaikkein vähiten kirjaston ulkopuolisia riippuvuuksia. Tämän lisäksi sen huomattiin sisältävän muista kirjastoista puuttuvia ominaisuuksia. Osittain edellämainitusta syystä johtuen Qt:n ongelmakohdaksi havaittiin joidenkin sen osien suuri monimutkaisuus ja tästä seuraava mahdollinen vaikeasti ylläpidettävä lähdekoodi. GTK+:n lähdekoodi sisältää muita kirjastoja vähemmän sisäisiä riippuvuuksia samaan kirjastoon, on korkeammalla abstraktiotasolla ja kirjaston osat ovat siirrettävissä ja erotettavissa toisistaan. Joissakin kohdissa GTK+:n ja etenkin sen C++-rajapinnan GTKmm:n lähdekoodi on kuitenkin tarpeettoman monimutkaista. WxWidgetsin toteutuksen havaittiin Qt:n tavoin olevan hyvin itsenäinen kokonaisuus, WxWidgetsin lähdekoodin monimutkaisuus on useimmiten jotakin GTK+:n ja Qt:n väliltä. WxWidgets on Qt:a vähemmän itsenäinen mutta kuitenkin itsenäisempi kuin GTK+. Kuten muutkin kirjastot myös wxWidgetsillä on omat kohtansa, joissa sen lähdekoodi on tarpeettoman monimutkaista.

Quality and analysis of administration processes in server operations

IT outsourcing refers to the way companies focus on their core competencies and buy the supporting functions from other companies specialized in that area. Service is the total outcome of numerous of activities by employees and other resources to provide solutions to customers' problems. Outsourcing and service business have their unique characteristics. Service Level Agreements quantify the minimum acceptable service to the user. The service quality has to be objectively quantified so that its achievement or non-achievement of it can be monitored. Usually offshoring refers to the transferring of tasks to low-cost nations. Offshoring presents a lot of challenges that require special attention and they need to be assessed thoroughly. IT Infrastructure management refers to installation and basic usability assistance of operating systems, network and server tools and utilities. ITIL defines the industry best practices for organizing IT processes. This thesis did an analysis of server operations service and the customers’ perception of the quality of daily operations. The agreed workflows and processes should be followed better. Service providers’ processes are thoroughly defined but both the customer and the service provider might disobey them. Service provider should review the workflows regarding customer functions. Customer facing functions require persistent skill development, as they communicate the quality to the customer. Service provider needs to provide better organized communication and knowledge exchange methods between the specialists in different geographical locations.

Järjestelmien siirtäminen uuteen käyttöjärjestelmäympäristöön

Käyttöjärjestelmän uuden version myötä vanhat ohjelmat eivät välttämättä toimi uudessa ympäristössä. Windows-käyttöjärjestelmässä sovellusten yhteensopivuus on aiemmin säilytetty melko hyvin. Uusimpiin Windows Vista ja Windows 7 -versioihin on tehty paljon tietoturvauudistuksia. Niistä johtuen vanhojen ohjelmien yhteensopivuutta on karsittu. Tässä työssä kuvataan automaatiojärjestelmän ohjelmakomponenttien siirtoa uuteen Windows-ympäristöön. Tavoitteena on saada tehtyä ohjeita muille automaatiojärjestelmän kehittäjille. Myös Windowsin tietoturvaominaisuuksiin tehdään katsaus, erityisesti pääsynhallintaan

Värispekrien eron laskenta

Olemassa olevat spektrieromittarit eivät vastaa riittävästi CIEDE2000-värieroa. Tämän työn tavoitteena oli toteuttaa menetelmä, joka laskee värispektrien eron siten, että tulos vastaa CIEDE2000-värieroa. Kehitystyön tuloksena syntyi menetelmä, joka perustuu ennalta laskettuihin eroihin tunnettujen spektrien välillä ja niiden perusteella johdettuihin laskentaparametreihin. menetelmällä pystyy laskemaan spektrieroja vain niiden spektrien välillä, jotka saadaan sekoittamalla tunnettuja spektrejä. Laskentaparametrien laskenta on työläs prosessi ja siksi menetelmään toteutettiin hajautus usealle tietokoneelle. Menetelmä saatiin vastaamaan hyvin CIEDE2000:ia suurimmalle osalle spektrejä harvoja poikkeuksia lukuunottamatta. Ongelmat johtuvat mallissa olevasta matemaattisesta ominaisuudesta. Spektrieromittari näyttää metameerisille spektreille nollasta poikkeavan arvon, vaikka CIEDE2000 näyttää nollaa. Tämä osoittaa spektrieromittarin oikeamman toiminnan CIEDE2000-värieroon verrattuna.

Drivers and barriers of mobile travel and tourism service adoption : a study of individual perceptions and business model development in a travel and tourism context

The Travel and Tourism field is undergoing changes due to the rapid development of information technology and digital services. Online travel has profoundly changed the way travel and tourism organizations interact with their customers. Mobile technology such as mobile services for pocket devices (e.g. mobile phones) has the potential to take this development even further. Nevertheless, many issues have been highlighted since the early days of mobile services development (e.g. the lack of relevance, ease of use of many services). However, the wide adoption of smartphones and the mobile Internet in many countries as well as the formation of so-called ecosystems between vendors of mobile technology indicate that many of these issues have been overcome. Also when looking at the numbers of downloaded applications related to travel in application stores like Google Play, it seems obvious that mobile travel and tourism services are adopted and used by many individuals. However, as business is expected to start booming in the mobile era, many issues have a tendency to be overlooked. Travelers are generally on the go and thus services that work effectively in mobile settings (e.g. during a trip) are essential. Hence, the individuals’ perceived drivers and barriers to use mobile travel and tourism services in on-site or during trip settings seem particularly valuable to understand; thus this is one primary aim of the thesis. We are, however, also interested in understanding different types of mobile travel service users. Individuals may indeed be very different in their propensity to adopt and use technology based innovations (services). Research is also switching more from investigating issues of mobile service development to understanding individuals’ usage patterns of mobile services. But designing new mobile services may be a complex matter from a service provider perspective. Hence, our secondary aim is to provide insights into drivers and barriers of mobile travel and tourism service development from a holistic business model perspective. To accomplish the research objectives seven different studies have been conducted over a time period from 2002 – 2013. The studies are founded on and contribute to theories within diffusion of innovations, technology acceptance, value creation, user experience and business model development. Several different research methods are utilized: surveys, field and laboratory experiments and action research. The findings suggest that a successful mobile travel and tourism service is a service which supports one or several mobile motives (needs) of individuals such as spontaneous needs, time-critical arrangements, efficiency ambitions, mobility related needs (location features) and entertainment needs. The service could be customized to support travelers’ style of traveling (e.g. organized travel or independent travel) and should be easy to use, especially easy to take into use (access, install and learn) during a trip, without causing security concerns and/or financial risks for the user. In fact, the findings suggest that the most prominent barrier to the use of mobile travel and tourism services during a trip is an individual’s perceived financial cost (entry costs and usage costs). It should, however, be noted that regulations are put in place in the EU regarding data roaming prices between European countries and national telecom operators are starting to see ‘international data subscriptions’ as a sales advantage (e.g. Finnish Sonera provides a data subscription in the Baltic and Nordic region at the same price as in Finland), which will enhance the adoption of mobile travel and tourism services also in international contexts. In order to speed up the adoption rate travel service providers could consider e.g. more local initiatives of free Wi-Fi networks, development of services that can be used, at least to some extent, in an offline mode (do not require costly network access during a trip) and cooperation with telecom operators (e.g. lower usage costs for travelers who use specific mobile services or travel with specific vendors). Furthermore, based on a developed framework for user experience of mobile trip arrangements, the results show that a well-designed mobile site and/or native application, which preferably supports integration with other mobile services, is a must for true mobile presence. In fact, travel service providers who want to build a relationship with their customers need to consider a downloadable native application, but in order to be found through the mobile channel and make contact with potential new customers, a mobile website should be available. Moreover, we have made a first attempt with cluster analysis to identify user categories of mobile services in a travel and tourism context. The following four categories were identified: info-seekers, checkers, bookers and all-rounders. For example “all-rounders”, represented primarily by individuals who use their pocket device for almost any of the investigated mobile travel services, constituted primarily of 23 to 50 year old males with high travel frequency and great online experience. The results also indicate that travel service providers will increasingly become multi-channel providers. To manage multiple online channels, closely integrated and hybrid online platforms for different devices, supporting all steps in a traveler process should be considered. It could be useful for travel service providers to focus more on developing browser-based mobile services (HTML5-solutions) than native applications that work only with specific operating systems and for specific devices. Based on an action research study and utilizing a holistic business model framework called STOF we found that HTML5 as an emerging platform, at least for now, has some limitations regarding the development of the user experience and monetizing the application. In fact, a native application store (e.g. Google Play) may be a key mediator in the adoption of mobile travel and tourism services both from a traveler and a service provider perspective. Moreover, it must be remembered that many device and mobile operating system developers want service providers to specifically create services for their platforms and see native applications as a strategic advantage to sell more devices of a certain kind. The mobile telecom industry has moved into a battle of ecosystems where device makers, developers of operating systems and service developers are to some extent forced to choose their development platforms.

Avoimet tuotealustat ja allianssit älytelevisiomarkkinoilla

Älytelevisiomarkkinat ovat nykyisellään pirstaloituneet eri valmistajien kehittäessä omia älytelevisioalustoitaan, mikä tekee sovelluskehittämisestä erittäin työlästä, kun kehitystyö pitää tehdä jokaiselle alustalle erikseen. LG:n ja Philipsin perustama Smart TV Alliance pyrkii yksinkertaistamaan sovelluskehittäjien työtä, samalla houkutellen lisää kehittäjiä alalle. Työssä tutustutaan tuotealustoihin, avoimeen ja suljettuun innovaatioon, sekä alliansseihin. Lisäksi perehdytään älytelevisioihin sekä tietenkin itse Smart TV Allianceen. Lisäksi tarkastellaan nykyistä markkina-asetelmaa ja arvioidaan yksittäisten toimijoiden tilannetta ja mahdollisia toimenpiteitä. Työn painopiste on fyysisen laitevalmistajan ja käyttöjärjestelmän kehittäjän/ylläpitäjän näkökulmasta. Työn kannalta tärkeässä roolissa ovat ohjelmistopohjaiset tuotealustat. Eritoten työssä käsitellään älytelevisioiden ohjelmistoa tuotealustana, mutta hyvä vaihtoehtoinen ja eritoten monille käytännönläheisempi esimerkki on tietokoneen käyttöjärjestelmä, kuten Microsoft Windows tai useat Linux-pohjaiset käyttöjärjestelmät. Keskeisenä ominaisuutena näissä kaikissa on, että itse käyttöjärjestelmä toimii yhteisenä pohjana, jonka päälle voidaan rakentaa muuta toiminnallisuutta, kuten pelejä ja toimistosovelluksia.

Production planning and optimization of a pulp mill: introduction of the optimisation based scheduling software for pulp industry

The objective of this project was to introduce a new software product to pulp industry, a new market for case company. An optimization based scheduling tool has been developed to allow pulp operations to better control their production processes and improve both production efficiency and stability. Both the work here and earlier research indicates that there is a potential for savings around 1-5%. All the supporting data is available today coming from distributed control systems, data historians and other existing sources. The pulp mill model together with the scheduler, allows what-if analyses of the impacts and timely feasibility of various external actions such as planned maintenance of any particular mill operation. The visibility gained from the model proves also to be a real benefit. The aim is to satisfy demand and gain extra profit, while achieving the required customer service level. Research effort has been put both in understanding the minimum features needed to satisfy the scheduling requirements in the industry and the overall existence of the market. A qualitative study was constructed to both identify competitive situation and the requirements vs. gaps on the market. It becomes clear that there is no such system on the marketplace today and also that there is room to improve target market overall process efficiency through such planning tool. This thesis also provides better overall understanding of the different processes in this particular industry for the case company.

Energy Consumption of Applications on Mobile Phones

Battery consumption in mobile applications development is a very important aspect and has to be considered by all the developers in their applications. This study will present an analysis of different relevant concepts and parameters that may have impact on energy consumption of Windows Phone applications. This operating system was chosen because there is limited research even though there are related studies for Android an iOS operating systems. Furthermore, another reason is the increasing number of Windows Phone users. The objective of this research is to categorise the energy consumption parameters (e.g. use of one thread or several thread for the same output). The result for each group of experiment will be analyzed and a rule will be derived. The set of derived rules will serve as a guide for developers who intend to develop energy efficient Windows Phone applications. For each experiment, one application is created for each concept and the results are presented in two ways: a table and a chart. The table presents the duration of the experiment, the battery consumed by the experiment, the expected battery lifetime and the energy consumption, while the charts display the energy distribution based on the main threads: UI thread, application thread and network thread.

Enhancing Security of Linux OS against Administrators

Inside cyber security threats by system administrators are some of the main concerns of organizations about the security of systems. Since operating systems are controlled and managed by fully trusted administrators, they can negligently or intentionally break the information security and privacy of users and threaten the system integrity. In this thesis, we propose some solutions for enhancing the security of Linux OS by restricting administrators’ access to superuser’s privileges while they can still manage the system. We designed and implemented an interface for administrators in Linux OS called Linux Admins’ User Interface (LAUI) for managing the system in secure ways. LAUI along with other security programs in Linux like sudo protect confidentiality and integrity of users’ data and provide a more secure system against administrators’ mismanagement. In our model, we limit administrators to perform managing tasks in secure manners and also make administrators accountable for their acts. In this thesis we present some scenarios for compromising users’ data and breaking system integrity by system administrators in Linux OS. Then we evaluate how our solutions and methods can secure the system against these administrators’ mismanagement.

Agent-based management systems for many-core platforms : rigorous design and efficient implementation

Due to various advantages such as flexibility, scalability and updatability, software intensive systems are increasingly embedded in everyday life. The constantly growing number of functions executed by these systems requires a high level of performance from the underlying platform. The main approach to incrementing performance has been the increase of operating frequency of a chip. However, this has led to the problem of power dissipation, which has shifted the focus of research to parallel and distributed computing. Parallel many-core platforms can provide the required level of computational power along with low power consumption. On the one hand, this enables parallel execution of highly intensive applications. With their computational power, these platforms are likely to be used in various application domains: from home use electronics (e.g., video processing) to complex critical control systems. On the other hand, the utilization of the resources has to be efficient in terms of performance and power consumption. However, the high level of on-chip integration results in the increase of the probability of various faults and creation of hotspots leading to thermal problems. Additionally, radiation, which is frequent in space but becomes an issue also at the ground level, can cause transient faults. This can eventually induce a faulty execution of applications. Therefore, it is crucial to develop methods that enable efficient as well as resilient execution of applications. The main objective of the thesis is to propose an approach to design agentbased systems for many-core platforms in a rigorous manner. When designing such a system, we explore and integrate various dynamic reconfiguration mechanisms into agents functionality. The use of these mechanisms enhances resilience of the underlying platform whilst maintaining performance at an acceptable level. The design of the system proceeds according to a formal refinement approach which allows us to ensure correct behaviour of the system with respect to postulated properties. To enable analysis of the proposed system in terms of area overhead as well as performance, we explore an approach, where the developed rigorous models are transformed into a high-level implementation language. Specifically, we investigate methods for deriving fault-free implementations from these models into, e.g., a hardware description language, namely VHDL.

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.