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.

Relationship marketing in Latin American context: Implications for small Finnish software companies in Latin American B2B partnerships

After a productivity decrease of established national export industries in Finland such as mobile and paper industries, innovative, smaller companies with the intentions to internationalize right from the start have been proliferating. For software companies early internationalization is an especially good opportunity, as Internet usage becomes increasingly homogeneous across borders and software products often do not need a physical distribution channel. Globalization also makes Finnish companies turn to unfamiliar export markets like Latin America, a very untraditional market for Finns. Relationships consisting of Finnish and Latin American business partners have therefore not been widely studied, especially from a new-age software company’s perspective. To study these partnerships, relationship marketing theory was taken into the core of the study, as its practice focuses mainly on establishing and maintaining relationships with stakeholders at a profit, so that the objectives of all parties are met, which is done by a mutual exchange and fulfillment of promises. The most important dimensions of relationship marketing were identified as trust, commitment and attraction, which were then focused on, as the study aims to understand the implications Latin American business culture has for the understanding, and hence, effective application of relationship marketing in the Latin American market. The question to be answered consecutively was how should the dimensions of trust, commitment and attraction be understood in business relationships in Latin America? The study was conducted by first joining insights given by Latin American business culture literature with overall theories on the three dimensions. Through pattern matching, these insights were compared to empirical evidence collected from business professionals of the Latin American market and from the experiences of Finnish software businesses that had recently expanded into the market. What was found was that previous literature on Latin American business culture had already named many implications for the relationship marketing dimensions that were relevant also for small Finnish software firms on the market. However, key findings also presented important new drivers for the three constructs. Local presence in the area where the Latin American partner is located was found to drive or enhance trust, commitment and attraction. High-frequency follow up procedures were in turn found to drive commitment and attraction. Both local presence and follow up were defined according to the respective evidence in the study. Also, in the context of Finnish software firms in relationships with Latin American partners, the national origins or the foreignness of the Finnish party was seen to enhance trust and attraction in the relationship

In vitro production of cattle blastocysts in chemically defined medium with or without insulin supplementation

Selostus: Insuliinin vaikutus naudan blastokystien tuottamiseen in vitro kemiallisesti tunnetussa liuoksessa

Integrated environmental research and networking of economy and information in rural areas of Finland

Selostus: Kestävän kehityksen integroidun tutkimuksen ja verkostotalouden teorian tutkimusmenetelmälliset ongelmat

Calculation of wood volume and stem taper using terrestrial single-image close-range photogrammetry and contemporary software tools

Abstract

Software Process Modeling with Eclipse Process Framework

The software development industry is constantly evolving. The rise of the agile methodologies in the late 1990s, and new development tools and technologies require growing attention for everybody working within this industry. The organizations have, however, had a mixture of various processes and different process languages since a standard software development process language has not been available. A promising process meta-model called Software & Systems Process Engineering Meta- Model (SPEM) 2.0 has been released recently. This is applied by tools such as Eclipse Process Framework Composer, which is designed for implementing and maintaining processes and method content. Its aim is to support a broad variety of project types and development styles. This thesis presents the concepts of software processes, models, traditional and agile approaches, method engineering, and software process improvement. Some of the most well-known methodologies (RUP, OpenUP, OpenMethod, XP and Scrum) are also introduced with a comparison provided between them. The main focus is on the Eclipse Process Framework and SPEM 2.0, their capabilities, usage and modeling. As a proof of concept, I present a case study of modeling OpenMethod with EPF Composer and SPEM 2.0. The results show that the new meta-model and tool have made it possible to easily manage method content, publish versions with customized content, and connect project tools (such as MS Project) with the process content. The software process modeling also acts as a process improvement activity.

Dynamic Runtime Variation and Branding in S60 Software

Diplomityössä tutkitaan keinoja brändätä ja varioida S60-ohjelmistoja dynaamisesti ja ajonaikaisesti. S60 on kehitysalusta, jota käyttävät useat puhelinvalmistajat ja heidän puhelimiaan käyttävät lukuisat eri operaattorit. Operaattorit haluavat puhelimiensa tai osan puhelimen sovelluksista erottuvan kilpailijoista heidän omalla brändillään ja tämän takia täytyy olla keinot joko koko puhelimen, tai valittujen sovellusten brändäykselle. Osa sovelluksista saatetaan haluta vaihtavan käytettyä brändiä sen käyttämien resurssien, kuten verkkopalvelimen, mukaan. Variointidataa tulee myös pystyä jakamaan eri sovellusten tai sovellusten osien kesken. Työssä esitellään Symbian käyttöjärjestelmä ja S60 kehitysympäristö, sekä pohditaan Symbianin turvallisuuskäytäntöjen tuomia haasteita variointidatan jakamiseen eri sovellusten välillä. Olemassaolevia variointitapoja tutkitaan työn mahdolliseksi pohjaksi. Työ sisältää esittelyn projektista, jossa kehitettiin erään S60 sovelluksen dynaaminen brändäystoteutus, joka myös mahdollistaa variointidatan jakamisen eri sovellusten kanssa.

Evaluation of performance analysis software for Linux computing cluster

Tietokonejärjestelmän osien ja ohjelmistojen suorituskykymittauksista saadaan tietoa,jota voidaan käyttää suorituskyvyn parantamiseen ja laitteistohankintojen päätöksen tukena. Tässä työssä tutustutaan suorituskyvyn mittaamiseen ja mittausohjelmiin eli ns. benchmark-ohjelmistoihin. Työssä etsittiin ja arvioitiin eri tyyppisiä vapaasti saatavilla olevia benchmark-ohjelmia, jotka soveltuvat Linux-laskentaklusterin suorituskyvynanalysointiin. Benchmarkit ryhmiteltiin ja arvioitiin testaamalla niiden ominaisuuksia Linux-klusterissa. Työssä käsitellään myös mittausten tekemisen ja rinnakkaislaskennan haasteita. Benchmarkkeja löytyi moneen tarkoitukseen ja ne osoittautuivat laadultaan ja laajuudeltaan vaihteleviksi. Niitä on myös koottu ohjelmistopaketeiksi, jotta laitteiston suorituskyvystä saisi laajemman kuvan kuin mitä yhdellä ohjelmalla on mahdollista saada. Olennaista on ymmärtää nopeus, jolla dataa saadaan siirretyä prosessorille keskusmuistista, levyjärjestelmistä ja toisista laskentasolmuista. Tyypillinen benchmark-ohjelma sisältää paljon laskentaa tarvitsevan matemaattisen algoritmin, jota käytetään tieteellisissä ohjelmistoissa. Benchmarkista riippuen tulosten ymmärtäminen ja hyödyntäminen voi olla haasteellista.

Release Process Effectiveness - Case of Operating Room Management Software

Työn päätavoitteena oli tuoda esiin tärkeimmät julkistamisprosessin tehokkuuteen vaikuttavat tekijät. Tutkimuksessa tarkasteltiin aihetta julkistamisprojektien vetäjän näkökulmasta. Kirjallinen selvitys kattaa keskeisimmät ohjelmistoprosessin, palvelun laadun sekä projektihallinnan teoriat. Kokeellisena aineistona käytettiin asiakkailta ja myynnin sekä käyttöönoton organisaatioilta tullutta palautetta ja asiantuntijahaastatteluita. Case-tuotteena tarkasteltiin suuren kansainvälisen yrityksen jälleenmyymää leikkaussalihallinnan ohjelmistoa. Tärkeimpiä julkistamisprosessin tehokkuuteen vaikuttavia tekijöitä ovat tiekartan ja julkistamispakettien sisällön hallinta, projektin aikataulujen pitäminen, rehellinen ja nopea kommunikaatio myyntikanavaan ja asiakkaille, sekä hyvin toteutettu testaus. Työssä käydään läpi esimerkkistrategioita kehittymiseen näillä alueilla.

Outsourcing and Offshore Software Development in Africa

Globalization of software today is making many companies in the industrialized nations to outsource their work to low-wage countries. This thesis aims at obtaining an initial general overview of offshore software development in Africa. It seeks to explore the state of offshore software outsourcing in Africa with a focus on the factors contributing to the successes and challenges of offshore software development practicesin Africa. The thesis made use of electronic questionnaires and voice interviews to collect the data. Identified African vendors were interviewed, and the data was analyzed qualitatively. The study found that theAfrican software outsourcing industry is still at its infancy. It is expected that the industry will grow. However, a lot needs to be done, and African governments are called upon to actively implement supportive infrastructures that will promote the growth of the local and export software industries. Further research is recommended to cover the wide context ofthe topic.

Production scheduling tools' evaluation in a global telecommunications and electronics company

Tutkimuksen päätavoite on arvioida, ovatko neljä ohjelmistovaihtoehtoa riittäviä tuotannon aikataulutuksen työkaluja ja mikä työkaluista sopii toimeksiantajayritykselle. Alatavoitteena on kuvata tuotannon aikataulutuksen nyky- ja tahtotila prosessimallinnuksen avulla, selvittää työkalun käyttäjätarpeet ja määritellä priorisoidut valintakriteerit työkalulle.Tutkimuksen teoriaosuudessa tutkitaan tuotannon aikataulutuksen logiikkaa ja haasteita. Työssä tarkastellaan aikataulutusohjelmiston valintaa rinnakkain prosessinmallinnuksen kanssa. Aikataulutusohjelmistovaihtoehdot ja metodit käyttäjätarpeiden selvittämiseksi käydään läpi. Empiriaosuudessa selvitetään tutkimuksen suhde toimeksiantajayrityksen strategiaan. Käyttäjätarpeet selvitetään haastattelujen avulla jaanalysoidaan QFD matriisin avulla. Toimeksiantajayrityksen tuotannon aikataulutuksen nyky- ja tahtotilaprosessit mallinnetaan, jotta ohjelmistojen sopivuutta, aikataulutusprosessia tukevana työkaluna voidaan arvioida.Tutkimustuloksena ovatpriorisoidut valintakriteerit aikataulutustyökalulle eli käyttäjätarpeista johdetut tärkeimmät toiminnalliset ominaisuudet, järjestelmätoimittaja-arvio sekä suositukset jatkotoimenpiteistä ja lisätutkimuksesta.

Re-usable ASIC integrationverification software architecture

Mikropiirien valmistus- ja suunnittelutekniikoiden kehittyminen mahdollistaa yhä monimutkaisempien mikropiirien valmistamisen. Piirien verifioinnista onkin tullut prosessin aikaa vievin osa,sillä kompleksisuuden kasvaessa kasvaa verifioinnin tarve eksponentiaalisesti. Vaikka erinäisiä strategioita piirien integroinnin verifiointiin on esitetty, mm. verifioinnin jakaminen koko suunnitteluprosessin ajalle, jopa yli puolet koko piirin suunnitteluun ja valmistukseen käytetystä työmäärästä kuluu verifiointiin. Uudelleenkäytettävät komponentit ovat pääosassa piirin suunnittelussa, mutta verifioinnissa uudelleenkäytettävyyttä ei ole otettu kunnolla käyttöön ainakaan verifiointiohjelmistojen osalta. Tämä diplomityö esittelee uudelleenkäytettävän mikropiirien verifiointiohjelmistoarkkitehtuurin, jolla saadaan verifiointitaakkaa vähennettyä poistamalla verifioinnissa käytettävien ohjelmistojen uudelleensuunnittelun ja toteuttamisen tarvetta.