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.

Study of ligand-based virtual screening tools in computer-aided drug design

Virtual screening is a central technique in drug discovery today. Millions of molecules can be tested in silico with the aim to only select the most promising and test them experimentally. The topic of this thesis is ligand-based virtual screening tools which take existing active molecules as starting point for finding new drug candidates. One goal of this thesis was to build a model that gives the probability that two molecules are biologically similar as function of one or more chemical similarity scores. Another important goal was to evaluate how well different ligand-based virtual screening tools are able to distinguish active molecules from inactives. One more criterion set for the virtual screening tools was their applicability in scaffold-hopping, i.e. finding new active chemotypes. In the first part of the work, a link was defined between the abstract chemical similarity score given by a screening tool and the probability that the two molecules are biologically similar. These results help to decide objectively which virtual screening hits to test experimentally. The work also resulted in a new type of data fusion method when using two or more tools. In the second part, five ligand-based virtual screening tools were evaluated and their performance was found to be generally poor. Three reasons for this were proposed: false negatives in the benchmark sets, active molecules that do not share the binding mode, and activity cliffs. In the third part of the study, a novel visualization and quantification method is presented for evaluation of the scaffold-hopping ability of virtual screening tools.

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

Abstract

Using tools to help cost estimating and pricing: examination of costing model's and cost breakdown's workability and their capability to cooperative work

Tämä diplomityö käsittelee työkaluja, jotka on suunniteltu kustannusten ennakointiin ja hinnan asetantaan. Aluksi on käyty läpi perinteisen ja toimintoperusteisen kustannuslaskennan perusteita. Näiden menetelmien välisiä eroja on tarkasteltu ja toimintoperusteisen kustannuslaskennan paremmin sopivuus nykypäivän yrityksille on perusteltu. Toisena käsitellään hinnoittelu. Hinnan merkitys, hinnoittelumenetelmät ja päätös lopullisesta hinnasta on käyty läpi. Hinnoittelun jälkeen esitellään kustannusjärjestelmät ja kustannusten arviointi. Nämä asiat todistavat, että tarkat kustannusarviot ovat elintärkeitä yritykselle. Tuotteen kustannusarviointi, hinnan asetanta ja tarjoaminen ovat erittäin merkityksellisiä asioita ottaen huomioon koko projektin elinkaaren ja tulevat tuotot. Nykyään on yleistä käyttää työkaluja kustannusarvioinnissa ja joskus myös hinnoittelussa. Työkalujen luotettavuus on tiedettävä, ennenkuin työkalut otetaan käyttöön. Myös työkalujen käyttäjät täytyy perehdyttää hyvin. Muuten yritys todennäköisesti kohtaa odottamattomia ja epämiellyttäviä yllätyksiä.

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.

Johdon laskentajärjestelmän suunnittelu ja toimintoperusteisen laskennan käyttöönotto tietojärjestelmähankkeen yhteydessä

Tutkimus on tehty keskisuomalaiselle pk-yritykselle vuosien 2003-2005 aikana. Tutkimusjaksolla kohdeyrityksessä on toteutettu lukuisia mittavia muutoksia ja merkittävä investointiohjelma. Tutkimuksen kannalta oleellisin muutos on ollut yrityksen tietojärjestelmien kokonaisvaltainen uudistaminen. Vanha tuotannonohjausjärjestelmä on korvattu uudella toiminnanohjausjärjestelmällä ja myös taloudenohjausjärjestelmät on uudistettu. Tutkimuksen tavoitteena on ollut laatia kokonaisvaltainen suunnitelma johdon laskentajärjestelmien kehittämiseksi ja selvittää erityisesti toimintolaskentajärjestelmän sekä suorituskyvyn mittaus- ja analysointijärjestelmän implementoinnin edellytyksiä tutkimuksen kohdeyrityksessä ja laatia konkreettinen esitys järjestelmien rakentamiseksi. Johdon laskentajärjestelmän kokonaissuunnitelmassa tarkoituksena on laatia laskentajärjestelmän loogisten elementtien kuvauksen lisäksi esitys tarvittavista sovelluksista sekä tutkia sovellusten välisiä fyysisiä rajapintoja ja suunnitella järjestelmäintegraatio siten, että johdon laskentajärjestelmän koko naissuunnitelma on mahdollista taloudellisesti toteuttaa. Tutkimuksen tavoitteena on lisäksi ollut selvittääyrityksen toimintojen kustannukset ja tuoteryhmien kannattavuudet sekä rakentaasuorituskyvyn mittaus- ja analysointijärjestelmä SAKE prosessi-malliinperustuen. Lisäksi tutkimuksen puitteissa on rakennettu erilaisia liiketoimintaa tukevia raportteja erilaisilla kehitysvälineillä. Tutkimukselle asetetut sisällölliset tavoitteet saavutettiin pääpiirteissään. Jatkuvatoimisten ja integroitujen toimintolaskentajärjestelmän sekä suorituskyvyn mittaus- ja analysointijärjestelmän rakentaminen osoittautui tutkimuksen aikana haastavaksi, joskaan ei mahdottomaksi tehtäväksi. Järjestelmien rakennustyö jatkuu tutkimuksessa esitettyihin ajatuksiin perustuen yhteistyössä ohjelmistotoimittajan kanssa edelleen ja järjestelmät valmistunevat vuosien 2005-2006 aikana.

Development of Paperboard Forming Tools with a Focus on Intelligent Manufacturing

Tämä diplomityö käsittelee kartonginmuovaukseen käytettävien puristintyökalujen kehittämistä. Työntavoitteina oli kehittää työkalutekniikan suunnittelua ja valmistusta edullisemmaksi, nopeammaksi ja työkaluja toiminnoiltaan tehokkaammiksi. Työn tuli sisältää myös ohjeet työkalujen suunnittelemiseksi ja valmistamiseksi jatkoa ajatellen. Työn aikana selvitettiin mahdollisia työkalurakennevaihtoehtoja, valmistusmateriaaleja sekä niiden käsittelymenetelmiä ja lastuamista sekä sen tarjoamia mahdollisuuksia valmistusmenetelmänä. Työkalupari suunniteltiin modulaariseksi siten, että uusia työkaluja varten vain osa komponenteista täytyy valmistaa uudelleen, samalla työkalun osien lukumäärää pienennettiin merkittävästi. Valmistusmateriaaliksi valittiin hyvin lastuttava työkaluteräs ja sen koneistaminen tapahtui vaakakaraisessa koneistuskeskuksessa. Työn loppuvaiheessa työkalukokonaisuudelle tehtiin kustannuslaskelma jaoteltuna eri työvaiheille sekä komponenteittain. Työkalu asennettiin puristimeen ja sille suoritettiin käyttötestaus. Työn aikana karttuneen kokemuksen sekä koekäytön perusteella tehtiin jatkokehitysehdotuksia.

Artificially Intelligent and Adaptive Methods for Prediction and Analysis of Superheater Fireside Corrosion in Fluidized Bed Boilers

Superheater corrosion causes vast annual losses for the power companies. With a reliable corrosion prediction method, the plants can be designed accordingly, and knowledge of fuel selection and determination of process conditions may be utilized to minimize superheater corrosion. Growing interest to use recycled fuels creates additional demands for the prediction of corrosion potential. Models depending on corrosion theories will fail, if relations between the inputs and the output are poorly known. A prediction model based on fuzzy logic and an artificial neural network is able to improve its performance as the amount of data increases. The corrosion rate of a superheater material can most reliably be detected with a test done in a test combustor or in a commercial boiler. The steel samples can be located in a special, temperature-controlled probe, and exposed to the corrosive environment for a desired time. These tests give information about the average corrosion potential in that environment. Samples may also be cut from superheaters during shutdowns. The analysis ofsamples taken from probes or superheaters after exposure to corrosive environment is a demanding task: if the corrosive contaminants can be reliably analyzed, the corrosion chemistry can be determined, and an estimate of the material lifetime can be given. In cases where the reason for corrosion is not clear, the determination of the corrosion chemistry and the lifetime estimation is more demanding. In order to provide a laboratory tool for the analysis and prediction, a newapproach was chosen. During this study, the following tools were generated: · Amodel for the prediction of superheater fireside corrosion, based on fuzzy logic and an artificial neural network, build upon a corrosion database developed offuel and bed material analyses, and measured corrosion data. The developed model predicts superheater corrosion with high accuracy at the early stages of a project. · An adaptive corrosion analysis tool based on image analysis, constructedas an expert system. This system utilizes implementation of user-defined algorithms, which allows the development of an artificially intelligent system for thetask. According to the results of the analyses, several new rules were developed for the determination of the degree and type of corrosion. By combining these two tools, a user-friendly expert system for the prediction and analyses of superheater fireside corrosion was developed. This tool may also be used for the minimization of corrosion risks by the design of fluidized bed boilers.

Coping with Technology: A Study on Economic Methodology and Strategic Management of Technology

There is a broad consensus among economists that technologicalchange has been a major contributor to the productivity growth and, hence, to the growth of the material welfare in western industrialized countries at least over the last century. Paradoxically, this issue has not been the focal point of theoretical economics. At the same time, we have witnessed the rise of the importance of technological issues at the strategic management level of business firms. Interestingly, the research has not accurately responded to this challenge either. The tension between the overwhelming empirical evidence of the importance of technology and its relative omission in the research offers a challenging target for a methodological endeavor. This study deals with the question of how different theories cope with technology and explain technological change. The focusis at the firm level and the analysis concentrates on metatheoretical issues, except for the last two chapters, which examine the problems of strategic management of technology. Here the aim is to build a new evolutionary-based theoreticalframework to analyze innovation processes at the firm level. The study consistsof ten chapters. Chapter 1 poses the research problem and contrasts the two basic approaches, neoclassical and evolutionary, to be analyzed. Chapter 2 introduces the methodological framework which is based on the methodology of isolation. Methodological and ontoogical commitments of the rival approaches are revealed and basic questions concerning their ways of theorizing are elaborated. Chapters 3-6 deal with the so-called substantive isolative criteria. The aim is to examine how different approaches cope with such critical issues as inherent uncertainty and complexity of innovative activities (cognitive isolations, chapter 3), theboundedness of rationality of innovating agents (behavioral isolations, chapter4), the multidimensional nature of technology (chapter 5), and governance costsrelated to technology (chapter 6). Chapters 7 and 8 put all these things together and look at the explanatory structures used by the neoclassical and evolutionary approaches in the light of substantive isolations. The last two cpahters of the study utilize the methodological framework and tools to appraise different economics-based candidates in the context of strategic management of technology. The aim is to analyze how different approaches answer the fundamental question: How can firms gain competitive advantages through innovations and how can the rents appropriated from successful innovations be sustained? The last chapter introduces a new evolutionary-based technology management framework. Also the largely omitted issues of entrepreneurship are examined.

Oston ja ostovaraston raportoinnin ja mittariston kehittäminen toiminnanohjausjärjestelmän pohjalta

Työn tavoitteena oli kehittää Stora Enson Varkauden tehtaiden oston ja osto-varastojen raportointia ja toiminnan mittaamista toiminnanohjausjärjestelmän käyttöönottoprojektin yhteydessä. Työssä selvitettiin suorituskykymittareiden merkitystä yrityksen toiminnalle ja mittareista muodostettavalta mittaus-järjestelmältä vaadittavia ominaisuuksia. Lisäksi kartoitettiin materiaali-toimintojen yhteyttä koko yrityksen toimintaan. Työ painottuu SAP R/3:n materiaalihallinnon raporttien kartoittamiseen. Lisäksi työssä käsitellään Varenso Oy:n johtamisjärjestelmästä, Latukoneesta, saatavia mittareita. Mittariston kehittämisprosessi sisälsi käytössä olevien mittareiden arvioinnin, uusien mittareiden kartoittamisen sekä mittareiden karsinnan ja valinnan. Valituille mittareille luotiin raportointipohjat, joiden avulla niitä jatkossa seurataan. SAP R/3:n materiaalihallinnon raportointimahdollisuudet ovat laajat, mutta ne eivät kuitenkaan vielä kata kaikkia oston ja ostovarastojen raportointitarpeita. Mittaamisen ja raportoinnin kehittäminen edelleen vaatii SAP R/3:n raportointiominaisuuksien laajempaa käyttöönottoa tai muiden työkalujen hyödyntämistä raportoinnin tukena.

Työn tietotukijärjestelmän kehitys hienopaperikoneelle

Tämän projektin tarkoituksena oli kehittää paperinvalmistuslinjan multimediapohjaista tietotukijärjestelmää. Kirjallisuusosassa on todettu, että nykyisessä työympäristössä tarvitaan entistä enemmän tietotaitoa työkyvyn ylläpitämiseksi. Työntekijöiden osaaminen on avainasemassa kilpailukyvyn säilyttämisessä. Esille nousee myös suurten ikäluokkien eläköityminen ja osaavan työvoiman riittäminen. Näistä syistä erilaiset koulutukset ovat tällä hetkellä erityisen tärkeitä. Verkko-opetusvälineet ovat taloudellisesti kannattavia erityisesti suurille kohderyhmille ja sopivat hyvin paperiteollisuuden käyttöön. Parhaimmillaan ne ovat myös hyvin tehokkaita opetusvälineitä. Kokeellisessa osan alussa nähtiin tärkeäksi järjestelmän käytettävyyden ja kiinnostavuuden parantaminen ja siksi siihen päätettiin tehdä kokonaan uusi käyttöliittymä ja selkeämpi rakenne. Järjestelmän sisältö rakennettiin uudelleen hyväksikäyttäen vanhaa materiaalia soveltuvin osin. Järjestelmään laadittiin perussisältösivujen lisäksi useita johdantoja, joista saa nopeasti käsityksen tietystä prosessin osasta. Järjestelmään lisättiin myös useita multimediaelementtejä, kuten uusia kuvia, animaatioita ja videoita. Järjestelmään lisättiin myös hakutoiminto, sanasto ja käyttöohje. Näillä uudistuksilla pyrittiin parantamaan järjestelmän käytettävyyttä erityisesti prosessityöntekijöiden perehdytyksen ja työnopastuksen apuvälineenä.

Development of e-Service tools for customer services and processes, Case: KONE Oyj Finland

Tutkimuksen tavoitteena oli selvittää miten kehittää yrityksen nykyistä e-palvelujärjestelmää, Internet -teknologiaan perustuvaa sähköisiä kommunikaatio- ja tiedonjakojärjestelmää, yrityksen business-to-business asiakkuuksien johtamisessa. Tavoitteena oli myös luoda ehdotukset uusista e-palvelusopimusmalleista. Tutkimuksen teoriaosuudessa pyrittiin kehittämään aikaisempiin tutkimuksiin, tietokirjallisuuteen ja asiantuntijoihin perustuva viitekehysmalli. Empiirisessä osassa tutkimuksen tavoitteisiin pyrittiin haastattelemalla yrityksen asiakkaita ja henkilöstöä, sekä tarkastelemalla asiakaskontaktien nykyistä tilaa ja kehittymistä. Näiden tietojen perusteella selvitettiin e-palvelun käyttäjien tarpeita, profiilia ja valmiuksia palvelun käyttöön sekä palvelun nykyistä houkuttelevuutta. Tutkimuksen teoriaosan lähdeaineistona käytettiin kirjallisuutta, artikkeleita ja tilastoja asiakashallinnasta sekä e-palveluiden, erityisesti Internet ja verkkopalveluiden markkinoinnista, nykytilasta sekä palveluiden kehittämisestä. Lisäksi tutkittiin kirjallisuutta arvoverkostoanalyysistä, asiakkaan arvosta, informaatioteknologiasta, palvelun laadusta ja asiakastyytyväisyydestä. Tutkimuksen empiirinen osa perustuu yrityksen henkilöstöltä sekä asiakkailta haastatteluissa kerättyihin tietoihin, yrityksen ennalta keräämiin materiaaleihin sekä Taloustutkimuksen keräämiin tietoihin. Tutkimuksessa käytettiin case -menetelmää, joka oli yhdistelmä sekä kvalitatiivista että kvantitatiivista tutkimusta. Casen tarkoituksena oli testata mallin paikkansapitävyyttä ja käyttökelpoisuutta, sekä selvittää onko olemassa vielä muita tekijöitä, jotka vaikuttavat asiakkaan saamaan arvoon. Kvalitatiivinen aineisto perustuu teemahaastattelumenetelmää soveltaen haastateltuihin asiakkaisiin ja yrityksen työntekijöihin. Kvantitatiivinen tutkimus perustuu Taloustutkimuksen tutkimukseen ja yrityksen asiakaskontakteista kerättyyn tietoon. Haastatteluiden perusteella e-palvelut nähtiin hyödyllisinä ja tulevaisuudessa erittäin tärkeinä. E-palvelut nähdään yhtenä tärkeänä kanavana, perinteisten kanavien rinnalla, tehostaa business-to-business -asiakkuuksien johtamista. Tutkimuksen antamien tulosten mukaan asiakkaiden palveluun liittyvän tieto-, taito-, tarpeellisuus- ja kiinnostavuustasojen vaihtelevaisuus osoittaa selvän tarpeen eritasoisille e-palvelupaketti ratkaisuille. Tuloksista muodostettu ratkaisuehdotus käsittää neljän eri e-palvelupaketin rakentamisen asiakkaiden eri tarpeita mukaillen.