Sähkökäyttöisen konejärjestelmän vuorovaikutteinen simulointi

Työn tavoitteena oli toteuttaa simulointimalli, jolla pystytään tutkimaan kestomagnetoidun tahtikoneen aiheuttaman vääntömomenttivärähtelyn vaikutuksia sähkömoottoriin liitetyssä mekaniikassa. Tarkoitus oli lisäksi selvittää kuinka kyseinen simulointimalli voidaan toteuttaa nykyaikaisia simulointiohjelmia käyttäen. Saatujen simulointitulosten oikeellisuus varmistettiin tätä työtä varten rakennetulla verifiointilaitteistolla. Tutkittava rakenne koostui akselista, johon kiinnitettiin epäkeskotanko. Epäkeskotankoon kiinnitettiin massa, jonka sijaintia voitiin muunnella. Massan asemaa muuttamalla saatiin rakenteelle erilaisia ominaistaajuuksia. Epäkeskotanko mallinnettiin joustavana elementtimenetelmää apuna käyttäen. Mekaniikka mallinnettiin dynamiikan simulointiin tarkoitetussa ADAMS –ohjelmistossa, johon joustavana mallinnettu epäkeskotanko tuotiin ANSYS –elementtimenetelmäohjelmasta. Mekaniikan malli siirrettiin SIMULINK –ohjelmistoon, jossa mallinnettiin myös sähkökäyttö. SIMULINK –ohjelmassa mallinnettiin sähkökäyttö, joka kuvaa kestomagnetoitua tahtikonetta. Kestomagnetoidun tahtikoneen yhtälöt perustuvat lineaarisiin differentiaaliyhtälöihin, joihin hammasvääntömomentin vaikutus on lisätty häiriösignaalina. Sähkökäytön malli tuottaa vääntömomenttia, joka syötetään ADAMS –ohjelmistolla mallinnettuun mekaniikkaan. Mekaniikan mallista otetaan roottorin kulmakiihtyvyyden arvo takaisinkytkentänä sähkömoottorin malliin. Näin saadaan aikaiseksi yhdistetty simulointi, joka koostuu sähkötoimilaitekäytöstä ja mekaniikasta. Tulosten perusteella voidaan todeta, että sähkökäyttöjen ja mekaniikan yhdistetty simulointi on mahdollista toteuttaa valituilla menetelmillä. Simuloimalla saadut tulokset vastaavat hyvin mitattuja tuloksia.

EU-projektien hallinnointi

Tutkielman päätavoitteena on selvittää EU-projektien hallinnointia rahoittavan viranomaisen vaatimusten mukaisesti. Tutkielmassa on käytetty toiminta-analyyttista tutkimusotetta. Tutkielman teoreettisen viitekehyksen muodostavat projektisykli-malli ja elinkaari-ajattelu projektin toteuttamisessa. Projektisykli-mallia laajennetaan sen kanssa yhteensopivilla yleisillä projektiteorioilla. Tutkielman empiirinen osa perustuu Etelä-Karjalan liiton rahoittavana viranomaisena laatimien ohjeiden ja ehtojen tutkimiseen sekä EU-rahoitusprosessin tutkimiseen LTKK:n toteuttamien rakennerahastohankkeiden rahoitusmateriaalien avulla. Tutkittava materiaali koostuu Etelä-Karjalan liiton arkistoimasta hankkeiden rahoitusprosessin asiakirjoista. Hankkeissa ilmenneiden ongelmien välttämistä käsitellään projektien hyvän hallinnoinnin kautta. Hyvän hallinnoinnin perustaksi arvioidaan LTKK:n projektien hallinnointi- ja sopimusohjeistoa, rahoittajan ohjeistuksia sekä selvitetään rahoittajan lomakkeiden ydinkohtia. Rahoittajan projektien toteuttamiselle asettamissa ehdoissa merkittävässä asemassa ovat kustannukset, niiden tukikelpoisuus ja osoittaminen projektin aiheuttamiksi. Olennaisimmat ongelmat tai puutteet hankkeiden hallinnoinnissa ovat liittyneet kustannusten todentamiseen. Projektien hyvä hallinnointi perustuu rahoittajan ohjeisiin ja ehtoihin perehtymiseen, hankkeiden hyvään taloussuunnitteluun, kustannusseurantaan sekä projektihenkilöstön ja taloushenkilöstön yhteistyöhön.

Vieraalla kielellä tapahtuvan sisäisen viestinnän vaikutukset organisaation tietovarantoon postmodernin tietokäsityksen viitekehyksessä

Tutkimus pohtii tiedon ja kielitaidon välistä suhdetta kansainvälisen organisaation sisäisessä viestinnässä. Työssä keskitytään erityisesti virallisen kielen vaihtamisen vaikutuksiin organisatorisentiedon laatuun ja määrään. Aihepiiriä lähestytään käsiteanalyyttisin keinoin. Työn on kvalitatiivinen ja siinä on käytetty kirjallista materiaalia, jonka kanssa tutkijalla ei ole ollut vuorovaikutuksessa. Tutkimustulokset osoittavat että on todennäköiseksi, jopa lähes varmaa, että organisaation virallisen kielen vaihtuminen muuttaa organisaation viestintärakennetta. En seurauksena kommunikaatiosuhteet eivät perustu enää osaamiseen tai viralliseen asemaan organisaatiossa. Uudet viestintäverkostot muodostuvat kielitaidon varaan jolloin väistämättä sivutetaan henkilöitä joilla olisi tietämystä, mutta ei kielitaitoa jakaa sitä organisaatiolle. Kansainvälistyminen tuo mukanaan laajemman potentiaalisentietovarannon, joka on mahdollista saada palvelemaan organisaatiota. Näiden kahden vastakkaisen seikan kokonaisvaikutus organisaation tietovarannolle kaipaa lisätutkimusta.

Kirjanpidon luotettavuus

Tutkimuksen tavoitteena on selvittää millainen on luotettava kirjanpito, ja kuinka tilintarkastaja ja verotarkastaja varmistavat kirjanpidon luotettavuuden. Tutkimusmetodologiana käytetään käsiteanalyyttista tutkimusotetta. Tutkimuksessa tarkastellaan, kuinka kirjanpito ja tilinpaatos muodostuvat lakien ja hyvän kirjanpitotavan säätelemänä. Tilinpäätöksen tulee antaa oikeat ja riittävät tiedot yrityksen toiminnan tuloksesta ja taloudellisesta asemasta. Luotettava kirjanpito on ajanmukaista ja täydellistä. Se pitää yrityksen liiketapahtumat erillään yrityksen sidosryhmien liiketapahtumista ja omaisuudesta, täyttää todennettavuuden vaatimukset ja on laadittu sekä varovaisuuden periaatetta että kaikkia muita kirjanpidon yleisiä periaatteita noudattaen. Tilintarkastaja ja verotarkastaja tarkastavat kirjanpidon luotettavuutta. Jokaisella osakeyhtiöllä on velvollisuus toimittaa tilintarkastus. Verotarkastusta ei pystytä toimittamaan kaikissa yhtiöissä jälkiverotusaikana, vaan verotarkastuksella on voimakas virheitä ennaltaehkäisevä vaikutus. Tilintarkastuskertomus on julkinen asiakirja. Yrityksen kaikki sidosryhmät voivat hyödyntää tilintarkastajan lausuntoja. Verotarkastus palvelee lähinnä verotusta. Tilintarkastajan tulee noudattaa työssään hyvää tilintarkastustapaa, verotarkastajan hyvää verotarkastustapaa.

Sosiaalityö ja maahanmuuttajat. Lastensuojelun ammattilaisten ja asiakkaiden vuorovaikutus ja tulkinnat

Tutkimuksen tavoitteena oli tuottaa tietoa siitä, mitä maahanmuuttajia koskevat erityiskysymykset suomalaisessa lastensuojelun sosiaalityössä ovat ja miten näitä kysymyksiä lastensuojelussa käsitellään. Teoreettismetodologisena viitekehyksenä on sosiaalinen konstruktionismi. Etnisten suhteiden tutkimusperinteessä työ paikantuu keskusteluun, jossa kulttuuri ja etnisyys nähdään sosiaalisesti rakentuvina ja muuntuvina. Analyysissä sovelletaan diskurssianalyyttistä metodologiaa. Tutkimus rakentuu yhteenveto-osiosta ja neljästä artikkelista. Maahanmuuttajasosiaalityötä ja lastensuojelua tarkastellaan sosiaalityöntekijöiden, muiden ammattilaisten ja asiakkaiden kielenkäytön kautta. Aineisto koostuu 11 lastensuojelun asiakaskeskustelusta ja niiden jälkeen keskustelun osapuolille tehdyistä haastatteluista, joita on yhteensä 35. Tutkimuksessa analysoidaan seuraavia kysymyksiä: Miten sosiaalityöntekijät tulkitsevat maahanmuuttajasosiaalityön erityisyyttä oman ammatillisen tehtävänsä näkökulmasta? Minkälaisia ominaisuuksia sosiaalityöntekijät rakentavat maahanmuuttaja-asiakkaille? Miten lastensuojelun keskusteluissa puhutaan monikulttuurisuuteen liittyvistä teemoista, kuten erilaisuudesta ja samanlaisuudesta sekä kulttuuri- ja rasismikysymyksistä? Miten maahanmuuttajalasten ja -nuorten osallisuus lastensuojelun asiakaskeskusteluissa rakentuu aikuisten ja lasten itsensä tuottamana? Mitä ja miten maahanmuuttajalapset ja -nuoret puhuvat kokemuksistaan lastensuojelussa ja suomalaisessa yhteiskunnassa? Maahanmuuttajien erityiskysymyksiä ovat kieleen, kulttuuriin ja valtayhteiskunnan toimintaan liittyvät ymmärtämisvaikeudet, kokemukset arkipäivän rasismista sekä perheen ja yhteisön merkittävä, osin ristiriitainen rooli. Lapsilla ja nuorilla kulttuuri on muuntuvaa ja jatkuvien neuvottelujen kohteena. Aineiston lastensuojelutilanteiden taustalla on usein kouluympäristöön liittyviä vaikeuksia. Haastatteluissa lapset kertovat kokemuksistaan ja toimijuudestaan perheeseen, yhteisöön ja kouluun paikantuvissa tilanteissa. Asiakaskeskusteluissa lasten puhuja-asema on usein heikko, jos aikuiset eivät aktiivisesti vahvista sitä. Jotkut lapset ottavat itse vahvan puhuja-aseman. Asiakaskeskusteluissa maahanmuuttajien erityiskysymyksistä puhutaan harvoin eksplisiittisesti. Haastatteluissa sosiaalityöntekijät enemmän tai vähemmän tietoisesti paikantavat maahanmuuttajasosiaalityötä vieraannuttavaan, sopeuttavaan, tasa-arvoistavaan, kulttuuritietoiseen, rasismitietoiseen ja osallistavaan kehykseen. Kehykset nostavat sosiaalityön tavoitteista, menetelmistä ja asiakkaasta keskeisiksi erilaisia asioita. Tulkinnat ovat muuntuvia, vaikka osoittavat myös tiettyä säännönmukaisuutta. Kulttuuri on keskeinen käsite erilaisuuden ja samanlaisuuden ymmärtämiseksi. Sekä työntekijät että asiakkaat perustelevat toivottavia elämäntapoja "omalla kulttuurillaan" ja selittävät ongelmia ”erilaisella kulttuurilla”. Kulttuurin käsitettä voidaan myös käyttää työvälineenä asiakaskeskusteluissa avattaessa asiakkaan omaa näkökulmaa korostavaa dialogia. Perheen ja kulttuurisen yhteisön merkitys on tärkeää arvioida lapsen ja nuoren hyvinvoinnin ja kulttuurisen identiteetin kehittymisen näkökulmasta. Sosiaalityöntekijöillä on merkittävä välittäjän rooli yhtäältä valtayhteiskunnan ja maahanmuuttaja-asiakkaiden, toisaalta vanhempien, yhteisöjen sekä lasten ja nuorten välillä. Lastensuojelussa haasteena on arkipäivän rasismin tiedostaminen sekä siihen pureutuvien työmenetelmien kehittäminen.

Yhteiskuntavastuuraporttien ulkoinen varmentaminen

Tutkimuksen päätavoitteena oli tutkia miten suomalaiset suuret pörssiyritykset ulkoisesti varmentavat yhteiskuntavastuuraporttinsa. Lisäksi tavoitteena oli tutkia miten yritykset arvioivat varmentamisen vaikuttavan raporttien luotettavuuteen. Työn teorian muodosti kansainväliset ja kotimaiset kirjat ja artikkelit. Empiirinen aineisto kerättiin yritysten yhteiskuntavastuuraporteista, yritysten internetsivuilta ja haastatteluilla. Teemahaastatteluja tehtiin neljälle yrityksen edustajalle ja kahdelle tilintarkastusyhteisön ulkoi-selle varmentajalle. Tutkimusmenetelmä oli kvalitatiivinen ja kuvaileva. Yhteiskuntavastuun huomioiminen ja siitä raportoiminen on yleistynyt Suomessa ja maailmalla 2000-luvulla. Yritykset koetaan tänä päivänä merkittäviksi tekijöiksi yhteiskunnassa ja näin ollen yrityksiltä vaaditaan vastuullista ja ehdottoman luotettavaa toimintaa. Vastuun kantamista vaa-ditaan erityisesti kansainvälisiltä yrityksiltä. Sidosryhmät odottavat yritysten yhteiskuntavastuuraporttien tarjoavan luotettavaa tietoa päätöksenteon tueksi. Luotettavuuden ja uskottavuuden lisäämiseksi, jotkut yritykset ovat alkaneet käyttää yhteiskuntavastuuraporttien ulkoista varmennusta. Ulkoisella varmentamisella tarkoitetaan sellaista toimintaa, jossa kolmas riip-pumaton taho varmentaa yrityksen ei-taloudellisen raportin.

Ympäristöteknologioiden verifioinnin mahdollisuudet pilaantuneiden maiden laadukkaan käsittelyn edistämisessä

EU on käynnistämässä ympäristöteknologioiden verifiointijärjestelmää, jonka avulla voidaan tarjota käyttäjille ja sijoittajille riippumatonta tietoa innovatiivisten teknologioiden toimivuudesta ja suorituskyvystä ja parantaa niiden markkina-asemaa. Verifioinnilla tarkoitetaan kolmannen osapuolen suorittamaa prosessia tai mekanismia, jonka avulla tuotteen toiminta ja suorituskyky voidaan todentaa. Kansallinen ympäristöteknologioiden verifiointijärjestelmä on käytössä mm. Yhdysvalloissa ja Kanadassa. Euroopassa järjestelmä otettaneen käyttöön vuonna 2011–2012. Suomessa tehdään nykyisin noin 300 pilaantuneen maan puhdistushanketta koskevaa lupa- ja ilmoituspäätöstä vuosittain. Noin 85 prosentissa kohteista käytetään kunnostusmenetelmänä massanvaihtoa. Massanvaihto tulee ainakin toistaiseksi säilymään yleisimpänä kunnostusmenetelmänä, mutta mm. in situ -menetelmien käytön arvioidaan lisääntyvän. Tämän diplomityön tavoitteena oli arvioida voidaanko verifiointia hyödyntää pilaantuneiden maiden laadukkaan käsittelyn edistämisessä ja voiko verifiointi nopeuttaa innovatiivisten kunnostusmenetelmien markkinoillepääsyä. Aihetta tarkasteltiin mm. kahden erityyppisen pilaantuneen maan ja pohjaveden kunnostusmenetelmän, reaktiivisten seinämien (in situ) ja bitumistabiloinnin (ex situ) kautta. Pilaantuneiden maiden kunnostusmenetelmien toimivuus riippuu monista eri tekijöistä, joista osaa ei voida hallita tai mallintaa luotettavasti. Verifiointi soveltuukin parhaiten laitteiden tai PIMA-menetelmiä yksinkertaisempien puhdistusmenetelmien suorituskyvyn todentamiseen. Verifiointi saattaa kuitenkin hyvin toimia PIMA-kunnostuksen kohdalla esimerkiksi tiedollisena ohjauskeinona. Reaktiivisten seinämien ja bitumistabiloinnin verifioinnin työvaiheet ovat hyvin samankaltaiset, suurimpana erona seinämien kohdalla tulee kuvata myös kohde johon seinämä on asennettu. Reaktiivisten seinämien toiminta on riippuvaista monista ympäristötekijöistä, toisin kuin erillisellä laitteistolla suoritettavan bitumistabiloinnin. Tulosten perusteella voidaan yleistää, että verifiointi soveltuu paremmin ex situ -, kuin in situ -kunnostusmenetelmille.

Short story

Digitoitu 14. 1. 2009

Segmental Durations of Speech

This dissertation considers the segmental durations of speech from the viewpoint of speech technology, especially speech synthesis. The idea is that better models of segmental durations lead to higher naturalness and better intelligibility. These features are the key factors for better usability and generality of synthesized speech technology. Even though the studies are based on a Finnish corpus the approaches apply to all other languages as well. This is possibly due to the fact that most of the studies included in this dissertation are about universal effects taking place on utterance boundaries. Also the methods invented and used here are suitable for any other study of another language. This study is based on two corpora of news reading speech and sentences read aloud. The other corpus is read aloud by a 39-year-old male, whilst the other consists of several speakers in various situations. The use of two corpora is twofold: it involves a comparison of the corpora and a broader view on the matters of interest. The dissertation begins with an overview to the phonemes and the quantity system in the Finnish language. Especially, we are covering the intrinsic durations of phonemes and phoneme categories, as well as the difference of duration between short and long phonemes. The phoneme categories are presented to facilitate the problem of variability of speech segments. In this dissertation we cover the boundary-adjacent effects on segmental durations. In initial positions of utterances we find that there seems to be initial shortening in Finnish, but the result depends on the level of detail and on the individual phoneme. On the phoneme level we find that the shortening or lengthening only affects the very first ones at the beginning of an utterance. However, on average, the effect seems to shorten the whole first word on the word level. We establish the effect of final lengthening in Finnish. The effect in Finnish has been an open question for a long time, whilst Finnish has been the last missing piece for it to be a universal phenomenon. Final lengthening is studied from various angles and it is also shown that it is not a mere effect of prominence or an effect of speech corpus with high inter- and intra-speaker variation. The effect of final lengthening seems to extend from the final to the penultimate word. On a phoneme level it reaches a much wider area than the initial effect. We also present a normalization method suitable for corpus studies on segmental durations. The method uses an utterance-level normalization approach to capture the pattern of segmental durations within each utterance. This prevents the impact of various problematic variations within the corpora. The normalization is used in a study on final lengthening to show that the results on the effect are not caused by variation in the material. The dissertation shows an implementation and prowess of speech synthesis on a mobile platform. We find that the rule-based method of speech synthesis is a real-time software solution, but the signal generation process slows down the system beyond real time. Future aspects of speech synthesis on limited platforms are discussed. The dissertation considers ethical issues on the development of speech technology. The main focus is on the development of speech synthesis with high naturalness, but the problems and solutions are applicable to any other speech technology approaches.

Tuoteryhmän kehitysprojektin optimointi

Tämä diplomityö toteutettiin Sammet Dampers Oy:ltä saatuna toimeksiantona. Yritys haluaa yhä parempia tuloksia tuoteryhmien kehitysprojekteista, jolloin se asettaa vaatimuksia kehitysprojekteissa käytettävälle kehitysprosessille. Yrityksen täytyy optimoida ja systematisoida käytettävää menetelmää, jotta näihin parempiin tuloksiin voidaan päästä. Työn ensimmäisenä tavoitteena on optimoida yrityksen käytössä oleva tuoteryhmien kehitysprojekteissa käytettävä prosessimalli. Tavoitteen mukaisesti työssä luodaan uusi optimoitu tuoteryhmien kehitysprosessimalli, joka vastaa yrityksen tarpeisiin. Tämä uusi malli kirjataan osaksi yrityksen toiminnanohjausjärjestelmää. Työn toisena tavoitteena on käyttää uutta optimoitua prosessimallia kellopeltien tuoteryhmän kehitysprojektissa. Tätä kehitysprojektia käytetään samalla uuden prosessimallin sisäänajamiseen osaksi yrityksen toimintoja.Tämän diplomityön puitteissa kellopeltien kehitysprojektista käydään läpi kehitysprojektin ensimmäinen osio eli vaatimustenmäärittelyprosessi ja esitellään sen tuloksena syntynyt toteutussuunnitelma. Työn tuloksena syntyneen uuden tuoteryhmien kehitysprojektin prosessimallin avulla voidaan saavuttaa merkittäviä parannuksia tarkasteltaessa kehitysprojektin tuloksia ajankäytön, laadun ja kustannusten suhteen.

A proposal for a repertoire of software testing methods

Nowadays software testing and quality assurance have a great value in software development process. Software testing does not mean a concrete discipline, it is the process of validation and verification that starts from the idea of future product and finishes at the end of product’s maintenance. The importance of software testing methods and tools that can be applied on different testing phases is highly stressed in industry. The initial objectives for this thesis were to provide a sufficient literature review on different testing phases and for each of the phases define the method that can be effectively used for improving software’s quality. Software testing phases, chosen for study are: unit testing, integration testing, functional testing, system testing, acceptance testing and usability testing. The research showed that there are many software testing methods that can be applied at different phases and in the most of the cases the choice of the method should be done depending on software type and its specification. In the thesis the problem, concerned to each of the phases was identified; the method that can help in eliminating this problem was suggested and particularly described.

Magnetic Resonance Experiments with Atomic Hydrogen

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

Virtuaalitekniikoiden ja riskianalyysin käyttö kivenmurskainten tuotekehityksessä

Tässä työssä keskitytään Metso Mineralsin valmistamien tuotteiden suunnitteluympäristöön ja erityisesti sen kehittämismahdollisuuksiin uusien teknologioiden avulla. Käyttövarmuuden parantamiseksi yksi potentiaalisimmista keinoista on parantaa laitteiden huollettavuutta. Tyypillisesti huollettavuuden verifiointi tapahtuu vasta prototyyppien testauksessa työmaaolosuhteissa, jolloin havaittujen ongelmien muuttaminen on hankalaa. Siksi huollettavuuteen tulisi kiinnittää enemmän huomiota jo tuotekehitysvaiheessa. Tässä työssä selvitetään virtuaalitekniikoiden tarjoamia mahdollisuuksia em. asioiden parantamiseksi. Työn toisena osakokonaisuutena tutkitaan riskianalyysien kehittämismahdollisuuksia. Tavoitteena on kehittää toimiva menetelmä riskianalyysin suorittamiseen virtuaaliprototyyppien avulla ja testata kaupallisten riskianalyysiin tarkoitettujen sovellusten käyttöä. Lopuksi tarkastellaan vielä uusien menetelmien integrointia osaksi tuotekehitysprosessia. Tehtyjen Case-tutkimusten perusteella havaittiin, että virtuaaliympäristöjen ja -tekniikoiden avulla saavutetaan hyötyä tuotekehityksen varhaisessa vaiheessa. Kyselytutkimuksesta saadun palautteen perusteella virtuaalitekniikoiden sovelluksille annettiin asteikolla 1–5 yleisarvosanaksi keskimäärin kolme. Virtuaalitekniikoiden ja riskianalyysien yhteiskäyttöä testattiin onnistuneesti, mutta tämä vaatii vielä kehittämistä.

Effect of hydrodynamics on modelling, monitoring and control of crystallization

Crystallization is a purification method used to obtain crystalline product of a certain crystal size. It is one of the oldest industrial unit processes and commonly used in modern industry due to its good purification capability from rather impure solutions with reasonably low energy consumption. However, the process is extremely challenging to model and control because it involves inhomogeneous mixing and many simultaneous phenomena such as nucleation, crystal growth and agglomeration. All these phenomena are dependent on supersaturation, i.e. the difference between actual liquid phase concentration and solubility. Homogeneous mass and heat transfer in the crystallizer would greatly simplify modelling and control of crystallization processes, such conditions are, however, not the reality, especially in industrial scale processes. Consequently, the hydrodynamics of crystallizers, i.e. the combination of mixing, feed and product removal flows, and recycling of the suspension, needs to be thoroughly investigated. Understanding of hydrodynamics is important in crystallization, especially inlargerscale equipment where uniform flow conditions are difficult to attain. It is also important to understand different size scales of mixing; micro-, meso- and macromixing. Fast processes, like nucleation and chemical reactions, are typically highly dependent on micro- and mesomixing but macromixing, which equalizes the concentrations of all the species within the entire crystallizer, cannot be disregarded. This study investigates the influence of hydrodynamics on crystallization processes. Modelling of crystallizers with the mixed suspension mixed product removal (MSMPR) theory (ideal mixing), computational fluid dynamics (CFD), and a compartmental multiblock model is compared. The importance of proper verification of CFD and multiblock models is demonstrated. In addition, the influence of different hydrodynamic conditions on reactive crystallization process control is studied. Finally, the effect of extreme local supersaturation is studied using power ultrasound to initiate nucleation. The present work shows that mixing and chemical feeding conditions clearly affect induction time and cluster formation, nucleation, growth kinetics, and agglomeration. Consequently, the properties of crystalline end products, e.g. crystal size and crystal habit, can be influenced by management of mixing and feeding conditions. Impurities may have varying impacts on crystallization processes. As an example, manganese ions were shown to replace magnesium ions in the crystal lattice of magnesium sulphate heptahydrate, increasing the crystal growth rate significantly, whereas sodium ions showed no interaction at all. Modelling of continuous crystallization based on MSMPR theory showed that the model is feasible in a small laboratoryscale crystallizer, whereas in larger pilot- and industrial-scale crystallizers hydrodynamic effects should be taken into account. For that reason, CFD and multiblock modelling are shown to be effective tools for modelling crystallization with inhomogeneous mixing. The present work shows also that selection of the measurement point, or points in the case of multiprobe systems, is crucial when process analytical technology (PAT) is used to control larger scale crystallization. The thesis concludes by describing how control of local supersaturation by highly localized ultrasound was successfully applied to induce nucleation and to control polymorphism in reactive crystallization of L-glutamic acid.

Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.