Methods for construction and analysis of computational models in systems biology : applications to the modelling of the heat shock response and the self-assembly of intermediate filaments

Systems biology is a new, emerging and rapidly developing, multidisciplinary research field that aims to study biochemical and biological systems from a holistic perspective, with the goal of providing a comprehensive, system- level understanding of cellular behaviour. In this way, it addresses one of the greatest challenges faced by contemporary biology, which is to compre- hend the function of complex biological systems. Systems biology combines various methods that originate from scientific disciplines such as molecu- lar biology, chemistry, engineering sciences, mathematics, computer science and systems theory. Systems biology, unlike “traditional” biology, focuses on high-level concepts such as: network, component, robustness, efficiency, control, regulation, hierarchical design, synchronization, concurrency, and many others. The very terminology of systems biology is “foreign” to “tra- ditional” biology, marks its drastic shift in the research paradigm and it indicates close linkage of systems biology to computer science. One of the basic tools utilized in systems biology is the mathematical modelling of life processes tightly linked to experimental practice. The stud- ies contained in this thesis revolve around a number of challenges commonly encountered in the computational modelling in systems biology. The re- search comprises of the development and application of a broad range of methods originating in the fields of computer science and mathematics for construction and analysis of computational models in systems biology. In particular, the performed research is setup in the context of two biolog- ical phenomena chosen as modelling case studies: 1) the eukaryotic heat shock response and 2) the in vitro self-assembly of intermediate filaments, one of the main constituents of the cytoskeleton. The range of presented approaches spans from heuristic, through numerical and statistical to ana- lytical methods applied in the effort to formally describe and analyse the two biological processes. We notice however, that although applied to cer- tain case studies, the presented methods are not limited to them and can be utilized in the analysis of other biological mechanisms as well as com- plex systems in general. The full range of developed and applied modelling techniques as well as model analysis methodologies constitutes a rich mod- elling framework. Moreover, the presentation of the developed methods, their application to the two case studies and the discussions concerning their potentials and limitations point to the difficulties and challenges one encounters in computational modelling of biological systems. The problems of model identifiability, model comparison, model refinement, model inte- gration and extension, choice of the proper modelling framework and level of abstraction, or the choice of the proper scope of the model run through this thesis.

On the impact of rigorous approaches on the quality of development

Software systems are expanding and becoming increasingly present in everyday activities. The constantly evolving society demands that they deliver more functionality, are easy to use and work as expected. All these challenges increase the size and complexity of a system. People may not be aware of a presence of a software system, until it malfunctions or even fails to perform. The concept of being able to depend on the software is particularly significant when it comes to the critical systems. At this point quality of a system is regarded as an essential issue, since any deficiencies may lead to considerable money loss or life endangerment. Traditional development methods may not ensure a sufficiently high level of quality. Formal methods, on the other hand, allow us to achieve a high level of rigour and can be applied to develop a complete system or only a critical part of it. Such techniques, applied during system development starting at early design stages, increase the likelihood of obtaining a system that works as required. However, formal methods are sometimes considered difficult to utilise in traditional developments. Therefore, it is important to make them more accessible and reduce the gap between the formal and traditional development methods. This thesis explores the usability of rigorous approaches by giving an insight into formal designs with the use of graphical notation. The understandability of formal modelling is increased due to a compact representation of the development and related design decisions. The central objective of the thesis is to investigate the impact that rigorous approaches have on quality of developments. This means that it is necessary to establish certain techniques for evaluation of rigorous developments. Since we are studying various development settings and methods, specific measurement plans and a set of metrics need to be created for each setting. Our goal is to provide methods for collecting data and record evidence of the applicability of rigorous approaches. This would support the organisations in making decisions about integration of formal methods into their development processes. It is important to control the software development, especially in its initial stages. Therefore, we focus on the specification and modelling phases, as well as related artefacts, e.g. models. These have significant influence on the quality of a final system. Since application of formal methods may increase the complexity of a system, it may impact its maintainability, and thus quality. Our goal is to leverage quality of a system via metrics and measurements, as well as generic refinement patterns, which are applied to a model and a specification. We argue that they can facilitate the process of creating software systems, by e.g. controlling complexity and providing the modelling guidelines. Moreover, we find them as additional mechanisms for quality control and improvement, also for rigorous approaches. The main contribution of this thesis is to provide the metrics and measurements that help in assessing the impact of rigorous approaches on developments. We establish the techniques for the evaluation of certain aspects of quality, which are based on structural, syntactical and process related characteristics of an early-stage development artefacts, i.e. specifications and models. The presented approaches are applied to various case studies. The results of the investigation are juxtaposed with the perception of domain experts. It is our aspiration to promote measurements as an indispensable part of quality control process and a strategy towards the quality improvement.

Siirtohinnoitteluperiaatteet johtamisen apuvälineenä: case-tutkimus

Tämä tutkimus tarkastelee siirtohinnoittelun periaatteita ja sen taustalla vaikuttavia tekijöitä. Tutkielman tavoitteena on tutkia kohdeyrityksen nykyistä siirtohinnoittelua ja laatia sille periaatteet sen yksiköiden väliselle sisäiselle kaupalle. Tarkoituksena on kehittää siirtohinnoitteluperiaatteet, jotka auttavat johtoa liiketoiminnan eteenpäin viemisessä niin, että nuo periaatteet ovat samalla oikeudenmukaiset kohdeyrityksen eri osapuolille. Tutkimus on luonteeltaan kvalitatiivinen, teoreettinen ja kuvaileva case-tutkimus. Se tuo esille teoriaosuudessa eri siirtohinnoitteluvaihtoehtoja ja pohtii analyyttisesti niiden hyötyjä ja haittoja. Teoriaosuus perustuu kattavalle kirjallisuudelle, jonka avulla otetaan huomioon tekijöitä, jotka vaikuttavat siirtohinnoitteluprosessin taustalla. Tutkielman empiirinen aineisto kerättiin haastattelemalla kohdeyrityksen ylintä johtoa. Haastatteluiden rakenne oli luonteeltaan puolistrukturoitu. Lisäksi käytiin aiheeseen liittyvää keskustelua useaan otteeseen kohde-yrityksen talouspäällikön kanssa sekä tehtiin tutustumiskäynti erääseen osuuskuntaan, jossa kohdeyritys on osakkaana. Vierailu perustui osuuskunnan talouspäällikön pitämään esitykseen ja sen aikana käytyyn keskusteluun. Haastattelut tehtiin kevään 2012 aikana. Tutkimuksen perusteella siirtohinnoittelu on monimutkainen prosessi, jossa samanaikaisesti ei voida saavuttaa kaikkia siltä vaadittuja tavoitteita. Siirtohinnoitteluperiaatteita laadittaessa tulee ottaa etenkin huomioon 1) organisaation liiketoiminnan luonne 2) yksiköiden luonne, 3) vaihdettavien tuotteiden luonne, 4) erilaisten hintojen saatavuus sekä 5) suorituskyvyn mittaus ja arviointi. Tämä tutkimus suosittelee kohdeyrityksen tulos-yksiköille yleisesti mukautetun markkinaperusteisen siirtohinnoittelu-vaihtoehdon käyttöönottoa. Jalostustoimintaa vaativien tuotteiden sisäiselle kaupalle tutkimus suosittelee kustannusperusteisen vaihtoehdon noudattamista.

Scheduling of guarded command based models

Formal methods provide a means of reasoning about computer programs in order to prove correctness criteria. One subtype of formal methods is based on the weakest precondition predicate transformer semantics and uses guarded commands as the basic modelling construct. Examples of such formalisms are Action Systems and Event-B. Guarded commands can intuitively be understood as actions that may be triggered when an associated guard condition holds. Guarded commands whose guards hold are nondeterministically chosen for execution, but no further control flow is present by default. Such a modelling approach is convenient for proving correctness, and the Refinement Calculus allows for a stepwise development method. It also has a parallel interpretation facilitating development of concurrent software, and it is suitable for describing event-driven scenarios. However, for many application areas, the execution paradigm traditionally used comprises more explicit control flow, which constitutes an obstacle for using the above mentioned formal methods. In this thesis, we study how guarded command based modelling approaches can be conveniently and efficiently scheduled in different scenarios. We first focus on the modelling of trust for transactions in a social networking setting. Due to the event-based nature of the scenario, the use of guarded commands turns out to be relatively straightforward. We continue by studying modelling of concurrent software, with particular focus on compute-intensive scenarios. We go from theoretical considerations to the feasibility of implementation by evaluating the performance and scalability of executing a case study model in parallel using automatic scheduling performed by a dedicated scheduler. Finally, we propose a more explicit and non-centralised approach in which the flow of each task is controlled by a schedule of its own. The schedules are expressed in a dedicated scheduling language, and patterns assist the developer in proving correctness of the scheduled model with respect to the original one.

Kasvatus on kasvamaan saattamista. Kasvatusfilosofinen tutkimus J. A. Hollon sivistyskasvatusajattelusta

Tutkimukseni käsittelee J. A. Hollon (1885–1967) sivistyskasvatusajattelua. Hollo oli monitoiminen kulttuurivaikuttaja, joka toimi kriitikkona, kirjailijana, suomentajana ja kasvatustieteilijänä. Häntä voidaan pitää J. V. Snellmanin rinnalla yhtenä merkittävimpänä suomalaisena kasvatusajattelijana. Hänen kasvatusajattelustaan ei ole kuitenkaan aiemmin tehty väitöskirjatason tutkimusta. Tutkimuskysymykseni ovat seuraavat: 1. Millainen on Hollon näkemys kasvatuksesta, kasvatuksen maailmasta ja kasvatuksen teoriasta? 2. Mikä on Hollon käsitys kasvattajan ja kasvatettavan merkityksestä kasvatustapahtumassa? 3. Mitä asioita sisältyy sivistyskasvatuksen eli kasvamaan saattamisen elementteihin? Tutkimukseni on kasvatusfilosofinen. Tutkimusmenetelmäni on systemaattinen analyysi ja lähestymistapani on hermeneuttinen. Tutkimukseni pääaineistona ovat Hollon kasvatusta koskevat kirjoitukset, joista tärkeimmät ovat Mielikuvitus ja sen kasvattaminen I-II (1918, 1919), Kasvatuksen maailma (1927), Kasvatuksen teoria (1927) ja Itsekasvatus ja elämisen taito (1931). Hollon mukaan kasvatuksen maailma on suhteellisen itsenäinen elämänmuoto (Lebensform), jolla on oma ontologinen erityislaatunsa, so. sui generis. Kasvatusoppia ei pidä redusoida psykologiaan tai filosofiaan, koska sillä tavoin se menettää tieteellisen itsenäisyytensä. Hollon mielestä kasvatuksen teoria on teoria käytäntöä varten. Kasvatuksen teorian luomisessa tulee ottaa huomioon kasvatuksen maailman erityispiirteenä oleva kokonaisvaltainen näkökulma ja elämän palvelemisen päämäärä. Kasvattaminen on aina myös eettistä toimintaa. Kasvatuksen tavoitteena on hyvä elämä. Hollon mukaan kasvattajan tehtävä on luoda kasvatettavalleen eheä sivistyksellinen perusta. Tämä voi tapahtua vain laaja-alaisen sivistyskasvatuksen avulla, jonka runkona on antiikin humanistinen sivistysperinne. Sivistyskasvatukseen kuuluvat älyllinen, eettinen, uskonnollinen, esteettinen ja toiminnallinen kasvatus. Mielikuvituksen avulla kasvattaja voi yhdistää kasvatuksen osa-alueet eheäksi kokonaisuudeksi. Ilman mielikuvitusta erilaiset ilmiöt olisivat pirstaleisina, toisistaan erillisinä osina ihmisen mielessä. Opettajan persoona on merkittävä tekijä kasvatuksessa. Se tulee ottaa huomioon opettajankoulutuksen eli kasvattajan kasvattamisen valinnoissa. Opettaja-kasvattajan on tärkeää opiskella laajasti humanistisia opintoja, koska kasvatuksessa on kysymys ihmisestä. Ennen kaikkea kasvattajan eettistä ja esteettistä kykyä tulee harjoituttaa. Näin hän oppii käyttämään mielikuvitustaan kasvatustapahtumassa siten, että hän tulee kasvatuksellisesti näkeväksi kasvamaan saattajaksi, joka ymmärtää sen, mikä kussakin tilanteessa vaatii erityistä huomiota. Tutkimukseni osoittaa, että Hollon henkitieteellinen ja fenomenologis-hermeneuttinen kasvatusnäkemys ei ole vain vastaparadigma empiiriselle kasvatustieteelle, vaan myös nykyajan teknis-taloudelliselle eetokselle, joka yhtäältä uhkaa välineellistää kasvatuksen ja toisaalta väärällä tavoin tieteellistää kasvatuksen tutkimuksen. Tämän takia kasvatusoppi kysymyksineen uhkaa siirtyä kasvatuskeskustelussa syrjemmälle, jopa hävitä kokonaan. Kasvatuksen ja kasvatuksen tutkimuksen vaarana on niiden liiallinen sitouttaminen tuotantoelämän jatkeeksi, minkä seurauksena on ihmisyyden toteuttamisen vaikeutuminen. Tutkimuksen lopuksi esitän ideaalikoulunäkemykseni, joka perustuu osittain Hollon kasvatusnäkemykseen. Hollon näkemys on yhä ajankohtainen ja merkittävä kontribuutio kasvatusta, sen teoriaa ja käytäntöä koskevaan keskusteluun.

Formal development and quantitative verification of dependable systems

-

Magnetic Resocance Imaging Methods in the Follow-up of Multiple Sclerosis and in Farby Disease

Multiple sclerosis (MS) is a chronic immune-mediated inflammatory disorder of the central nervous system. MS is the most common disabling central nervous system (CNS) disease of young adults in the Western world. In Finland, the prevalence of MS ranges between 1/1000 and 2/1000 in different areas. Fabry disease (FD) is a rare hereditary metabolic disease due to mutation in a single gene coding α-galactosidase A (alpha-gal A) enzyme. It leads to multi-organ pathology, including cerebrovascular disease. Currently there are 44 patients with diagnosed FD in Finland. Magnetic resonance imaging (MRI) is commonly used in the diagnostics and follow-up of these diseases. The disease activity can be demonstrated by occurrence of new or Gadolinium (Gd)-enhancing lesions in routine studies. Diffusion-weighted imaging (DWI) and diffusion tensor imaging (DTI) are advanced MR sequences which can reveal pathologies in brain regions which appear normal on conventional MR images in several CNS diseases. The main focus in this study was to reveal whether whole brain apparent diffusion coefficient (ADC) analysis can be used to demonstrate MS disease activity. MS patients were investigated before and after delivery and before and after initiation of diseasemodifying treatment (DMT). In FD, DTI was used to reveal possible microstructural alterations at early timepoints when excessive signs of cerebrovascular disease are not yet visible in conventional MR sequences. Our clinical and MRI findings at 1.5T indicated that post-partum activation of the disease is an early and common phenomenon amongst mothers with MS. MRI seems to be a more sensitive method for assessing MS disease activity than the recording of relapses. However, whole brain ADC histogram analysis is of limited value in the follow-up of inflammatory conditions in a pregnancy-related setting because the pregnancy-related physiological effects on ADC overwhelm the alterations in ADC associated with MS pathology in brain tissue areas which appear normal on conventional MRI sequences. DTI reveals signs of microstructural damage in brain white matter of FD patients before excessive white matter lesion load can be observed on conventional MR scans. DTI could offer a valuable tool for monitoring the possible effects of enzyme replacement therapy in FD.

Reusable formal architectures for networked systems

Today's networked systems are becoming increasingly complex and diverse. The current simulation and runtime verification techniques do not provide support for developing such systems efficiently; moreover, the reliability of the simulated/verified systems is not thoroughly ensured. To address these challenges, the use of formal techniques to reason about network system development is growing, while at the same time, the mathematical background necessary for using formal techniques is a barrier for network designers to efficiently employ them. Thus, these techniques are not vastly used for developing networked systems. The objective of this thesis is to propose formal approaches for the development of reliable networked systems, by taking efficiency into account. With respect to reliability, we propose the architectural development of correct-by-construction networked system models. With respect to efficiency, we propose reusable network architectures as well as network development. At the core of our development methodology, we employ the abstraction and refinement techniques for the development and analysis of networked systems. We evaluate our proposal by employing the proposed architectures to a pervasive class of dynamic networks, i.e., wireless sensor network architectures as well as to a pervasive class of static networks, i.e., network-on-chip architectures. The ultimate goal of our research is to put forward the idea of building libraries of pre-proved rules for the efficient modelling, development, and analysis of networked systems. We take into account both qualitative and quantitative analysis of networks via varied formal tool support, using a theorem prover the Rodin platform and a statistical model checker the SMC-Uppaal.

Real-time Image-based RGB-D Camera Motion Tracking and Environment Mapping

In this work, image based estimation methods, also known as direct methods, are studied which avoid feature extraction and matching completely. Cost functions use raw pixels as measurements and the goal is to produce precise 3D pose and structure estimates. The cost functions presented minimize the sensor error, because measurements are not transformed or modified. In photometric camera pose estimation, 3D rotation and translation parameters are estimated by minimizing a sequence of image based cost functions, which are non-linear due to perspective projection and lens distortion. In image based structure refinement, on the other hand, 3D structure is refined using a number of additional views and an image based cost metric. Image based estimation methods are particularly useful in conditions where the Lambertian assumption holds, and the 3D points have constant color despite viewing angle. The goal is to improve image based estimation methods, and to produce computationally efficient methods which can be accomodated into real-time applications. The developed image-based 3D pose and structure estimation methods are finally demonstrated in practise in indoor 3D reconstruction use, and in a live augmented reality application.

Testing FCM technique for the wind energy scenarios in Finland

In the latter days, human activities constantly increase greenhouse gases emissions in the atmosphere, which has a direct impact on a global climate warming. Finland as European Union member, developed national structural plan to promote renewable energy generation, pursuing the aspects of Directive 2009/28/EC and put it on the sharepoint. Finland is on a way of enhancing national security of energy supply, increasing diversity of the energy mix. There are plenty significant objectives to develop onshore and offshore wind energy generation in country for a next few decades, as well as another renewable energy sources. To predict the future changes, there are a lot of scenario methods developed and adapted to energy industry. The Master’s thesis explored “Fuzzy cognitive maps” approach in scenarios developing, which captures expert’s knowledge in a graphical manner and using these captures for a raw scenarios testing and refinement. There were prospects of Finnish wind energy development for the year of 2030 considered, with aid of FCM technique. Five positive raw scenarios were developed and three of them tested against integrated expert’s map of knowledge, using graphical simulation. The study provides robust scenarios out of the preliminary defined, as outcome, assuming the impact of results, taken after simulation. The thesis was conducted in such way, that there will be possibilities to use existing knowledge captures from expert panel, to test and deploy different sets of scenarios regarding to Finnish wind energy development.

From emerging opportunities to successful business networks – evidence from bioenergy

Increasing renewable energy utilization is a challenge that is tried to be solved in different ways. One of the most promising options for renewable energy is different biomasses, and the bioenergy field offers numerous emerging business opportunities. The actors in the field have rarely all the needed know-how and resources for exploiting these opportunities, and thus it is reasonable to seize them in cooperation. Networking is not an easy task to carry out, however, and in addition to its advantages for the firms engaged, it sets numerous challenges as well. The development of a network is a result of several steps firms need to take. In order to gain optimal advantage of their networks, firms need to weigh out with whom, why and how they should cooperate. In addition, everything does not depend on the firms themselves, as several factors in the external environment set their own enablers and barriers for cooperation. The formation of a network around a business opportunity is thus a multiphase process. The objective of this thesis is to depict this process via a step-by-step analysis and thus increase understanding on the whole development path from an entrepreneurial opportunity to a successful business network. The empirical evidence has been gathered by discussing the opportunities of animal manure refinement to biogas and forest biomass utilization for heating in Finland. The thesis comprises two parts. The first part provides an overview of the study, and the second part includes five research publications. The results reveal that it is essential to identify and analyze all the steps in the development process of a network, and several frameworks are used in the thesis to analyze these steps. The frameworks combine the views of theory and practical experiences of empirical study, and thus give new multifaceted views for the discussion on SME networking. The results indicate that the ground for cooperation should be investigated adequately by taking account of the preconditions in all the three contexts in which the actors operate: the social context, the region and the institutional environment. In case the project advances to exploitation, the assets and objectives of the actors should be paired off, which sets a need for relationships and sub-networks differing in breadth and depth. Different relationships and networks require different kinds of maintenance and management. Moreover, the actors should have the capability to change the formality or strategy of the relationships if needed. The drivers for these changes come along with the changing environment, which causes changes in the objectives of the actors and this way in the whole network. Bioenergy as the empirical field of the study represents well an industrial field with many emerging opportunities, a motley group of actors, and sensitivity for fast changes.

Rigorous development of safety-critical systems

Nowadays, computer-based systems tend to become more complex and control increasingly critical functions affecting different areas of human activities. Failures of such systems might result in loss of human lives as well as significant damage to the environment. Therefore, their safety needs to be ensured. However, the development of safety-critical systems is not a trivial exercise. Hence, to preclude design faults and guarantee the desired behaviour, different industrial standards prescribe the use of rigorous techniques for development and verification of such systems. The more critical the system is, the more rigorous approach should be undertaken. To ensure safety of a critical computer-based system, satisfaction of the safety requirements imposed on this system should be demonstrated. This task involves a number of activities. In particular, a set of the safety requirements is usually derived by conducting various safety analysis techniques. Strong assurance that the system satisfies the safety requirements can be provided by formal methods, i.e., mathematically-based techniques. At the same time, the evidence that the system under consideration meets the imposed safety requirements might be demonstrated by constructing safety cases. However, the overall safety assurance process of critical computerbased systems remains insufficiently defined due to the following reasons. Firstly, there are semantic differences between safety requirements and formal models. Informally represented safety requirements should be translated into the underlying formal language to enable further veri cation. Secondly, the development of formal models of complex systems can be labour-intensive and time consuming. Thirdly, there are only a few well-defined methods for integration of formal verification results into safety cases. This thesis proposes an integrated approach to the rigorous development and verification of safety-critical systems that (1) facilitates elicitation of safety requirements and their incorporation into formal models, (2) simplifies formal modelling and verification by proposing specification and refinement patterns, and (3) assists in the construction of safety cases from the artefacts generated by formal reasoning. Our chosen formal framework is Event-B. It allows us to tackle the complexity of safety-critical systems as well as to structure safety requirements by applying abstraction and stepwise refinement. The Rodin platform, a tool supporting Event-B, assists in automatic model transformations and proof-based verification of the desired system properties. The proposed approach has been validated by several case studies from different application domains.

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.

Weldability of powder bed fusion fabricated stainless steel 316L sheets to cold rolled sheet metal

Weldability of powder bed fusion (PBF) fabricated components has come to discussion in past two years due to resent developments in the PBF technology and limited size of the machines used in the fabrication process. This study concentrated on effects of energy input of welding on mechanical properties and microstructural features of welds between PBF fabricated stainless steel 316L sheets and cold rolled sheet metal of same composition by the means of destructive testing and microscopic analysis. Optical fiber diameter, laser power and welding speed were varied during the experiments that were executed following one variable at a time (OVAT) method. One of the problems of welded PBF fabricated components has been lower elongations at break comparing to conventionally manufactured components. Decreasing energy input of the laser keyhole welding decreased elongations at break of the welded specimens. Ultimate tensile strengths were not affected significantly by the energy input of the welding, but fracturing of the specimens welded using high energy input occurred from the weld metal. Fracturing of the lower energy input welds occurred from the PBF fabricated base metal. Energy input was found to be critical factor for mechanical properties of the welds. Multioriented grain growth and formation of neck at fusion zone boundary on the cold rolled side of the weld was detected and suspected to be result from weld pool flows caused by differences in molten weld pool behaviour between the PBF fabricated and cold rolled sides of the welds.

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.