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.

Long-term fertilizer field trials: comparison of three mathematical response models

Selostus: Lannoituksen pitkäaikaiset kenttäkokeet: kolmen matemaattisen mallin vertailu

Calibration of a desktop scanner and digital image analysis procedure for quantification of a root morphology

Selostus: Tasoskannerin ja digitaalisen kuva-analyysimenetelmän kalibrointi juurten morfologian kvantifioimiseksi

Stress intensity factor of wood from crack-tip displacement fields obtained from digital image processing

Abstract

Individual tree measurements by means of digital aerial photogrammetry

University of Helsinki, Faculty of Agriculture and Forestry, Department of Forest Resource Management

Three mathematical models for bucking-to-order

Abstract

Designing Digital Filters for Servo Systems

The aim of this work was to select an appropriate digital filter for a servo application and to filter the noise from the measurement devices. Low pass filter attenuates the high frequency noise beyond the specified cut-off frequency. Digital lowpass filters in both IIR and FIR responses were designed and experimentally compared to understand their characteristics from the corresponding step responses of the system. Kaiser Windowing and Equiripple methods were selected for FIR response, whereas Butterworth, Chebyshev, InverseChebyshev and Elliptic methods were designed for IIR case. Limitations in digital filter design for a servo system were analysed. Especially the dynamic influences of each designed filter on the control stabilityof the electrical servo drive were observed. The criterion for the selection ofparameters in designing digital filters for servo systems was studied. Control system dynamics was given significant importance and the use of FIR and IIR responses in different situations were compared to justify the selection of suitableresponse in each case. The software used in the filter design was MatLab/Simulink® and dSPACE's DSP application. A speed controlled Permanent Magnet Linear synchronous Motor was used in the experimental work.

Synchronous Digital Hierarchy implementation to a Radio Transmission Node

Kiristyville markkinoille on aina tuotava jotain uutta tarjottavaa ja SDH-kortti on yksi sellainen tuote jonka Nokia Networks julkistaa osaksi uutta Nokia Flexihub Nodea. Tavoitteena on suunnitella VC-12kanavoitu STM-1 kortti yhdistämään ylemmän tason tietoliikenneverkko suuren kapasiteetin radioon. Ennen kuin markkinoilla on valmis tuote, on sen takana valtaisa määrä työtä. Erilaisia dokumentteja on pitänyt tuottaa ja sopimuksia tehdä. Esimerkiksi vaatimusmäärittelyt on oltava selvät, jotta tiedetään mitä tuotteelta halutaan. Tätä ennen on kuitenkin pitänyt ymmärtää miten SDHtoimii ja miten otsikkotavuja käsitellään. Myös erilaiset piirivalinnat aiheuttavat miettimistä, sillä markkinoilla on runsaasti valmiita piirejä SDH signaalinkäsittelyyn. Varma tiedonsiirto on tärkeää puhelinoperaattorille ja siksi joudutaan miettimään varmennuksia ja niiden toteuttamista. Myös synkronointi on tärkeä osa SDH järjestelmää ja sen toteuttaminen hyvin on tärkeää. Hälytykset on otettava huomioon ja mietittävä, miten niiden käsittely saadaan hoidettua järkevästi, ilman että mikään järjestelmän osa ruuhkautuu kohtuuttomasti. Tässä Diplomityössä on tutustuttu SDH-järjestelmään, otsikkotavujen käsittelyyn ja vaatimusmäärittelyihin.

Embedding, Extraction and Detection of Digital Watermark in Spectral Images

Tässä diplomityössä tutkitaan tekniikoita, joillavesileima lisätään spektrikuvaan, ja menetelmiä, joilla vesileimat tunnistetaanja havaitaan spektrikuvista. PCA (Principal Component Analysis) -algoritmia käyttäen alkuperäisten kuvien spektriulottuvuutta vähennettiin. Vesileiman lisääminen spektrikuvaan suoritettiin muunnosavaruudessa. Ehdotetun mallin mukaisesti muunnosavaruuden komponentti korvattiin vesileiman ja toisen muunnosavaruuden komponentin lineaarikombinaatiolla. Lisäyksessä käytettävää parametrijoukkoa tutkittiin. Vesileimattujen kuvien laatu mitattiin ja analysoitiin. Suositukset vesileiman lisäykseen esitettiin. Useita menetelmiä käytettiin vesileimojen tunnistamiseen ja tunnistamisen tulokset analysoitiin. Vesileimojen kyky sietää erilaisia hyökkäyksiä tarkistettiin. Diplomityössä suoritettiin joukko havaitsemis-kokeita ottamalla huomioon vesileiman lisäyksessä käytetyt parametrit. ICA (Independent Component Analysis) -menetelmää pidetään yhtenä mahdollisena vaihtoehtona vesileiman havaitsemisessa.

Value Sales Approach in Digital Printing

Digitaalinen tulostus osana informaatiologistiikan toimialaa elää murroskautta kovankilpailun ja palveluiden kehittymisen myötä. Moderni teknologia mahdollistaa uudenlaisia älykkäitä palveluita, jotka antavat lisäarvoa niin yritysasiakkaille kuin kuluttajillekin. Siten myös myyntiprosesseja kehitetään tukemaan arvon luontia. Tutkimuksen teoreettisessa osuudessa sovellettiin arvon luomiseen ja myymiseen liittyviä keskeisiä teorioita, sekä organisaation ostokäyttäytymisen ja suhdemarkkinoinnin asioita. Empiirinen tutkimus toteutettiin asiakas- ja asiantuntijahaastatteluiden sekä kansainvälisten koulutuspäivien avulla. Työn tavoitteena oli luoda teoreettisen ja empiirisen tutkimuksen tulosten pohjalta ohjeistus digitaalisen tulostuksen palveluiden arvomyyntiin. Lisäksi työssä käsiteltiin myyntiprosessiin liittyviä kysymyksiä alan ominaispiirteet huomioon ottaen.