Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.

New directions in Stochastic Multicriteria Acceptability Analysis

Decisions taken in modern organizations are often multi-dimensional, involving multiple decision makers and several criteria measured on different scales. Multiple Criteria Decision Making (MCDM) methods are designed to analyze and to give recommendations in this kind of situations. Among the numerous MCDM methods, two large families of methods are the multi-attribute utility theory based methods and the outranking methods. Traditionally both method families require exact values for technical parameters and criteria measurements, as well as for preferences expressed as weights. Often it is hard, if not impossible, to obtain exact values. Stochastic Multicriteria Acceptability Analysis (SMAA) is a family of methods designed to help in this type of situations where exact values are not available. Different variants of SMAA allow handling all types of MCDM problems. They support defining the model through uncertain, imprecise, or completely missing values. The methods are based on simulation that is applied to obtain descriptive indices characterizing the problem. In this thesis we present new advances in the SMAA methodology. We present and analyze algorithms for the SMAA-2 method and its extension to handle ordinal preferences. We then present an application of SMAA-2 to an area where MCDM models have not been applied before: planning elevator groups for high-rise buildings. Following this, we introduce two new methods to the family: SMAA-TRI that extends ELECTRE TRI for sorting problems with uncertain parameter values, and SMAA-III that extends ELECTRE III in a similar way. An efficient software implementing these two methods has been developed in conjunction with this work, and is briefly presented in this thesis. The thesis is closed with a comprehensive survey of SMAA methodology including a definition of a unified framework.

Implementing Microsoft .NET Framework for Bitumen-Extranet

Ohjelmistoprojektit pohjautuvat nykyään useasti osittain itsenäisesti suunniteltujen ja; toteutettujen ohjelmakomponenttien yhdistelemiseen. Tällä keinolla voidaan vähentää kehitystyön; viemää aikaa ja kustannuksia, jotta saadaan tuotettua kilpailukykyisempiä ohjelmistoja.; Tässädokumentissa käsitellään komponenttipohjaisen ohjelmistotuotannon näkökulmia ja; Microsoft .NET Framework ympäristöä, joka on kehitysympäristö komponenttipohjaisille; ohjelmistoille. Lisäksi esitellään tapauskohtainen ohjelmistoprojekti extranet-verkon; toteutukseen.

Cross-Border Innovation Support Platform for the SMEs: The Case of St. Petersburg Corridor Region

Työssä tutkitaan eri mekanismeja rajojen ylittävään innovaatioiden edistämiseen pienten ja keskisuurten yritysten näkökulmasta. Case ympäristönä on Kaakkois-Suomen ja Luoteis-Venäjän alueeli Pietarin Corridor. Tavoitteena on löytää tarkemmat määritykset ja rajauksetnäille mekanismeille. Teoriassa muodostettiin viitekehys rajojen ylittävälle innovaatioiden edistämismallille. Mallin pohjalta toteutettiinhaastattelututkimus, joka suoritettiin case-ympäristössä. Haastattelujoukko koostui yritysten edustajista, tutkimus-henkilöstöstä sekä julkisista toimijoista. Innovaatiojärjestelmä oli avoin uusille toimintamenetelmille.Menetelmien toteuttamistapa kuitenkin jakoi mielipiteitä. Toimijoiden välille tarvitaan parempaa yhteistyötä ja tämän kautta selkeämpää kommunikointia yritysten suuntaan. Innovaatioiden edistämiseen ehdotetaan Innovation Relay Centre tyyppisen toiminnan laajentamista Corridorin alueelle sekä sen käyttämän teknologioiden välittämismallin sekä kansainvälisen verkoston hyödyntämistä. Edistämisen tukena tulisi käyttää innovaatiotietokanta-työkalua.

EPCM-toimitustapamallin kehittäminen Kvaerner Power Oy:n voimalaitostoimituksiin

Tämän diplomityön päämääränäoli laatia suunnitelma voimalaitoksen toimittamiseksi EPCM-toimitustavalla. Työn keskeisiksi tavoitteiksi asetettiin EPCM-toimitustapaan perustuvan toimitustapakonseptin muodostaminen, toimituksiin liittyvien terminologian selkeyttäminen ja harmonisointi sekä voimalaitoksen suhteellisen kustannusrakenteen laatiminen. Työssä tutkittiin voimalaitostoimituksissa tavanomaisesti käytettyjä sopimustyyppejä, kiinteähintaista sopimusta ja kustannusvoittolisäsopimusta sekä harvinaisemmin käytettyjä kattohinta- ja tavoitekustannussopimusta. Vallitsevat toimitustavat, EPC- ja EPCM-toimitustavat sekä monitoimittajatapa, esiteltiin ja niiden vahvuudet sekä heikkoudet selvitettiin. Projektin ominaisuuksilla, markkinoilla ja tilaajan kyvyllä, asiantuntemuksella sekä resursseilla todettiin olevan vaikutusta toimitustavan valintaan. Lisäksi tehtiin katsaus voimalaitostoimitusten kehitystrendeihin ja projektin riskienhallintaan. Voimalaitoksen laitosjärjestelmäjako kehitettiin ja sitä soveltamalla määritettiin voimalaitoksen suhteellinen kustannusrakenne. Kattilaitoksen osuus voimalaitoksen rakentamiskustannuksista todettiin merkittävimmäksi. Laitosjärjestelmien laitekustannusten havaittiin olevan korkeimmat. EPCM-toimitustapamalli kehitettiin teoriaosan pohjalta ja sen rakenne, organisaatio, sopimustyypit ja -suhteetsekä toimituksen riskien jako kuvattiin. Voimalaitoksen rakentamiskustannuksia vertailtiin eri toimitustavoilla ja EPCM-toimitustapamalli todettiin EPC-toimitustapaa edullisemmaksi.

Tuotehallinnan kehittämismahdollisuudet puutuoteteollisuuden konetoimittajalla

Työn tavoitteena oli selvittää niitä keinoja, joiden avulla Raute Woodin nykyistä tuotehallintaa pystytään kehittämään. Aluksi kartoitettiin tuotehallinnan kannalta olennaisia työkaluja. Korkean teknologian tuotteet asettavat tuotehallinnalle olennaisesti kovemmat vaatimukset, sillä tuotteen hallinta ei rajoitu pelkästään mekaanisen mallin hallintaan. Jotta tuotteita jatkossa pystyttäisiin hallitsemaan täydellisinä kokonaisuuksina tarvitaan toimintamalli, jonka pohjalta tuotteeseen liittyvät tiedot saadaan hallittua yhtenäisesti.Kehittämistoimenpiteiden lähtökohdaksi kuvattiin tuotehallinnan ja tilaus-toimitusprosessin nykytilanne. Nykytilanteesta etsittiin ne tekijät, jotka vaikuttavat kaikkein suurimmassa määrin havaittuihin tuotehallinnan ongelmiin. Havaittujen ongelmien ja valittujen ratkaisumetodien pohjalta alettiin suunnitella keinoja tuotehallinnan kehittämiseksi. Lopputuloksena esitetään ratkaisuehdotus tuotehallinnan tulevaisuuden hallintamalliksi. Ratkaisuehdotuksessa esitetään teorian pohjalta johdetut mallit tuotteiden kokonaisvaltaiseen hallintaan sekä kuvataan tilaus-toimitusprosessi tuotteen näkökulmasta. Ehdotuksessa kuvataan myös uusi tuotetunnistejärjestelmä, jonka pohjalta tuotteet voidaan jatkossa yksilöidä yksiselitteisesti. Tuotetunnistejärjestelmä tukee työssä kehitettyä uutta modulaarista tuoterakennemallia. Lisäksi esitellään tuotemalliajattelun soveltumista mahdolliseen uuteen tuotehallintaratkaisuun ja sen tuomia uusia mahdollisuuksia toiminnan kehittämiseen.

SAP R/3 -toimimianohjausjärjestelmän käytettävyyden parantaminen metsäteollisuusyrityksessä

Työn tavoitteena on parantaa SAP R/3-järjestelmän käytettävyyttä muutoksenhallintaprosessia mallintamalla. Työn alussa selkeytetään järjestelmän käytön nykytilaa yrityksessä sekä käyttäjien vaatimia parannuskohteita. Työn teoriaosassa käsitellään asiakasnäkökulmasta prosessien kehittämisen sekä niiden mallintamisen teoriaa. Teoriaosassa haetaan vastauksia järjestelmiin liittyviin kysymyksiin: - Kuinka selkeytetään käyttöönottoa sekä hyödynnetään toiminnan prosessilähtöistä kehittämistä? - Kuinka asiakastarpeita kartoittamalla huomioidaan käyttäjien tulevat taipeet? - Miten prosessimallintaminen lisää käyttäjien luottamusta ja yrityksen kilpailukykyä? Soveltavassa osassa tutkitaan vika- ja pienkehityspyyntöjen hallintaa ARIS-mallinnuksen avulla. Toimintoketjun avulla luodaan M-real-konsemissa käyttäjien ja palveluntarjoajan yhteinen toimintamalli. Prosessin omistajuus, käyttäjien liittymäpinta sekä toiminnan organisointi huomioidaan kaikkien osapuolten kesken

Adaptive Protocol Stacks for Mobile Devices

Tulevaisuudessa siirrettävät laitteet, kuten matkapuhelimet ja kämmenmikrot, pystyvät muodostamaan verkkoyhteyden käyttäen erilaisia yhteysmenetelmiä eri tilanteissa. Yhteysmenetelmillä on toisistaan poikkeavat viestintäominaisuudet mm. latenssin, kaistanleveyden, virhemäärän yms. suhteen. Langattomille yhteysmenetelmille on myös ominaista tietoliikenneyhteyden ominaisuuksien voimakas muuttuminen ympäristön suhteen. Parhaan suorituskyvyn ja käytettävyyden saavuttamiseksi, on siirrettävän laitteen pystyttävä mukautumaan käytettyyn viestintämenetelmään ja viestintäympäristössä tapahtuviin muutoksiin. Olennainen osa tietoliikenteessä ovat protokollapinot, jotka mahdollistavat tietoliikenneyhteyden järjestelmien välillä tarjoten verkkopalveluita päätelaitteen käyttäjäsovelluksille. Jotta protokollapinot pystyisivät mukautumaan tietyn viestintäympäristön ominaisuuksiin, on protokollapinon käyttäytymistä pystyttävä muuttamaan ajonaikaisesti. Perinteisesti protokollapinot ovat kuitenkin rakennettu muuttumattomiksi niin, että mukautuminen tässä laajuudessa on erittäin vaikeaa toteuttaa, ellei jopa mahdotonta. Tämä diplomityö käsittelee mukautuvien protokollapinojen rakentamista käyttäen komponenttipohjaista ohjelmistokehystä joka mahdollistaa protokollapinojen ajonaikaisen muuttamisen. Toteuttamalla esimerkkijärjestelmän, ja mittaamalla sen suorituskykyä vaihtelevassa tietoliikenneympäristössä, osoitamme, että mukautuvat protokollapinot ovat mahdollisia rakentaa ja ne tarjoavat merkittäviä etuja erityisesti tulevaisuuden siirrettävissä laitteissa.

Sahan kustannustenjakomalli toimintolaskentaa apuna käyttäen

Työn tavoitteena oli rakentaa sahan kustannuksille laskentamalli, jolla kustannukset voidaan kohdistaa markkinasegmenteille. Työssä käytettiin toimintolaskentaa, joka kohdistaa kustannuksia tarkemmin, kuin perinteiset kustannuslaskentamenetelmät. Toimintolaskenta on kaksivaiheinen menetelmä, jossa ensin resurssit kohdistetaan käytön mukaan toiminnoille ja näiltä edelleen laskentakohteille toimintojen kulutuksen mukaan. Suuri osa mallin rakentamisajasta kului toimintojen määrittelyyn, analysointiin, tiedonhakuun ja laskentainformaation keräämiseen. Rakennettua kustannustenjakomallia voidaan käyttää apuna esim. segmentti-, asete- tai tuotekohtaista kannattavuutta laskettaessa. Kustannustenjakomalli kohdistaa sahan kustannukset kolmelle eri kustannusobjektille. Nämä objektit ovat tuote, segmentti ja tehdas. Tehdastason kustannukset kohdistetaan ainoastaan tuotteiden tehdashintojen määrittämisessä. Nämä kustannukset eivät vaikuta mitenkään tuotteen tai markkinasegmentin kannattavuuteen. Laskentamallin rakenne riippuu mallin käyttötarkoituksesta. Kustannustenjakomallia kokeiltiin kolmelle erilaiselle sahaukselle. Mallissa tarkasteltiin normaalikokoisen tukin, Japanin sahatavaran (lyhyt tukki) ja pienen tukin sahauksia sekä näiden aiheuttamia kustannuksia. Toimintolaskenta soveltuu hyvin sahan kustannusten kohdistamiseen. Koska sahan tuotanto on prosessimaista, niin toimintoja on vähän. Vaikka segmenttitason palvelutoimintojen osuus kustannuksista onkin pieni, niin toimintolaskenta toimii usein todellisena silmien avaajana, kun toimintoja ja niiden kustannuksia analysoidaan.

Siltanosturin mallinnusmenetelmien kehittäminen

Työn tarkoituksena oli selvittää kaupallisen dynamiikan simulointiohjelmiston (Adams) soveltuvuus siltanosturin mallintamiseen. Työn kohteena oli kaksipalkkinen siltanosturi, joka sijaitsi KCI:n tiloissa Hyvinkäällä. Nosturin jänneväli oli noin 19.5 metriä ja nostokyky 16 tonnia. Mallintamisessa keskityttiin nosturin dynamiikkaan sekä ohjausvoimiin nosturin kantopyörissä. Simulointitulokset verifioitiin mittauksin. Koska mallista haluttiin mahdollisimman yksinkertainen, mallinnettiin ainoastaan pääkannattajat ja köydet joustavina. Muut osat mallinnettiin jäykkinä. Yksinkertaisuuteen pyrittiin sen vuoksi, että mallia oli tarkoitus käyttää perustana komponenttikirjaston luomiseksi myöhempää käyttöä varten. Tuloksista todettiin mallin soveltuvan hyvin nosturin dynamiikan mallintamiseen. Mallista saatavat tulokset vastasivat hyvin mitattuja liikkeitä. Ohjausvoimia ei kuitenkaan saatu verifioitua. Käytetty mittausmenetelmä osoittautui sopimattomaksi.

Venttiili- ja toimilaitetehtaan tuotannon suunnittelu

Venttiili- ja toimilaitetehtaassa kokoonpannaan erilaisia venttiilityyppejä sekä toimi- laitteita. Koko Metso Automationin Helsingin tehtaiden tuotantotilanteen muuttuessa käynnistettiin kehitysprojekti, jonka tarkoituksena oli uudenaikaistaa venttiilien ja toimilaitteiden valmistus vastaamaan nykypäivän vaatimuksia. Laajamittaisen osa- valmistuksen ulkoistuksen ja tuotteiston muutoksen vuoksi tuotannon uudelleen- järjestäminen oli välttämätöntä. Diplomityön tarkoituksena oli suunnitella venttiili- ja toimilaitetehtaan layout sekä uutta tuotantotilannetta vastaavat toimintatavat. Haasteena oli kolmen hyvin erilailla toimivan tuotetehtaan yhdistäminen yhdeksi kokonaisuudeksi, jossa kunkin tehtaan parhaat toimintatavat yhdistyvät. Nykyinen tuotanto ja valmistusmäärät kartoitettiin ja analysoitiin, minkä jälkeen tuotannon suunnittelu uusiin tiloihin käynnistettiin. Työ jaettiin järjestelmällisesti osiin teorian ja käytännön osuuksien kesken siten, että teoria tukee työn käytännön- osuutta. Apuna käytettiin useita erilaisia materiaalivirtojen kartoitusmenetelmiä, lukuisia mittareita, selvityksiä, ennusteita ja erilaisia malleja tulevasta tuotannosta. Layout suunniteltiin käytössäolevaan tehdashalliin, mikä aiheutti runsaasti haasteita ja rajoitteita. Aikataulu tehtiin tarkasti siten, että muuttojärjestys lyötiin lukkoon, mutta kuormitustilanne ja koneiden siirrot aiheuttivat muutoksia aikataulussa. Tavoite tuotannon häiriöttömyydestä toteutui hyvin aikataulun kustannuksella. Käytännönosuudessa tarkasteltiin erityisesti kapasiteetin joustavuutta kuormituksen vaihdellessa sekä kehitettiin toimintatavat, joilla se hallitaan. Lisäksi tutkimuksen aikana käynnistettiin useita kehitysprojekteja työn tulosten pohjalta. Näitä olivat erilaiset varaston hallintaan sekä solujen itseohjautuvuuteen liittyvät asiat. Diplomityön tuloksena saatiin uusi layout sekä sitä tukeva uusi toimintatapa, solujen itseohjautuvuuden kehittäminen käynnistettiin, varastojen hallinnan osittainen ulkoistaminen aloitettiin. Lisäksi tuotannolle kehitettiin lukuisia seurantamittareita. Layoutprojekti toteutettiin loppuun diplomityön aikana

Digital Audio Broadcasting: Technology and Prospects

The subject of the thesis was the digital audio broadcasting technology developed in the Eureka project 147. The research was based on the literature on the subject. At first, some reasons for the digitisation of broadcasting technology were given. Next, the channel multiplexing and channel coding methods employed by digital radio were discussed. The design of these methods is based on certain phenomena related to the propagation of radio-frequency signals, and these phenomena were also described. After that, audio and data transfer mechanisms as well as the structure of digital radio network were explained. Furthermore, digital audio and data services were considered. Finally, the digital radio was examined from marketing and administrative aspects. From a merely technical point of view, the digital radio technology offers several improvements in comparison with analogue technology. However, the digital radio has not become as widespread as it was perhaps originally expected during its development.

Tietovirtojen kehittäminen teollisessa valmistusprosessissa

Työn tavoitteena on analysoida ABB Oy:n Indutiokoneet-tulosyksikön tuotantoprosessin loppuosaa tietovirtojen näkökulmasta ja tutkia miten tiedonkulkua tulisi kehittää valmistusprosessin loppupään tehostamiseksi. Teoreettisena viitekehyksessä vertaillaan prosessinkehittämisen koulukuntia jatkuvaa parantamista ja prosessien suunnittelua ja käsitellään prosessin hallintaan ja kehittämiseen tarvittavia tietovirtoja ja niiden käsitteellistämistä sekä prosessinkehitysprojektin vaiheita. Tarkasteltavaa prosessia lähestytään analysoimalla, miten tutkittava osaprosessi toimii tällä hetkellä ja mitä ongelmia prosessin tiedonkulkuun liittyy. Analyysin pohjalta identifioidaan kahdeksan virhettä prosessissa ja virheiden poistamiseksi kehitystoimenpiteet, jotka liittyvät prosessin tekniseen infrastruktuuriin ja tietotekniseen tukeen sekä prosessin henkilöstön ohjeistukseen. Kehitysehdotusten avulla tarkasteltavassa työyksikössä nykyisin suoritettavia, varsinaisia työvaiheita tukevia vaiheita voidaan poistaa, mikä vapauttaa puolipäiväisen työpanoksen muihin tehtäviin ja pakkausprosessin virheiden väheneminen tuo rahallisia säästöjä kuljetuskustannuksissa.

Coolant Flow and Heat Transfer in Pebble-Bed Reactor Core

This thesis gathers knowledge about ongoing high-temperature reactor projects around the world. Methods for calculating coolant flow and heat transfer inside a pebble-bed reactor core are also developed. The thesis begins with the introduction of high-temperature reactors including the current state of the technology. Process heat applications that could use the heat from a high-temperature reactor are also introduced. A suitable reactor design with data available in literature is selected for the calculation part of the thesis. Commercial computational fluid dynamics software Fluent is used for the calculations. The pebble-bed is approximated as a packed-bed, which causes sink terms to the momentum equations of the gas flowing through it. A position dependent value is used for the packing fraction. Two different models are used to calculate heat transfer. First a local thermal equilibrium is assumed between the gas and solid phases and a single energy equation is used. In the second approach, separate energy equations are used for the phases. Information about steady state flow behavior, pressure loss, and temperature distribution in the core is obtained as results of the calculations. The effect of inlet mass flow rate to pressure loss is also investigated. Data found in literature and the results correspond each other quite well, considered the amount of simplifications in the calculations. The models developed in this thesis can be used to solve coolant flow and heat transfer in a pebble-bed reactor, although additional development and model validation is needed for better accuracy and reliability.

Kehitystoiminnan (RTD) systematisointi vaiheittaisen etenemisen ja portfoliojohtamisen avulla

Kehitystoimintaan liittyvä termi, innovaatio, voidaan määritellä monella eri tavalla. Riippumatta tarkasta määritelmästä innovaatioiden johtaminen voidaan määritellä prosessiksi, jossa eri suoritusvaiheet seuraavat toisiaan. Olennaista on erottaa innovaatioprosessin alkupää ja varsinainen kehitysprojekti toisistaan. Innovaatioprosessin alkupää mielletään usein sumeaksi ja vaikeasti hallittavaksi, kun taas kehitysprojektin johtamiseen on kehitetty systemaattisia menetelmiä, esimerkiksi Stage-Gate-prosessi. Kehitysprojektien johtamisessa ongelmaksi muodostuu resurssien riittämättömyys mahdollisiin projekteihin nähden. Tämä liittää kehitystoiminnan kiinteästi portfoliojohtamiseen. RTD-toiminnalla tarkoitetaan UPM Timberissä kehitystoimintaa, joka sisältää tuotekehityksen lisäksi myös prosessien ja teknologian kehitystoiminnot. UPM Timberiltä on puuttunut systemaattinen toimintamalli RTD-projektien läpiviemiseksi eikä niiden valintaan ja resurssien allokointiin ole ollut järjestelmää. Tutkimuksessa määritetään RTD-toiminnan kriittiset menestystekijät sekä muodostetaan UPM Timberille RTD-toiminnan kehityshaasteet. Niiden perusteella luodaan UPM Timberille systemaattinen toimintamalli, RTD-prosessikuvaus, RTD-projektien läpiviemiseksi sekä integroidaan portfoliojohtaminen toimintamalliin.