Factors Related to Study Success at Lappeenranta University of Technology

Tutkimuksen avulla selvitettiin opintomenestykseen liittyviä tekijöitä Lappeenrannan teknillisessä korkeakoulussa (LTKK). Tutkimus liittyi opetuksen ja oppimisen kehitystyöhön tuotantotalouden osastolla. Tutkimuksen viitekehyksen muodosti oppimistuloksia selittävä malli, joka on laadittu Tynjälän (1999) kokoaman mallin perusteella. Tutkimuksen perusjoukko muodostui LTKK:n läsnä olevista perusopiskelijoista lukuun ottamatta jatko- ja vaihto-opiskelijoita. Opiskelijat jaettiin ositetulla otannalla ryhmiin, joissa suoritettiin yksinkertainen satunnaisotanta. Otoskoko oli 645 opiskelijaa. Tiedonkeruumenetelmänä oli Internet-kysely. Aineisto analysoitiin useiden kvantitatiivisten ja kvalitatiivisten menetelmien avulla. Tutkimuksen tuloksia voidaan pitää luotettavina ja tutkimuksen avulla saatiin tärkeää ja hyödyllistä tietoa opintomenestyksestä ja oppimisprosesseista. Tulosten perusteella merkittävimmät oppimistuloksiin positiivisesti liittyvät tekijät ovat syväsuuntautunut opiskelustrategia ja luottaminen omiin kykyihin, ja negatiiviset tekijät ovat oppimisen itsesäätelyn puute, omien kykyjen epäily ja pintasuuntautunut opiskelustrategia. Merkitysorientoituneet, itsesäätelykykyiset opiskelijat menestyivät LTKK:ssa parhaiten.

Mother-offspring competition promotes colonization success.

Colonization is the crucial process underlying range expansions, biological invasions, and metapopulation dynamics. Which individuals leave their natal population to colonize empty habitats is a crucial question and is presently unresolved. Dispersal is the first step in colonization. However, not all dispersing individuals are necessarily good colonizers. Indeed, in some species, the phenotype of dispersers differs depending on the selective pressures that induce dispersal. In particular, kin-based interactions, a factor driving social evolution, should induce different social response profiles in nondispersing and dispersing individuals. Kin competition (defined here as between the mother and offspring) has been proven to produce dispersers with a particular phenotype that may enhance their colonizing ability. By using the common lizard (Lacerta vivipara), we conducted a multipopulation experiment to study the effect of kin competition on dispersal and colonization success. We manipulated mother-offspring interactions, which are the most important component of kin competition in the studied species, at the family and population levels and measured the consequences on colonization success. We demonstrate that mother-offspring competition at the population level significantly influences colonization success. Increased competition at the population level enhanced the colonization rate of the largest juveniles as well as the growth and survival of the colonizers. Based on these results, we calculated that kin-induced colonization halves the extinction probability of a newly initiated population. Because interactions between relatives are likely to affect the ability of a species to track habitat modifications, kin-based dispersal should be considered in the study of invasion dynamics and metapopulation functioning.

Tuotannon kehitysinvestointiprojektien läpivientimalli

Tämän diplomityön tarkoituksena oli tutkia ja etsiä kehityskohteita kohdeyrityksen kehitysinvestointiprojektien toimintamallissa. Diplomityön tavoitteena oli tutkia nykyistä investointikäytäntöä ja luoda eri linjastoissa tehtäville kehitysinvestointiesityksille edellytykset tukea yhteisesti yrityksen tulevia suhdannenäkymiä ja strategiaa. Työn tavoitteena oli myös pyrkiä välillisesti kasvattamaan investointiin sijoitettavan pääoman tuottoprosenttia pienentämällä kustannuksia huolellisen valmistelun keinoin jo investointiprojektin kehityksen alkuvaiheessa. Työkaluksi tähän todettiin olevan läpivientimalli. Tutkimusmenetelminä käytettiin kvantitatiivisia ja kvalitatiivisia tiedonkeruumenenelmiä. Näistä ylemmän johdon ja keskijohdon haastattelut, sekä omat kokemukset yrityksen käytännöistä vuosilta 2004-2008 näyttelivät pääroolia. Työn tuotoksena laadittiin aiheeseen liittyvä ohjeistus ja läpivientimalli osaksi yrityksen laatujärjestelmää. Malli sijoitettiin template tyyppisesti dokumentinhallinnointiohjelmistoon. Työn tuloksena on esitetty kehitysinvestointiprojektien läpivientimalli siten, että se tukee yrityksen strategiaa kestävän kehityksen ympäröimänä. Työlle asetetut tavoitteet saavutettiin sille tarkoitetussa aikavälissä.

Defining a framework model to determine total costs of managed desktops using ITIL best practices

In modern day organizations there are an increasing number of IT devices such as computers, mobile phones and printers. These devices can be located and maintained by using specialized IT management applications. Costs related to a single device accumulate from various sources and are normally categorized as direct costs like hardware costs and indirect costs such as labor costs. These costs can be saved in a configuration management database and presented to users using web based development tools such as ASP.NET. The overall costs of IT devices during their lifecycle can be ten times higher than the actual purchase price of the product and ability to define and reduce these costs can save organizations noticeable amount of money. This Master’s Thesis introduces the research field of IT management and defines a custom framework model based on Information Technology Infrastructure Library (ITIL) best practices which is designed to be implemented as part of an existing IT management application for defining and presenting IT costs.

Future trends of Finnish cement based construction

The construction material sector, as a capital intensive industry, is highly vulnerable to rapid fluctuations in the economic cycles. In Finland this was witnessed especially during the late 2000s, as in 2007 and 2008 the demand for several construction materials exceeded their supply and right after this, in 2009 the demand collapsed fast as a result of an international recession. These factors brought about the need to study the future trends of the market place of the commissioning company, Finnsementti Oy. As reliable short term market forecasts for the sector are difficult to compose, the study concentrates primarily in examining and identifying the trends that are likely to affect the Finnish cement industry, and as an extension, the concrete industry in a frame of 10 to 15 years. The study’s scope comprehends also the examination of the domestic construction sector, as it represents the end user industry of both cement and concrete. These motives for the study produce the research problem, which is to conduct a trend analysis for cement based building in the Finnish market area in the 2020s. The theoretical frame for composing a trend analysis in the case of this study is twofold. This is due to the fact that both, the macro and micro environments of the examined industries are studied. The main methods used are the PESTE-model (macro) and Porter’s five forces model (micro). The study applies a qualitative approach and the data is gathered by interviewing a group of experts from the cement, concrete and construction industries. The result of the paper is an overall trend analysis for the Finnish cement based building sector, which is based on ‘sub trend analyses’ concerning four identified sub-sectors of the Finnish construction industry. The results are a combination of findings from these sub-sectors and the analyzed data that deals with the studied sector’s macro and micro environment. The conclusions provide an overall picture of the examined sectors’ potential future as a whole and by defined sub-sectors of the construction industry. The recognition of future trends in different areas of the construction industry can be applied as a means for an industry actor’s decision making and in estimating the types of construction that are likely to grow or decline. Finally, based on the analyzed data and conclusions, the commissioning company is provided with a brief SWOT analysis, that provides additional tools for decision making and planning processes regarding the future.

Kunnossapitopalveluiden arvopohjaisen elinkaarimallin kehittäminen

Tutkimuksen päätavoitteena on luoda yleispätevä elinkaarimalli, jota voidaan hyö-dyntää laitetason kunnossapitoon liittyvissä päätöksentekotilanteissa eri teollisuu-denaloilla. Elinkaarimalliin yhdistettiin arvoajattelu, jonka pohjalta mallin käyttäjät voivat valita ja painottaa omien näkemyksiensä mukaan arvoa luovat elementit sekä nähdä muille verkostojäsenille arvoa lisäävät tekijät. Aiemmissa elinkaarimalleissa on keskitytty pääasiassa yhteen tarkastelunäkökulmaan, joten verkostotason työkalulle on selkeä tarve. Myöskään arvoajattelua ei ole aiemmin yhdistetty elinkaarilaskentaa soveltaviin malleihin. Työn osalta käytettiin konstruktiivista tutkimusotetta. Elinkaarimallia kehitettiin ja testattiin kaivosteollisuuden yritysverkostoon kuuluvien kahden case-tapauksen avulla. Tutkimuksen teoreettinen osa pohjautui työn oleellisempiin osa-alueisiin, kuten kunnossapitoon, arvoelementteihin ja elinkaarilaskentaan. Työn empiirisessä osiossa hyödynnettiin verkostoon kuuluvien yritysedustajien haastatteluita sekä yritysten tietojärjestelmästä saatuja tietoja. Arvoelementtien muodostuksessa käy-tettiin hyväksi myös muiden teollisuusyritysten ajatuksia ja näkökulmia. Työn merkittävin tulos on ensimmäisen version kehittäminen arvopohjaisesta elinkaarimallista. Elinkaarimalli antaa tuloksina jokaisen verkostojäsenen osalta laitteen kunnossapidon kustannukset ja tuotot vuositasolla sekä kumulatiivisesti koko elinkaaren ajalta niin reaali- kuin nykyarvonakin. Mallin tuloksena saadaan myös yhteistyön myötä kasvaneen lisäarvon suuruus ja jakautuminen verkoston toimijoiden välillä heidän valitsemiensa arvoelementtien mukaisesti. Näin ollen mallia voidaan käyttää tulevaisuuden ennustamisen lisäksi menneiden kustannusten ja tuottojen seurantamallina. Kokonaisuudessaan arvopohjaisen elinkaarimallin tuloksia voidaan hyödyntää laitetason kunnossapitoon liittyvissä sopimusneuvotte-luissa niin arvoa luovien elementtien kuin kustannus- ja tuottotekijöidenkin osalta. Kokonaisuudessaan arvoajattelun yhdistäminen ja hyödyntäminen elinkaarilas-kennassa on vielä alkuvaiheessa, joten kyseinen osa-alue onkin varsin järkevä jat-kotutkimuskohde. Avoimen ja tiiviin yritysyhteistyön kautta saadaan arvopohjai-sesta elinkaarimallista jatkokehitettyä erittäin hyödyllinen työkalu yritysverkosto-jen käytettäväksi. Kiristyvässä kilpailussa verkoston kokonaisarvon kasvu ja ja-kautuminen ovat tulevaisuudessa erittäin keskeisiä aihealueita, joten tämäntyylisten verkostotyökalujen hyödyntäminen nostanee ehdottomasti suosiotaan.

Tuotemallin ylläpito- ja pienkehitysprosessin kehittäminen

Työn tavoitteena oli selvittää yrityksen tuotekehitysorganisaation tuoteylläpitotoiminnan nykytila ja kartoittaa sen mahdolliset ongelmakohdat sekä kehityskohteet. Lisäksi tavoitteena oli vertailla yrityksen toimintamalleja toisen yrityksen vastaavaan organisaatioon kartoitettujen ongelmakohtien pohjalta, ja laatia kehitysehdotus ongelmien ratkaisemiseksi. Tutkimusmenetelminä käytettiin nykytilaselvityksessä semistrukturoituja asiantuntijahaastatteluja ja vertailututkimusta (engl. benchmarking). Kehitysehdotuksen laatimisen tueksi työhön sisältyi myös kirjallisuuskatsaus, jossa käsiteltiin esimerkiksi tuotteen elinkaarenhallintaa, konfiguraationhallintaa ja prosessijohtamista. Nykytilaselvityksen tuloksena oli kuvaus yrityksen tuoteylläpidontoiminnasta sekä havaituista ongelmakohdista. Vertailututkimuksen tuloksena saatiin kuvaus kohdeyrityksen kartoitettuihin ongelmakohtiin liittyvistä toimintamalleista, sekä joitain ratkaisuvaihtoehtoja. Nykytilaselvityksen ja vertailututkimuksen tulosten sekä kirjallisuuskatsauksen perusteella laadittu kehitysehdotus perustuu konfiguraationhallintasuunnitelman pohjaan, johon on sisällytetty kaikki ratkaisuehdotukset. Kehitysehdotuksessa esitetyt ratkaisuehdotukset vastaavat lähtökohtaisesti kartoitettuihin ongelmakohtiin, mutta ne vaativat vielä jatkokehittelyä. Työn tulokset toimivat pohjana yksityiskohtaisemmalle suunnittelulle ja jatkokehittelylle.

Reusable formal architectures for networked systems

Today's networked systems are becoming increasingly complex and diverse. The current simulation and runtime verification techniques do not provide support for developing such systems efficiently; moreover, the reliability of the simulated/verified systems is not thoroughly ensured. To address these challenges, the use of formal techniques to reason about network system development is growing, while at the same time, the mathematical background necessary for using formal techniques is a barrier for network designers to efficiently employ them. Thus, these techniques are not vastly used for developing networked systems. The objective of this thesis is to propose formal approaches for the development of reliable networked systems, by taking efficiency into account. With respect to reliability, we propose the architectural development of correct-by-construction networked system models. With respect to efficiency, we propose reusable network architectures as well as network development. At the core of our development methodology, we employ the abstraction and refinement techniques for the development and analysis of networked systems. We evaluate our proposal by employing the proposed architectures to a pervasive class of dynamic networks, i.e., wireless sensor network architectures as well as to a pervasive class of static networks, i.e., network-on-chip architectures. The ultimate goal of our research is to put forward the idea of building libraries of pre-proved rules for the efficient modelling, development, and analysis of networked systems. We take into account both qualitative and quantitative analysis of networks via varied formal tool support, using a theorem prover the Rodin platform and a statistical model checker the SMC-Uppaal.

Statistical analysis of survey-based event history data with application to modeling of unemployment duration

Longitudinal surveys are increasingly used to collect event history data on person-specific processes such as transitions between labour market states. Surveybased event history data pose a number of challenges for statistical analysis. These challenges include survey errors due to sampling, non-response, attrition and measurement. This study deals with non-response, attrition and measurement errors in event history data and the bias caused by them in event history analysis. The study also discusses some choices faced by a researcher using longitudinal survey data for event history analysis and demonstrates their effects. These choices include, whether a design-based or a model-based approach is taken, which subset of data to use and, if a design-based approach is taken, which weights to use. The study takes advantage of the possibility to use combined longitudinal survey register data. The Finnish subset of European Community Household Panel (FI ECHP) survey for waves 1–5 were linked at person-level with longitudinal register data. Unemployment spells were used as study variables of interest. Lastly, a simulation study was conducted in order to assess the statistical properties of the Inverse Probability of Censoring Weighting (IPCW) method in a survey data context. The study shows how combined longitudinal survey register data can be used to analyse and compare the non-response and attrition processes, test the missingness mechanism type and estimate the size of bias due to non-response and attrition. In our empirical analysis, initial non-response turned out to be a more important source of bias than attrition. Reported unemployment spells were subject to seam effects, omissions, and, to a lesser extent, overreporting. The use of proxy interviews tended to cause spell omissions. An often-ignored phenomenon classification error in reported spell outcomes, was also found in the data. Neither the Missing At Random (MAR) assumption about non-response and attrition mechanisms, nor the classical assumptions about measurement errors, turned out to be valid. Both measurement errors in spell durations and spell outcomes were found to cause bias in estimates from event history models. Low measurement accuracy affected the estimates of baseline hazard most. The design-based estimates based on data from respondents to all waves of interest and weighted by the last wave weights displayed the largest bias. Using all the available data, including the spells by attriters until the time of attrition, helped to reduce attrition bias. Lastly, the simulation study showed that the IPCW correction to design weights reduces bias due to dependent censoring in design-based Kaplan-Meier and Cox proportional hazard model estimators. The study discusses implications of the results for survey organisations collecting event history data, researchers using surveys for event history analysis, and researchers who develop methods to correct for non-sampling biases in event history data.

Long-term nutrient load management and lake restoration: Case of Säkylän Pyhäjärvi (SW Finland)

Eutrophication caused by anthropogenic nutrient pollution has become one of the most severe threats to water bodies. Nutrients enter water bodies from atmospheric precipitation, industrial and domestic wastewaters and surface runoff from agricultural and forest areas. As point pollution has been significantly reduced in developed countries in recent decades, agricultural non-point sources have been increasingly identified as the largest source of nutrient loading in water bodies. In this study, Lake Säkylän Pyhäjärvi and its catchment are studied as an example of a long-term, voluntary-based, co-operative model of lake and catchment management. Lake Pyhäjärvi is located in the centre of an intensive agricultural area in southwestern Finland. More than 20 professional fishermen operate in the lake area, and the lake is used as a drinking water source and for various recreational activities. Lake Pyhäjärvi is a good example of a large and shallow lake that suffers from eutrophication and is subject to measures to improve this undesired state under changing conditions. Climate change is one of the most important challenges faced by Lake Pyhäjärvi and other water bodies. The results show that climatic variation affects the amounts of runoff and nutrient loading and their timing during the year. The findings from the study area concerning warm winters and their influences on nutrient loading are in accordance with the IPCC scenarios of future climate change. In addition to nutrient reduction measures, the restoration of food chains (biomanipulation) is a key method in water quality management. The food-web structure in Lake Pyhäjärvi has, however, become disturbed due to mild winters, short ice cover and low fish catch. Ice cover that enables winter seining is extremely important to the water quality and ecosystem of Lake Pyhäjärvi, as the vendace stock is one of the key factors affecting the food web and the state of the lake. New methods for the reduction of nutrient loading and the treatment of runoff waters from agriculture, such as sand filters, were tested in field conditions. The results confirm that the filter technique is an applicable method for nutrient reduction, but further development is needed. The ability of sand filters to absorb nutrients can be improved with nutrient binding compounds, such as lime. Long-term hydrological, chemical and biological research and monitoring data on Lake Pyhäjärvi and its catchment provide a basis for water protection measures and improve our understanding of the complicated physical, chemical and biological interactions between the terrestrial and aquatic realms. In addition to measurements carried out in field conditions, Lake Pyhäjärvi and its catchment were studied using various modelling methods. In the calibration and validation of models, long-term and wide-ranging time series data proved to be valuable. Collaboration between researchers, modellers and local water managers further improves the reliability and usefulness of models. Lake Pyhäjärvi and its catchment can also be regarded as a good research laboratory from the point of view of the Baltic Sea. The main problem in both of them is eutrophication caused by excess nutrients, and nutrient loading has to be reduced – especially from agriculture. Mitigation measures are also similar in both cases.

Kaukolämmön hinnoittelumallien optimointi ja kehittäminen muuttuvassa toimintaympäristössä

Kaukolämpöliiketoiminnan kehittämistarve korostuu jatkuvasti alan rakennemuutosten ja markkinoiden muutoksien seurauksena. Turku Energian tavoitteena on uudistaa ja kehittää kaukolämmön hinnoitteluaan vastaamaan energian tuotannon, jakelun, loppukäytön ja muihin alan muutoksiin. Tässä opinnäytetyössä tutkitaan kaukolämmön hinnoittelun optimointi ja kehittämistä nykyisessä sekä tulevaisuuden markkina- ja tuotantorakenteessa. Nykyisen hinnoittelumallin lisäksi tutkitaan vaihtoehtoisia tapoja hinnoitella myytävä kaukolämpöenergia, kuten vuodenaikojen mukaan määriteltävä muuttuva energianhinta. Työn kirjallisuusosassa esitellään kaukolämmön tuotanto, siirto ja jakelu sekä liiketoiminta Suomessa ja Turun seudulla. Tutkittavat hinnoittelumallit perustuvat todellisiin ja arvioituihin liiketoiminnan kustannuksiin, sekä esitettyihin laskentaperiaatteisiin. Turku Energian nykyistä perusmaksun hintatasoa tulee korottaa, jotta se vastaa lämmönhankinnan kiinteitä kustannuksia tarkemmin ja minimoi liiketoiminnan markkinariskiä. Nykyisen hinnoittelun verokomponentin kehittämisellä lisätään hinnoittelun läpinäkyvyyttä. Kausihinnoittelun avulla energianhinta noudattaa tuotannon kustannuksia vuoden aikana ja ohjaa asiakkaiden lämmönkulutusta nykyistä tarkemmin. Uusiutuvilla energianlähteillä tuotettua kaukolämpöä voidaan myydä erillisillä tuotteilla, joiden avulla liiketoiminnalle saadaan lisäarvoa.

Influence of multi-phase phenomena on semibatch crystallization processes of aqueous solutions

Crystal properties, product quality and particle size are determined by the operating conditions in the crystallization process. Thus, in order to obtain desired end-products, the crystallization process should be effectively controlled based on reliable kinetic information, which can be provided by powerful analytical tools such as Raman spectrometry and thermal analysis. The present research work studied various crystallization processes such as reactive crystallization, precipitation with anti-solvent and evaporation crystallization. The goal of the work was to understand more comprehensively the fundamentals, phenomena and utilizations of crystallization, and establish proper methods to control particle size distribution, especially for three phase gas-liquid-solid crystallization systems. As a part of the solid-liquid equilibrium studies in this work, prediction of KCl solubility in a MgCl2-KCl-H2O system was studied theoretically. Additionally, a solubility prediction model by Pitzer thermodynamic model was investigated based on solubility measurements of potassium dihydrogen phosphate with the presence of non-electronic organic substances in aqueous solutions. The prediction model helps to extend literature data and offers an easy and economical way to choose solvent for anti-solvent precipitation. Using experimental and modern analytical methods, precipitation kinetics and mass transfer in reactive crystallization of magnesium carbonate hydrates with magnesium hydroxide slurry and CO2 gas were systematically investigated. The obtained results gave deeper insight into gas-liquid-solid interactions and the mechanisms of this heterogeneous crystallization process. The research approach developed can provide theoretical guidance and act as a useful reference to promote development of gas-liquid reactive crystallization. Gas-liquid mass transfer of absorption in the presence of solid particles in a stirred tank was investigated in order to gain understanding of how different-sized particles interact with gas bubbles. Based on obtained volumetric mass transfer coefficient values, it was found that the influence of the presence of small particles on gas-liquid mass transfer cannot be ignored since there are interactions between bubbles and particles. Raman spectrometry was successfully applied for liquid and solids analysis in semi-batch anti-solvent precipitation and evaporation crystallization. Real-time information such as supersaturation, formation of precipitates and identification of crystal polymorphs could be obtained by Raman spectrometry. The solubility prediction models, monitoring methods for precipitation and empirical model for absorption developed in this study together with the methodologies used gives valuable information for aspects of industrial crystallization. Furthermore, Raman analysis was seen to be a potential controlling method for various crystallization processes.

Computational models for and from biology : simple gene assembly and reaction systems

The advancement of science and technology makes it clear that no single perspective is any longer sufficient to describe the true nature of any phenomenon. That is why the interdisciplinary research is gaining more attention overtime. An excellent example of this type of research is natural computing which stands on the borderline between biology and computer science. The contribution of research done in natural computing is twofold: on one hand, it sheds light into how nature works and how it processes information and, on the other hand, it provides some guidelines on how to design bio-inspired technologies. The first direction in this thesis focuses on a nature-inspired process called gene assembly in ciliates. The second one studies reaction systems, as a modeling framework with its rationale built upon the biochemical interactions happening within a cell. The process of gene assembly in ciliates has attracted a lot of attention as a research topic in the past 15 years. Two main modelling frameworks have been initially proposed in the end of 1990s to capture ciliates’ gene assembly process, namely the intermolecular model and the intramolecular model. They were followed by other model proposals such as templatebased assembly and DNA rearrangement pathways recombination models. In this thesis we are interested in a variation of the intramolecular model called simple gene assembly model, which focuses on the simplest possible folds in the assembly process. We propose a new framework called directed overlap-inclusion (DOI) graphs to overcome the limitations that previously introduced models faced in capturing all the combinatorial details of the simple gene assembly process. We investigate a number of combinatorial properties of these graphs, including a necessary property in terms of forbidden induced subgraphs. We also introduce DOI graph-based rewriting rules that capture all the operations of the simple gene assembly model and prove that they are equivalent to the string-based formalization of the model. Reaction systems (RS) is another nature-inspired modeling framework that is studied in this thesis. Reaction systems’ rationale is based upon two main regulation mechanisms, facilitation and inhibition, which control the interactions between biochemical reactions. Reaction systems is a complementary modeling framework to traditional quantitative frameworks, focusing on explicit cause-effect relationships between reactions. The explicit formulation of facilitation and inhibition mechanisms behind reactions, as well as the focus on interactions between reactions (rather than dynamics of concentrations) makes their applicability potentially wide and useful beyond biological case studies. In this thesis, we construct a reaction system model corresponding to the heat shock response mechanism based on a novel concept of dominance graph that captures the competition on resources in the ODE model. We also introduce for RS various concepts inspired by biology, e.g., mass conservation, steady state, periodicity, etc., to do model checking of the reaction systems based models. We prove that the complexity of the decision problems related to these properties varies from P to NP- and coNP-complete to PSPACE-complete. We further focus on the mass conservation relation in an RS and introduce the conservation dependency graph to capture the relation between the species and also propose an algorithm to list the conserved sets of a given reaction system.

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.

A speculative systems model of the dynamic interaction among students, faculty and administration in the community college, with particular reference to intrinsic motivation and the teacher-administrator interface

The challenge the community college faces in helping meet the needs of the living open system of society is examined in this study. It is postulated that internalization student outcomes are required by society to reduce entropy and remain self-renewing. Such behavior is characterized as having an intrinsically motivated energy source and displays the seeking and conquering of challenge, the development of reflective knowledge and skill, full use of all capabilities, internal control, growth orientation, high self-esteem, relativistic thinking and competence. The development of a conceptual systems model that suggests how transactions among students, faculty and administration might occur to best meet the needs of internalization outcomes in students, and intrinsic motivation in faculty is a major purpose of this study. It is a speculative model that is based on a synthesis of a wide variety of variables. Empirical evidence, theoretical considerations, and speculative ideas are gathered together from researchers and theoretici.ans who are working on separate answers to questions of intrinsic motivation, internal control and environments that encourage their development. The model considers the effect administrators·have on faculty anq the corresponding effect faculty may have on students. The major concentration is on the administrator--teacher interface.For administrators the model may serve as a guide in planning effective transactions, and establishing system goals. The teacher is offered a means to coordinate actions toward a specific overall objective, and the administrator, teacher and researcher are invited to use the model to experiment, innovate, verify the assumptions on which the model is based, and raise additional hypotheses. Goals and history of the community colleges in Ontario are examined against current problems, previous progress and open system thinking. The nature of the person as a five part system is explored with emphasis on intrinsic motivation. The nature, operation, conceptualization, and value of this internal energy source is reviewed in detail. The current state of society, education and management theory are considered and the value of intrinsically motivating teaching tasks together with "system four" leadership style are featured. Evidence is reviewed that suggests intrinsically motivated faculty are needed, and "system four" leadership style is the kind of interaction-influence system needed to nurture intrinsic motivation in faculty.