Moment Operators of Observables in Quantum Mechanics, with Applications to Quantization and Homodyne Detection

The questions studied in this thesis are centered around the moment operators of a quantum observable, the latter being represented by a normalized positive operator measure. The moment operators of an observable are physically relevant, in the sense that these operators give, as averages, the moments of the outcome statistics for the measurement of the observable. The main questions under consideration in this work arise from the fact that, unlike a projection valued observable of the von Neumann formulation, a general positive operator measure cannot be characterized by its first moment operator. The possibility of characterizing certain observables by also involving higher moment operators is investigated and utilized in three different cases: a characterization of projection valued measures among all the observables is given, a quantization scheme for unbounded classical variables using translation covariant phase space operator measures is presented, and, finally, a mathematically rigorous description is obtained for the measurements of rotated quadratures and phase space observables via the high amplitude limit in the balanced homodyne and eight-port homodyne detectors, respectively. In addition, the structure of the covariant phase space operator measures, which is essential for the above quantization, is analyzed in detail in the context of a (not necessarily unimodular) locally compact group as the phase space.

Mild Cognitive Impairment and Early Detection of Alzheimer`s Disease. A Positron Emission Tomography Study

Alzheimer`s disease (AD) is characterised neuropathologically by the presence of extracellular amyloid plaques, intraneuronal neurofibrillary tangles, and cerebral neuronal loss. The pathological changes in AD are believed to start even decades before clinical symptoms are detectable. AD gradually affects episodic memory, cognition, behaviour and the ability to perform everyday activities. Mild cognitive impairment (MCI) represents a transitional state between normal aging and dementia disorders, especially AD. The predictive accuracy of the current and commonly used MCI criteria devide this disorder into amnestic (aMCI) and non-amnestic (naMCI) MCI. It seems that many individuals with aMCI tend to convert to AD. However many MCI individuals will remain stable and some may even recover. At present, the principal drugs for the treatment of AD provide only symptomatic and palliative benefits. Safe and effective mechanism-based therapies are needed for this devastating neurodegenerative disease of later life. In conjunction with the development of new therapeutic drugs, tools for early detection of AD would be important. In future one of the challenges will be to detect at an early stage these MCI individuals who will convert to AD. Methods which can predict which MCI subjects will convert to AD will be much more important if the new drug candidates prove to have disease-arresting or even disease–slowing effects. These types of drugs are likely to have the best efficacy if administered in the early or even in the presymptomatic phase of the disease when the synaptic and neuronal loss has not become too widespread. There is no clinical method to determine with certainly which MCI individuals will progress to AD. However there are several methods which have been suggested as predictors of conversion to AD, e.g. increased [11C] PIB uptake, hippocampal atrophy in MRI, low CSF A beta 42 level, high CSF tau-protein level, apolipoprotein E (APOE) ε4 allele and impairment in episodic memory and executive functions. In the present study subjects with MCI appear to have significantly higher [¹¹C] PIB uptake vs healthy elderly in several brain areas including frontal cortex, the posterior cingulate, the parietal and lateral temporal cortices, putamen and caudate. Also results from this PET study indicate that over time, MCI subjects who display increased [¹¹C] PIB uptake appear to be significantly more likely to convert to AD than MCI subjects with negative [¹¹C] PIB retention. Also hippocampal atrophy seems to increase in MCI individuals clearly during the conversion to AD. In this study [¹¹C] PIB uptake increases early and changes relatively little during the AD process whereas there is progressive hippocampal atrophy during the disease. In addition to increased [¹¹C] PIB retention and hippocampal atrophy, the status of APOE ε4 allele might contribute to the conversion from MCI to AD.

Identification and characterisation of a novel adhesin of Streptococcus suis and its use as a target of adhesion inhibition and bacterial detection

Streptococcus suis is an important pig pathogen but it is also zoonotic, i.e. capable of causing diseases in humans. Human S. suis infections are quite uncommon but potentially life-threatening and the pathogen is an emerging public health concern. This Gram-positive bacterium possesses a galabiose-specific (Galalpha1−4Gal) adhesion activity, which has been studied for over 20 years. P-fimbriated Escherichia coli−bacteria also possess a similar adhesin activity targeting the same disaccharide. The galabiose-specific adhesin of S. suis was identified by an affinity proteomics method. No function of the protein identified was formerly known and it was designated streptococcal adhesin P (SadP). The peptide sequence of SadP contains an LPXTG-motif and the protein was proven to be cell wall−anchored. SadP may be multimeric since in SDS-PAGE gel it formed a protein ladder starting from about 200 kDa. The identification was confirmed by producing knockout strains lacking functional adhesin, which had lost their ability to bind to galabiose. The adhesin gene was cloned in a bacterial expression host and properties of the recombinant adhesin were studied. The galabiose-binding properties of the recombinant protein were found to be consistent with previous results obtained studying whole bacterial cells. A live-bacteria application of surface plasmon resonance was set up, and various carbohydrate inhibitors of the galabiose-specific adhesins were studied with this assay. The potencies of the inhibitors were highly dependent on multivalency. Compared with P-fimbriated E. coli, lower concentrations of galabiose derivatives were needed to inhibit the adhesion of S. suis. Multivalent inhibitors of S. suis adhesion were found to be effective at low nanomolar concentrations. To specifically detect galabiose adhesin−expressing S. suis bacteria, a technique utilising magnetic glycoparticles and an ATP bioluminescence bacterial detection system was also developed. The identification and characterisation of the SadP adhesin give valuable information on the adhesion mechanisms of S. suis, and the results of this study may be helpful for the development of novel inhibitors and specific detection methods of this pathogen.

Inactive endosialidase-based detection of bacterial and oncofetal polysialic acid

Polysialic acid is a carbohydrate polymer which consist of N-acetylneuraminic acid units joined by alpha2,8-linkages. It is developmentally regulated and has an important role during normal neuronal development. In adults, it participates in complex neurological processes, such as memory, neural plasticity, tumor cell growth and metastasis. Polysialic acid also constitutes the capsule of some meningitis and sepsis-causing bacteria, such as Escherichia coli K1, group B meningococci, Mannheimia haemolytica A2 and Moraxella nonliquefaciens. Polysialic acid is poorly immunogenic; therefore high affinity antibodies against it are difficult to prepare, thus specific and fast detection methods are needed. Endosialidase is an enzyme derived from the E. coli K1 bacteriophage, which specifically recognizes and degrades polysialic acid. In this study, a novel detection method for polysialic acid was developed based on a fusion protein of inactive endosialidase and the green fluorescent protein. It utilizes the ability of the mutant, inactive endosialidase to bind but not cleave polysialic acid. Sequencing of the endosialidase gene revealed that amino acid substitutions near the active site of the enzyme differentiate the active and inactive forms of the enzyme. The fusion protein was applied for the detection of polysialic acid in bacteria and neuroblastoma. The results indicate that the fusion protein is a fast, sensitive and specific reagent for the detection of polysialic acid. The use of an inactive enzyme as a specific molecular tool for the detection of its substrate represents an approach which could potentially find wide applicability in the specific detection of diverse macromolecules.

Supervised localimage feature detection

This thesis is about detection of local image features. The research topic belongs to the wider area of object detection, which is a machine vision and pattern recognition problem where an object must be detected (located) in an image. State-of-the-art object detection methods often divide the problem into separate interest point detection and local image description steps, but in this thesis a different technique is used, leading to higher quality image features which enable more precise localization. Instead of using interest point detection the landmark positions are marked manually. Therefore, the quality of the image features is not limited by the interest point detection phase and the learning of image features is simplified. The approach combines both interest point detection and local description into one phase for detection. Computational efficiency of the descriptor is therefore important, leaving out many of the commonly used descriptors as unsuitably heavy. Multiresolution Gabor features has been the main descriptor in this thesis and improving their efficiency is a significant part. Actual image features are formed from descriptors by using a classifierwhich can then recognize similar looking patches in new images. The main classifier is based on Gaussian mixture models. Classifiers are used in one-class classifier configuration where there are only positive training samples without explicit background class. The local image feature detection method has been tested with two freely available face detection databases and a proprietary license plate database. The localization performance was very good in these experiments. Other applications applying the same under-lying techniques are also presented, including object categorization and fault detection.

Neurophysiologic diagnosis, clinical symptoms and neuropathologic findings in polyneuropathies

Tausta: Polyneuropatia (PNP) on ääreishermoston sairaus, joka aiheuttaa laaja-alaisia, yleensä symmetrisiä vaurioita ääreishermostossa. PNP:aan johtavia syitä on satoja. Tavoitteet: Löytää parhaat neurofysiologiset menetelmät uremian, myelooman hoidossa käytettävän talidomidin sekä Fabryn taudin aiheuttaman PNP:n diagnosoimiseksi. Fabryn taudissa tutkin lisäksi ohutsäieneuropatian aiheuttamia neuropatologisia löydöksiä iholta otetusta koepalasta. Tutkimuksissa kartoitettiin lisäksi PNP:n aiheuttamien subjektiivisten oireiden korrelaatio neurofysiologisten ja neuropatologisten löydösten kanssa. Munuaisten vajaatoimintaa sairastavilla potilailla tavoitteena oli tutkia dialyysihoidon tehon vaikutusta autonomisen hermoston toimintaan sekä yhden dialyysikerran vaikutusta neurofysiologisiin löydöksiin. Aineisto ja menetelmät: I: Tutkittiin 21 uremiapotilaan sensoristen ja motoristen hermojen vasteet, värinä- sekä lämpötuntokynnykset ennen ja jälkeen hemodialyysin. Subjektiiviset PNP oireet kartoitettiin PNP oireita kysyvillä kaavakkeella. II:12 talidomidi hoitoa saavaa myeloomapotilasta, tutkimuksen menetelmät olivat samat kuin tutkimuksessa I. III: 12 Fabryn tautia sairastavaa potilasta, edellä mainittujen neurofysiologisten tutkimusten lisäksi potilailta otettiin ihobiopsia säären alueelta. Ihobiopsiasta laskettiin ohuiden hermosyiden määrä koepalan värjäyksen jälkeen. Subjektiiviset PNP oireet kartoitettiin kyselykaavakkeella. Sydämen sykevaihtelu tutkittiin levossa taajuustason analyysillä. IV: 32 uremiapotilaan autonomisen hermoston toimintaa tutkittiin sydämen sykevaihtelun aikatason analysillä, paksujen myelinoituneiden säikeiden toimintaa tutkittiin perifeeristen sensoristen hermojen mittauksilla toistetusti noin 2.9 vuoden aikana. Tulokset: Ureemisen PNP:n diagnostiikassa herkimmät tutkimukset ovat F-aaltojen parametrit alaraajojen motorisista hermoista, värinätuntokynnys alaraajoista sekä suralishermon amplitudi. Positiiviset PNP oireet uremiassa korreloivat värinätunto-kynnyksen sekä sensoristen hermojen neurografialöydösten kanssa. Neurofysiologisten tutkimusten ajankohdalla dialyysiajankohtaan nähden ei ole merkitystä. Talidomidi-PNP on pääasiassa sensorinen, mutta motoriset syyt ovat lievästi vaurioituneet. Talidomidi PNP:ssa subjektiiviset oireet korreloivat huonosti neurofysiologisten löydösten kanssa. Fabryn taudissa naisilla on oletettua enemmän ohutsäieneuropatian aiheuttamia oireita ja löydöksiä. Paksujen säikeiden löydöksiä ei tullut esiin. Ohutsäieneuropatian diagnostiikassa ihobiopsia ja kvantitatiiviset tuntokynnysmittaustestit täydentävät toisiaan. Tehokas dialyysi parantaa autonomisen hermoston toimintaa uremiapotilailla. Päätelmät: Erityyppisten polyneuropatioiden diagnostiikassa pitää etukäteen valita PNP tyypille oikeat tutkimusmenetelmät raskaiden tutkimuspatterien vähentämiseksi sekä diagnostiikan parantamiseksi. PNP:n aiheuttamat oireet ja kliiniset löydökset pitää aina tutkia, mutta yksin ne eivät ole herkkiä PNP:n diagnostiikassa.

Switchable Lanthanide Luminescence for Detection of Biomolecules

Binary probes are oligonucleotide probe pairs that hybridize adjacently to a complementary target nucleic acid. In order to detect this hybridization, the two probes can be modified with, for example, fluorescent molecules, chemically reactive groups or nucleic acid enzymes. The benefit of this kind of binary probe based approach is that the hybridization elicits a detectable signal which is distinguishable from background noise even though unbound probes are not removed by washing before measurement. In addition, the requirement of two simultaneous binding events increases specificity. Similarly to binary oligonucleotide probes, also certain enzymes and fluorescent proteins can be divided into two parts and used in separation-free assays. Split enzyme and fluorescent protein reporters have practical applications among others as tools to investigate protein-protein interactions within living cells. In this study, a novel label technology, switchable lanthanide luminescence, was introduced and used successfully in model assays for nucleic acid and protein detection. This label technology is based on a luminescent lanthanide chelate divided into two inherently non-luminescent moieties, an ion carrier chelate and a light harvesting antenna ligand. These form a highly luminescent complex when brought into close proximity; i.e., the label moieties switch from a dark state to a luminescent state. This kind of mixed lanthanide complex has the same beneficial photophysical properties as the more typical lanthanide chelates and cryptates - sharp emission peaks, long emission lifetime enabling time-resolved measurement, and large Stokes’ shift, which minimize the background signal. Furthermore, the switchable lanthanide luminescence technique enables a homogeneous assay set-up. Here, switchable lanthanide luminescence label technology was first applied to sensitive, homogeneous, single-target nucleic acid and protein assays with picomolar detection limits and high signal to background ratios. Thereafter, a homogeneous four-plex nucleic acid array-based assay was developed. Finally, the label technology was shown to be effective in discrimination of single nucleotide mismatched targets from fully matched targets and the luminescent complex formation was analyzed more thoroughly. In conclusion, this study demonstrates that the switchable lanthanide luminescencebased label technology can be used in various homogeneous bioanalytical assays.

Enterohemorraginen Escherichia coli (EHEC) ja sen osoittaminen PCR-menetelmällä

Summary: Enterohemorrhagic Escherichia coli (EHEC) and its detection with a PCR method

Soodakattilan vesi-höyryjärjestelmän vuodonvalvonta

Työn tavoitteena oli kehittää Kaukaan sellutehtaalle luotettava vesi-höyrypiirin vuodonvalvontajärjestelmä. Vesi-höyrypiirin vuodonvalvontajärjestelmällä pystytään ehkäisemään soodakattilassa mahdollisen putkivaurion aiheuttama sulavesiräjähdys. Työn teoreettisessa osassa käsitellään soodakattilan turvallisuutta sekätutustutaan kaupallisilla markkinoilla oleviin vuodonvalvontajärjestelmiin. Vuodonvalvontajärjestelmän kehityksessä käytetään hyväksi prosessitietoa noin vuoden ajalta sekä yhden vakavan vesi-höyrypiirin putkirikon aikaisia mittaustietoja.Työssä testataan käytännössä Kaukaan soodakattilaan rakennettu järjestelmä. Työn tuloksena Kaukaan sellutehtaan soodakattilan on rakennettu vuodonvalvontajärjestelmä, joka havaitsee vesi-höyrypiirin putkirikon aiheuttaman vuodon, määrittää sen suuruuden sekä pystyy paikantamaan vuodon sijainnin.

Tuotekohtaisen kustannuslaskennan kehittäminen metallituoteyrityksessä

Työn tavoitteena oli muodostaa kustannuslaskentajärjestelmä tuotekohtaisten kustannusten selvittämiseen ja raportointiin. Kustannuksien määrätietoinen johtaminen ei ole mahdollista, ellei tuotteiden kustannusrakenne ja kustannuksiin vaikuttavat tekijät ole selvillä. Tavoitteeksi laskentajärjestelmälle asetettiin, että sen avulla tulisi pystyä selvittämään tuotteiden kustannusrakenteet sekä myyntikatteiden vaikutus yrityksen tuloksen muodostumiseen. Mallille asetettuja vaatimuksia oli vaivaton päivitysmahdollisuus, sekä laskentaperusteiden selvittäminen ja mahdollinen muokkaaminen. Laskentajärjestelmä toteutettiin taulukkolaskentaohjelmalla. Ensisijaiseksi laskentakohteeksi asetettiin yrityksen tuotteet, mutta tarvetta ilmeni myös projekti- ja asiakaskohtaisen kannattavuuden tarkasteluun. Työ jakaantuu kahteen osaan. Ensimmäisessä osassa suoritetaan kirjallisuustutkimus tuotekohtaisesta kustannuslaskennasta. Toisessa osassa on selvitetty kustannuslaskentajärjestelmän kehittämisen vaiheita kohdeyrityksessä, sekä esitelty järjestelmän rakennetta. Viimeiseksi on käyty läpi laskentajärjestelmän testausta, käyttömahdollisuuksia, tuloksien tarkastelua sekä jatkokehitysmahdollisuuksia.

Vaatimusmäärittelykäytäntöjen sovellettavuus talousohjauksen vaatimuksia kartoitettaessa

Vaatimusten määrittelyn tarkoitus on kartoittaa tietojärjestelmän käyttäjien työtehtäviä ja niihin liittyviä järjestelmän toiminnallisia ja ei-toiminnallisia vaatimuksia. Todellinen asiakasnäkökulma tulee esille yrityksen itse käynnistämässä vaatimusten määrittelyssä. Nykytilan selvittäminen ja kriittisten toimintojen havaitseminen käynnistävät kohdeyksikössä käytävän keskinäisen keskustelun, mikä on edellytyksenä järjestelmävaatimusten havaitsemiseen. Tämän työn teoriaosuudessa lähestytään eri näkökulmia vaatimustenmäärittelyyn. Tämän jälkeen esitellään muutamia asiakasyritykselle sopivia määrittelymenetelmiä, joita voidaan hyödyntää valmisohjelmistohankeen määrittelyssä. Työssä esitetään myös toiminnanohjaukseen ja tietovarastointiin tarkoitettujen järjestelmien tapaa kerätä taloudellista informaatiota ja luoda raportteja johdolle päätöksenteon tueksi. Työn empiirisessä osassa selvitetään mitkä ovat Lappeenrannan Energia Oy:n asettamat liiketoiminnalliset tarpeet ja vaatimukset uudelle talousohjauksen tietojärjestelmälle.

Community-acquired pneumonia in adult patients with special reference to rapid methods for etiological diagnosis

Aikuispotilaan kotisyntyisen keuhkokuumeen etiologinen diagnostiikka mikrobiologisilla pikamenetelmillä Tausta. Keuhkokuume on vakava sairaus, johon sairastuu Suomessa vuosittain n. 60 000 aikuista. Huolimatta siitä, että taudin hoito on kehittynyt, siihen liittyy yhä merkittävä, 6-15%:n kuolleisuus. Alahengitystieinfektion aiheuttajamikrobien tunnistaminen on myös edelleen haasteellista. Tavoitteet. Tämän työn tavoitteena oli tutkia Turun yliopistollisessa keskussairaalassa hoidettujen aikuispotilaiden keuhkokuumeen etiologiaa sekä selvittää uusien mikrobiologisten pikamenetelmi¬en hyödyllisyyttä taudinaiheuttajan toteamisessa. Aineisto. Osatöiden I ja III aineisto koostui 384 Turun yliopistollisen keskussairaalaan infektio-osastolla hoidetusta keuhkokuumepotilaasta. Osatyössä I tutkittiin keuhkokuumeen aiheuttaja¬mikrobeja käyttämällä perinteisten menetelmien lisäksi antigeeniosoitukseen ja PCR-tekniikkaan perustuvia pikamenetelmiä. Osatyö II käsitti 231 potilaasta koostuvan alaryhmän, jossa tutkittiin potilaiden nielun limanäytteestä rinovirusten ja enterovirusten esiintyvyyttä. Osatyössä III potilailta tutkittiin plasman C-reaktiivisen proteiinin (CRP) pitoisuus ensimmäisten viiden sairaalahoitopäi¬vän aikana. Laajoja tilastotieteellisiä analyysejä käyttämällä selvitettiin CRP:n käyttökelpoisuutta sairauden vaikeusasteen arvioinnissa ja komplikaatioiden kehittymisen ennustamisessa. Osatyössä IV 68 keuhkokuumepotilaan sairaalaan tulovaiheessa otetuista näytteistä määritettiin neutrofiilien pintareseptorien ekspressio. Osatyössä V analysoitiin sisätautien vuodeosastoilla vuosina 1996-2000 keuhkokuumepotilaille tehtyjen keuhkohuuhtelunäytteiden laboratoriotutkimustulokset. Tulokset. Keuhkokuumeen aiheuttaja löytyi 209 potilaalta, aiheuttajamikrobeja löydettiin kaikkiaan 230. Näistä aiheuttajista 135 (58.7%) löydettiin antigeenin osoituksella tai PCR-menetelmillä. Suu¬rin osa, 95 (70.4%), todettiin pelkästään kyseisillä pikamenetelmillä. Respiratorinen virus todettiin antigeeniosoituksella 11.1% keuhkokuumepotilaalla. Eniten respiratorisia viruksia löytyi vakavaa keuhkokuumetta sairastavilta potilailta (20.3%). 231 keuhkokuumepotilaan alaryhmässä todettiin PCR-menetelmällä picornavirus 19 (8.2%) potilaalla. Respiratorinen virus löytyi tässä potilasryh¬mässä kaiken kaikkiaan 47 (20%) potilaalta. Näistä 17:llä (36%) löytyi samanaikaisesti bakteerin aiheuttama infektio. CRP-tasot olivat sairaalaan tulovaiheessa merkitsevästi korkeammat vakavaa keuhkokuumetta (PSI-luokat III-V) sairastavilla potilailla kuin lievää keuhkokuumetta (PSI-luokat I-II) sairastavilla potilailla (p <0.001). Yli 100 mg/l oleva CRP-taso neljän päivän kuluttua sairaa¬laan tulosta ennusti keuhkokuumeen komplikaatiota tai huonoa hoitovastetta. Neutrofiilien komple¬menttireseptorin ekspressio oli pneumokokin aiheuttamaa keuhkokuumetta sairastavilla merkitse¬västi korkeampi kuin influenssan aiheuttamaa keuhkokuumetta sairastavilla. BAL-näytteistä vain yhdessä 71:stä (1.3%) todettiin diagnostinen bakteerikasvu kvantitatiivisessa viljelyssä. Uusilla menetelmilläkin keuhkokuumeen aiheuttaja löytyi vain 9.8% BAL-näytteistä. Päätelmät. Uusilla antigeeniosoitus- ja PCR-menetelmillä keuhkokuumeen etiologia voidaan saada selvitettyä nopeasti. Lisäksi näitä menetelmiä käyttämällä taudin aiheuttajamikrobi löytyi huomattavasti suuremmalta osalta potilaista kuin pelkästään tavanomaisia menetelmiä käyttämällä. Pikamenetelmien hyödyllisyys vaihteli taudin vaikeusasteen mukaan. Respiratorinen virus löytyi huomattavan usein keuhkokuumetta sairastavilta potilailta, ja näiden potilaiden taudinkuva oli usein vaikea. Tulovaiheen korkeaa CRP-tasoa voidaan käyttää lisäkeinona arvioitaessa keuhkokuumeen vaikeutta. CRP on erityisen hyödyllinen arvioitaessa hoitovastetta ja riskiä komplikaatioiden ke¬hittymiseen. Neutrofiilien komplementtireseptorin ekspression tutkiminen näyttää lupaavalta pi¬kamenetelmältä erottamaan bakteerien ja virusten aiheuttamat taudit toisistaan. Antimikrobihoitoa saavilla potilailla BAL-tutkimuksen löydökset olivat vähäiset ja vaikuttivat hoitoon vain harvoin.

Quality assurance of refuse derived fuel with machine vision

This thesis studies the use of machine vision in RDF quality assurance and manufacturing. Currently machine vision is used in recycling and material detection and some commer- cial products are available in the market. In this thesis an on-line machine vision system is proposed for characterizing particle size. The proposed machine vision system is based on the mapping between image segmenta- tion and the ground truth of the particle size. The results shows that the implementation of such machine vision system is feasible.

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.