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.

Smooth height/age curves from stem analysis with linear programming

[Abstract]

Automaattisen pakkauskoneen käyttövarmuuden varmentaminen

Työn tavoitteena oli selvittää ja varmistaa uuden pakkauskoneen riittävä käyttövarmuus. Käyttövarmuuden selvittämistä varten tutustuttiin käyttövarmuuden käsitteisiin jatunnuslukuihin, sekä selvitettiin kunnossapidon merkitystä käyttövarmuuteen. Pakkauskoneen käyttövarmuutta analysoitiin vikapuumallin avulla. Analysointia varten laadittu vikapuumalli koostuu 391 perustapahtumasta ja yhteensä 629 tapahtumasta. Käyttövarmuusanalyysi suoritettiin kvalitatiivisesti ja kvantitatiivisesti. Analysointi painottuu kuitenkin kvantitatiiviseen simulointiin. Käyttövarmuusanalysoinnin apuna käytettiin simulointiohjelmaa. Käyttövarmuusvaatimukseksi asetettiin 99 % käytettävyys vuoden käyttöjakson aikana. Vikapuuanalyysin tuloksena saatiin arvio pakkauskoneen kokonaiskäytettävyydestä. Kokonaiskäytettävyydeksi muodostui 96,44 %, joka ei täytä käyttövarmuusvaatimusta. Yksittäisistä komponenttityypeistä epäluotettavimpia olivat liimalaitteiston ja paineilmajärjestelmän komponentit. Analysointityökalun avulla voitiin osoittaa käyttövarmuutta parantavien osatekijöiden vaikutukset saatuun kokonaiskäytettävyyteen. Käyttövarmuuteen voitiin vaikuttaa kunnossapidon avulla, lyhentämällä korjausaikaa ja varmentamalla komponentteja. Esitettyjen keinojen avulla käytettävyyttä on mahdollista nostaa n. 2,18 prosenttiyksikköä. Toimenpidesuositukset esitettiin saatujen tulosten ja työssä havainnoitujen asioiden perusteella. Käytettävyyden parantamiseksi ja varmistamiseksi suositetaan oikeanlaisia kunnossapitotoimenpiteitä, tehokkaan vikadiagnostiikan rakentamista sekä antureiden varmentamista. Käyttökunnonvalvonta suositetaan suoritettavaksi määräaikaistarkastuksina. Käyttökuntoa on aloitettava seuraamaan pidemmällä aikavälillä tapahtuvina häiriöraportointeina. Lisäksi tulevaisuudessa on vaadittava käyttövarmuustakuut toimittajilta laitehankintojen yhteydessä.

Muon detector link system test set-up

CERNin tutkimuskeskuksen rakenteilla olevan hadronikiihdyttimen eräs tarkoitus on todistaa Higgsin bosonin olemassaolo. Higgsin bosonin löytyminen yhtenäistäisi nykyisen hiukkasfysiikan teorian ja antaisi selityksen sille kuinka hiukkaset saavat massansa. Kiihdyttimen CMS koeasema on tarkoitettu erityisesti myonien ilmaisuun. Tämä työ liittyy CMS koeaseman RPC-ilmaisintyypin linkkijärjestelmään, jonka tarkoituksena on käsitellä ilmaisimelta tulevia myonien aiheuttamia signaaleja ja lähettää tiedot tärkeäksi katsotuista törmäystapahtumista tallennettavaksi analysointia varten. Työssä on toteutettu linkkijärjestelmän ohjaus- ja linkkikorteille testiympäristö, jolla voidaan todeta järjestelmän eri osien keskinäinen yhteensopivuus ja toimivuus. Työn alkuosassa esitellään ilmaisimen linkkijärjestelmän eri osat ja niiden merkitykset. Työn loppuosassa käydään läpi eri testimenetelmiä ja analysoidaan niiden antamia tuloksia.

Ohjelmistokomponenttien käyttö .NET-sovelluskehityksen nopeuttajana

Diplomityön tavoitteena oli tutkia, miten uusi arkkitehtuurialusta soveltuu erään teolli-suusyrityksen tietojärjestelmien kehittämiseen ja sovellusten toteuttamiseen. Työssä keskeisin käsite oli ohjelmistoarkkitehtuuri ja siihen liittyvät suunnittelumallit sekä komponentit, jotka hyvin suunniteltuina toimivat perustana nopeammalle sovelluskehi-tykselle. Tutkimusmetodina käytettiin konstruktiivista (suunnittelutieteellistä) tutkimusmetodia. Sen vahvat ominaisuudet tukevat tutkimusaiheen innovatiivisuutta sekä soveltavan tie-teen käyttöä uuden tiedon tuottamiseksi. Heikkoutena voinee pitää tulosten analysoinnin vaikeutta, sillä evaluointi tapahtuu käytännöstä saatujen kokemusten perusteella. Työn tuloksena saatiin lisätietämystä komponenttiensuunnitteluun ja toteutukseen liit-tyvissä kysymyksissä. Lisäksi sovelluspalvelimelle luotiin joukko komponentteja, joita tullaan käyttämään jatkossa tietokantasovelluksissa: uusien komponenttien suunnittelua jatketaan ja järjestelmien suunnittelua muutetaan oliopohjaiseksi.

Vaihto-omaisuuden merkitysja hallinta tukkukaupassa

Tutkielman päätavoitteena on tutkia vaihto-omaisuuden merkitystä ja hallintaa tukkukaupassa. Tutkielman alatavoitteena on selvittää ostotoiminnan arvostusta yrityksessä sekä myynti- ja ostotoimintojen yhteistyötä. Yrityksen toiminnanohjausjärjestelmien hyödyntäminen vaihto-omaisuuden hallinnassa ja tiedon välittäjänä on toinen tutkielman alatavoitteista. Tutkielmassa haetaan myös vastauksia myynnin ostotoiminnoille esittämään kysymykseen: miksi yrityksessä ei voida pitää reilusti tavaraa varastossa. Tutkimus on tyypiltään kvalitatiivinen ja metodologialtaan tapaustutkimus. Tutkimusmenettelynä on käytetty teoriaa, havainnointia sekä case-yrityksen ja case-tuotesarjan tutkimusta. Tutkimuksen tulosten mukaan ostotoimintojen asema tukkukaupassa on saanut suuremman merkityksen kiristyvän kilpailun vuoksi. Kilpailutilanteessa yritykset pyrkivät tehokkaaseen kustannuksien ja käyttöpääoman hallintaan ja sitä kautta parantamaan tulostaan. Vaihto-omaisuuden hallinnassa tämä tarkoittaa tehokkaasti ostettuja ja hinnaltaan kilpailukykyisiä tuotteita ja varastointikulujen minimoimista. Lisäksi myynti- ja ostotoimintojen yhteistyön kehittäminen on ensiarvoisen tärkeää.

Python as a programming language for the introductory programming courses

Tämä kandidaatintyö tutkii tietotekniikan perusopetuksessa keskeisen aiheen,ohjelmoinnin, alkeisopetusta ja siihen liittyviä ongelmia. Työssä perehdytään ohjelmoinnin perusopetusmenetelmiin ja opetuksen lähestymistapoihin, sekä ratkaisuihin, joilla opetusta voidaan tehostaa. Näitä ratkaisuja työssä ovat mm. ohjelmointikielen valinta, käytettävän kehitysympäristön löytäminen sekä kurssia tukevien opetusapuvälineiden etsiminen. Lisäksi kurssin läpivientiin liittyvien toimintojen, kuten harjoitusten ja mahdollisten viikkotehtävien valinta kuuluu osaksitätä työtä. Työ itsessään lähestyy aihetta tutkimalla Pythonin soveltuvuutta ohjelmoinnin alkeisopetukseen mm. vertailemalla sitä muihin olemassa oleviin yleisiin opetuskieliin, kuten C, C++ tai Java. Se tarkastelee kielen hyviä ja huonoja puolia, sekä tutkii, voidaanko Pythonia hyödyntää luontevasti pääasiallisena opetuskielenä. Lisäksi työ perehtyy siihen, mitä kaikkea kurssilla tulisi opettaa, sekä siihen, kuinka kurssin läpivienti olisi tehokkainta toteuttaa ja minkälaiset tekniset puitteet kurssin toteuttamista varten olisi järkevää valita.

In Search of Corporate Renewal: How to Benefit from Corporate Venturing?

Despite the rapid change in today's business environment there are relatively few studies about corporate renewal. This study aims for its part at filling that research gap by studying the concepts of strategy, corporate renewal, innovation and corporate venturing. Its purpose is to enhance our understanding of how established companies operating in dynamic and global environment can benefit from their corporate venturing activities. The theoretical part approaches the research problem in corporate and venture levels. Firstly, it focuses on mapping the determinants of strategy and suggests using industry, location, resources, knowledge, structure and culture, market, technology and business model to assess the environment and using these determinants to optimize speed and magnitude of change.Secondly, it concludes that the choice of innovation strategy is dependent on the type and dimensions of innovation and suggests assessing market, technology, business model as well as novelty and complexity related to each of them for choosing an optimal context for developing innovations further. Thirdly, it directsattention on processes through which corporate renewal takes place. On corporate level these processes are identified as strategy formulation, strategy formation and strategy implementation. On the venture level the renewal processes are identified as learning, leveraging and nesting. The theoretical contribution of this study, the framework of strategic corporate venturing, joins corporate and venture level management issues together and concludes that strategy processes and linking processes are the mechanism through which continuous corporate renewaltakes place. The framework of strategic corporate venturing proposed by this study is a new way to illustrate the role of corporate venturing as a purposefullybuilt, different view of a company's business environment. The empirical part extended the framework by enhancing our understanding of the link between corporate renewal and corporate venturing in its real life environment in three Finnish companies: Metso, Nokia and TeliaSonera. Characterizing companies' environmentwith the determinants of strategy identified in this study provided a structured way to analyze their competitive position and renewal challenges that they arefacing. More importantly the case studies confirmed that a link between corporate renewal and corporate venturing exists and found out that the link is not as straight forward as indicated by the theory. Furthermore, the case studies enhanced the framework by indicating a sequence according to which the processes work. Firstly, the induced strategy processes strategy formulation and strategy implementation set the scene for corporate venturing context and management processes and leave strategy formation for the venture. Only after that can strategies formed by ventures come back to the corporate level - and if found viable in the corporate level be formalized through formulation and implementation. With the help of the framework of strategic corporate venturing the link between corporaterenewal and corporate venturing can be found and managed. The suggested response to the continuous need for change is continuous renewal i.e. institutionalizing corporate renewal in the strategy processes of the company. As far as benefiting from venturing is concerned the answer lies in deliberately managing venturing in a context different to the mainstream businesses and establishing efficientlinking processes to exploit the renewal potential of individual ventures.

Level Set Methods in Image Processing

This thesis gives an overview of the use of the level set methods in the field of image science. The similar fast marching method is discussed for comparison, also the narrow band and the particle level set methods are introduced. The level set method is a numerical scheme for representing, deforming and recovering structures in an arbitrary dimensions. It approximates and tracks the moving interfaces, dynamic curves and surfaces. The level set method does not define how and why some boundary is advancing the way it is but simply represents and tracks the boundary. The principal idea of the level set method is to represent the N dimensional boundary in the N+l dimensions. This gives the generality to represent even the complex boundaries. The level set methods can be powerful tools to represent dynamic boundaries, but they can require lot of computing power. Specially the basic level set method have considerable computational burden. This burden can be alleviated with more sophisticated versions of the level set algorithm like the narrow band level set method or with the programmable hardware implementation. Also the parallel approach can be used in suitable applications. It is concluded that these methods can be used in a quite broad range of image applications, like computer vision and graphics, scientific visualization and also to solve problems in computational physics. Level set methods and methods derived and inspired by it will be in the front line of image processing also in the future.

Ohutlevyn taivuttaminen pienerätuotannossa

Tutkimuksessa on selvitetty ohutlevyn taivuttamismenetelmien tärkeimmät kustannustekijät ja menetelmien taloudelliset käyttöalueet. Vertailtavina menetelminä on käsinsärmäys, robotisoitu särmäys, taivutusautomaatti ja taivutuskone. Tulosta on sovellettu Hackman Metos Oy:n keittiölaitteiden tuotantoon. Tutkimusmenetelminä oli haastattelututkimus, kirjallisuustutkimus, työntutkimustulosten käyttö, ryhmäteknologian soveltaminen ja kokeellinen tutkimus. Särmäysrobotin tärkein kustannustekijä on ohjelmointiaika, mikä vaikuttaa ratkaisevasti sen soveltuvuuteen pienerätuotantoon. Nykyisten särmäyssolujen taloudellinen käyttöalue on tuhansien kappaleiden vuosivolyymi satojen kappaleiden eräkoolla. taivutusautomaatin ohjelmointi- ja asetusajat ovat erittäin lyhyet ja sen tärkein kustannustekijä on käyttöaste. Mikäli käyttöaste on korkea, taivutusautomaatti on kannattava pienerätuotannossa pienille vuosivolyymeille. Taivutusautomaatin käyttöönotossa tuotteiden suunnittelu on tärkeä tekijä, sillä särmättäväksi suunnitellut osat eivät välttämättä sovellu taivutusautomaatilla taivutettavaksi. Taivutuskoneen investointikustannus on alhaisempi kuin särmäyspuristimen, mutta sillä on paljon tuotteen valmistettavuuden liittyviä rajoituksia. Taivutuskone on kannattava investointi, mikäli tuotannossa on paljon levyjä, joiden taivutukset ovat samaan suuntaan ja ne vaativat kaksi särmääjää. Tutkimuksen perusteella Hackman Metso Oy:ssä teknis-taloudellisin taivutusmenetelmä on käsinsärmäys. Tuotannon kasvaessa taivutusautomaatti tulee olemaan särmäysrobottia edullisempi. Taivutuskoneella on niin paljon valmistettavuusrajoituksia, että se ei sovellu yrityksen tuotantoon.