Fraktioinnin tehostaminen lajittelussa

Painelajittimet ovat yleisimpiä hiokkeen lajitteluun käytettyjä lajittimia. Painelajittimien suorituskyky on parantunut viimeisten vuosikymmenien aikana niin paljon, että pyörrepuhdistuksesta on pääosin voitu luopua osana hiokkeen lajittelua. Painelajittimen erinomaisuus perustuu siihen, että sillä voidaan erottaa massasta hyvinkin erilaisia epäpuhtauksia. Nykyään vallitsevia painelajittelun trendejä ovat sakeuden nosto, energiankulutuksen vähentäminen sekä eri fraktioiden erottumisen tehostuminen. Kaikilla pyritään vähentämään vedenkäyttöä ja parantamaan massan ominaisuuksia jatkoprosesseja silmälläpitäen. Tässä työssä tarkasteltiin painelajittimen roottorin kierrosnopeuden vaikutusta akseptimassan laatuun. Luodaan malli freeness-pudotukselle lajittimen yli. Sekä tarkastellaan myös automaatioon pohjautuvan säädön käyttöönottoa lajittimen akseptimassan freenesvaihteluiden tasaamiseksi. Toisaalta tehdään myös suppea selvitys lajittimien energiankulutuksista erilaisilla roottorin pyörimisnopeuksilla. Tuotantokäytössä oleviin lajittimiin asennettujen invertterisäätöjen ja koepisteistä saatujen tulosten avulla voidaan todeta, että laskemalla roottorin pyörimisnopeutta voidaan lajittimessa tapahtuvaa freenespudotusta kasvattaa. Samalla saavutetaan hyötyjä myös muissa massan ominaisuuksissa, kuten vetolujuudessa. Automaattisäädön käyttöönotolla saavutetaan huomattavasti pienempi hajonta akseptimassan freeneksessä. Rejektilinjan lajittimissa hajonta lähes puolittui ja päälinjan lajittimissa päästiin noin kolmanneksen parannukseen. Energian kulutuksia tutkittaessa huomataan, että roottorin kierrosnopeutta alentamalla voidaan merkittävästi vähentää lajittimien energian kulutusta. Parhaassa tapauksessa voidaan säästää neljännes lajittelun energiakustannuksissa.

E-Business Intreoperability Frameworks for SMEs

Current e-business standards have been developed and used by large organizations to reduce clerical costs in business transactions by increased automation and higher level of business-to-business integration. Small and medium enterprises (SME's), however, cannot easily adopt these standards due to the SME's lacking the technical expertise and resources for implementing them. Still, large organizations increasingly require their business partners, most of which are SME's, to be able to interoperate by their chosen e-business standards. The research question for the study was, first, which of the existing e-business technologies are most SME-adoptable, and, second, how could those e-business technologies be made easier for SME's to implement. The study was conducted as a literature study that evaluated the available e-business frameworks and SME-oriented e-business architectures based on the implementation complexity and costs incurred for the SME adopter. The study found that only few e-business solutions are SMEadoptable. The technological approaches used in the solutions need to be improved on a number of areas, the most important of which is implementation complexity. The study revealed that this also applies to the special, SME-oriented e-business architectures, which are also still too difficult for SME's to implement. Based on these findings, a high-level e-business interoperability framework concept was proposed as the basis for future research to overcome the found implementation complexities for SME's.

Hiontarobotti-solun tietojärjestelmä

Hiontarobotteja käytetään nopeuttamaan hiontaprosessia ja vähentämään henkilöiden tarvetta tehdä kuluttavaa ja raskasta työtä. Yleensä hiottavat kappaleet ovat suuria, jolloin hionta robotillakin kestää kauan. Kun hiottavat kappaleet ovat pieniä, robotti hioo kappaleen nopeasti. Tällöin tarvitaan automaattinen varastointi, jotta hiontarobotti pystyy jatkamaan nopeasti seuraavan kappaleen hiontaa. Automaattinen varastointi tarvitsee tiedonhallintajärjestelmän, jolla hallitaan varastossa olevien kappaleiden tietoja. Hiottava kappale täytyy esimerkiksi pystyä tunnistamaan ennen hionnan aloittamista. Yhtenä tunnistusmenetelmänä voidaan käyttää radiotaajuudella toimivia RFID-tunnisteita. Kun kappale tunnistetaan ennen hiontaa niin voidaan varmistua, että robotti suorittaa oikean hiontaohjelman kappaleelle. Diplomityö liittyy Master Automation Groupin ensimmäiseen automaattista varastoa hyödyntävään FlexMill™-hiontarobotti-soluun. Työssä on suunniteltu ja toteutettu tietokanta ja siihen liittyvä tietojärjestelmä. Kehitettävä ohjelma toimii solun toiminnasta vastaavan soluohjaimen tiedonhallintaosana. Ohjelma hyödyntää RFID-laitteita kappaleiden tunnistuksessa.

Operatiivisen toiminnan liikevaihdon seurantajärjestelmä

Tämä työ tehdään Steveco Oy:lle sataman operatiivisen toiminnan aiheuttamien kulujen ja tuottojen seurantaan. Työssä käsitellään automaattisen liikevaihdon laskennan ongelmia ja ratkaisuja. Työssä sivutaan myös työajanseurannan sosiaalisia vaikutuksia työntekijöihin, sekä esitetään keinoja ongelmatilanteiden välttämiseksi. Työn tuottavuuden mittaamiseksi on kehitetty matemaattisia malleja, joita voidaan soveltaa organisaatiossa työtehojen mittaamiseksi. Työssä esitellään näitä malleja sekä pohditaan niiden soveltamista. Työssä esitetään malli automaattiseen liikevaihdon ja kulujen laskentaan sekä siihen liittyviä teknisiä ratkaisuja. Työn lopussa todetaan että automaattinen liikevaihdon ja kulujen seurantajärjestelmä on mahdollista rakentaa ja tuloksessa päästään hyvin tarkkaan arvioon lopullisesta liikevaihdosta. Arvion tarkkuus riippuu operatiivisten järjestelmien käyttötavoista sekä työnohjauksen menettelytavoista.

Osaamisen hallinta suurissa muutosprojekteissa

Ydinvoimatoiminta on muuta teollisuustoimintaa huomattavasti säädellympi alue, missä organisaatioiden riittävä osaaminen on ydinturvallisuuden kannalta tärkeää. Tästä syystä osaamisen riittävyyden takaamiseksi panostetaan tinkimättömästi. Etenkin prosessi- ja turvajärjestelmiin tehtävät muutos- modernisointityöt luovat haasteita organisaatioiden nykyosaamiselle, koska muutosten hallinta edellyttää organisaatioilta jatkuvaa oppimista ja osaamisen kehittämistä. Fortum Power & Heat Oy:n omistamalla ydinvoimalaitoksella käynnistettiin vuoden 2005 alussa laaja automaatiouusintaan tähtäävä projekti. Järjestelmien kokonaistoimittajaksi oli valittu ranskalais-saksalainen Areva NP GmbH – Siemens AG – konsortio. Konsortion kokonaistoimitukseen kuuluu automaatiojärjestelmien uusimisen lisäksi myösydinvoimalaitoksen henkilöstön kouluttaminen. Loviisa ydinvoimalaitoksen käyttöluvan haltijana Fortum Power & Heat Oy on kokonaisvastuullinen ydinvoimalaitoksen toiminnasta. Täten myös henkilöstön riittävä osaaminen ja pätevyys ovat Fortumin vastuulla. Toimittajan järjestämien koulutustilaisuuksien avulla hankittu uusi osaaminen on havaittu riittämättömäksi. Tämän on koettu johtuvan osittain teoriaan painottuvasta koulutusmateriaalista ja myös siitä, että käytännön tarjoamiin koulutustilaisuuksiin kuten esimerkiksi osallistuminen suunnittelutyöhön ei ole hakeuduttu. Lisäksi koulutus kaipaa kokonaisuudessaan kehittämistä. Tästä johtuen ydinvoimalaitosten muutostöihin liittyvän henkilöstön osaamisen ja pätevyyden selvittämiseksi käynnistettiin tämä tutkimus. Tutkimuksessa on tunnistettu useita sellaisia kehityskohteita, joita tehostamalla on mahdollista kehittää automaatioylläpitoryhmän osaamista. Lisäksi on esitetty menettelytapoja ja käytäntöjä, joilla ylläpidon koulutusta on mahdollista tehostaa. Tutkimuksen tuotokset toimivat suuntaviivoina organisaation kehittämisen toteutukselle.

Voimalaitos- ja jätevesitutkimus

Tässä työssä tutkittiin Stora Enso Oyj:n Heinolan Flutingtehtaan voimalaitos- ja jätevesien seuranta-analyysimenetelmien kehittämistä. Käytössä olevia menetelmiä vertailtiin vaihtoehtoisiin uusiin menetelmiin, jotka perustuvat erotustekniikoihin ja automaatioon. Flutingtehtaalla nykyisin käytössä olevat analyysimenetelmät perustuvat suurelta osin standardimäärityksiin, joissa käytetään pääasiassa titrausta. Määritykset vievät paljon aikaa, koska titraukset toteutetaan manuaalisesti. Titrausten päätepisteet tulkitaan esim. indikaattorin värinmuutoksella ja saostamalla, joten määritysten tarkkuus vaihtelee. Kokeellisessa osassa Flutingtehtaan puhtaista voimalaitosvesistä yhdistetty sekoitenäyte analysoitiin kahdella ionikromatografilla, liekkiatomiabsorptiospektrometrillä ja kapillaarielektroforeesilla. Yksittäisiä näytteitä ei tutkittu. Lisäksi vesilaboratoriossa määritettävistä jätevesistä yhdistettiin sekoitenäyte, joka analysoitiin kapillaarielektroforeesilla. Samat sekoitenäytteet analysoitiin myös nykyisillä menetelmillä tehtaan vesilaboratoriossa. Tulokset osoittivat, että kokeellisessa osassa tutkitut menetelmät soveltuvat sekoitenäytteen perusteella hyvin vesilaboratoriossa käytössä oleviin kuukausianalyyseihin. Automaattisella näytteensyötöllä varustettuna kaikki kolme kokeellisessa osassa tutkittua menetelmää ovat yksikertaisia käyttää ja ne nopeuttavat analyysejä. Päivittäisiä titrausanalyysejä voidaan tehostaa ja nopeuttaa automaation avulla. Erotustekniikoilla esimerkiksi typpi voidaan määrittää kokonaistyppenä, mutta myös komponentteinaan eli ammoniakkina, nitraattina ja nitriittinä. Lisäksi samalla erotuksella voidaan määrittää useita alkali- ja maa-alkalimetalleja sekä raskas-metalleja toistomittauksilla. Menetelmän käyttöalue on laajempi erotustekniikoilla kuin perinteisillä liuoskemian mittauksilla. Erotustekniikoilla tunnistetaan helposti määritysten oikeellisuus detektointimahdollisuuksien monipuolisuuden vuoksi.

Järjestelmien siirtäminen uuteen käyttöjärjestelmäympäristöön

Käyttöjärjestelmän uuden version myötä vanhat ohjelmat eivät välttämättä toimi uudessa ympäristössä. Windows-käyttöjärjestelmässä sovellusten yhteensopivuus on aiemmin säilytetty melko hyvin. Uusimpiin Windows Vista ja Windows 7 -versioihin on tehty paljon tietoturvauudistuksia. Niistä johtuen vanhojen ohjelmien yhteensopivuutta on karsittu. Tässä työssä kuvataan automaatiojärjestelmän ohjelmakomponenttien siirtoa uuteen Windows-ympäristöön. Tavoitteena on saada tehtyä ohjeita muille automaatiojärjestelmän kehittäjille. Myös Windowsin tietoturvaominaisuuksiin tehdään katsaus, erityisesti pääsynhallintaan

Älykäs liikennetelematiikkajärjestelmä portti- ja puomiympäristön hallintaan ja automatisointiin

Tässä diplomityössä käsitellään älykkään liikennetelematiikkajärjestelmän määrittelyyn ja toteuttamiseen liittyviä haasteita. Työssä määritellyt konseptit keskittyvät logistiikkakeskuksiin ja parkkihalleihin ja niissä erityisesti puomi- ja porttiympäristöjen hallintaan ja automatisointiin. Työn tavoitteena on tukea kohdeyrityksen päätöksentekoa tuotelinjausten, järjestelemäkomponenttien sekä ohjelmistoympäristöjen valinnan osalta. Diplomityön tuloksia voidaan hyödyntää kohdeyrityksen operatiivisessa toiminnassa tehtäessä strategisia päätöksiä yrityksen tulevaisuuden tuotteiden suuntaviivoista ja teknologialinjauksista. Työ tarjoaa päätöksenteon tueksi sekä arvokasta tausta-aineistoa että suoria johtopäätöksiä ja suosituksia.

Uuden robottisolun ohjelmointitavan mahdollisuudet pienille ja keskisuurille yrityksille

Robotin ohjelmointi on aikaa vievää ja tarvitsee robotin ohjelmoinnin tuntevan operaattorin toimimaan robotin opettajana. Saadakseen robottisolun kustannustehokkaaksi operaattorilla olisi hyvä olla useampi solu hoidettavanaan samaan aikaan. Tämä ei ole suuri ongelma suurille yrityksille, joissa voi olla kymmeniä robottisoluja. Jos kyseessä on pieni tai keskisuuri yritys, automatisointi-investointi voi jäädä tekemättä ohjelmoinnin vaikeuden aiheuttaman ongelman vuoksi. Diplomityössä keskityttiin tutkimaan robotisointia pienten ja keskisuurten yritysten kannalta. Teoriaosassa on keskitytty robottisolun suunnittelun kannalta tarvittaviin perustietoihin robotin rakenteesta, ohjausjärjestelmästä, ohjelmoinnista sekä turvallisuudesta. Näiden perustietojen lisäksi on huomioitu hitsauksen automatisointia sekä taluttamalla ohjelmoitavan robottisolun tekninen konsepti. Taluttamalla ohjelmoitavan robottisolun konseptin käsittelyosassa on myös perehdytty taluttamalla ohjelmoinnin vaatimiin komponentteihin kuten voima/vääntö-anturi. Robottisolun suunnittelu on tehtävä koneasetuksen vaatimusten mukaan. Turvallisuus osiossa on käsitelty koneasetuksen vaatimuksia koneensuunnittelulle ja käytännön osassa on käsitelty Winnovan taluttamalla ohjelmoitavan robottisolun suunnittelua koneasetuksen ohjeiden mukaan. Käytännön osassa on tutkittu taluttamalla ohjelmoinnin tuomia etuja muihin ohjelmointimenetelmiin nähden sekä suoritettu investointilaskelmat taluttamalla ohjelmoitavasta ja opettamalla ohjelmoitavasta robottisolusta. Koetuloksista nähdään taluttamalla ohjelmoinnin olevan nopeampi ja yksinkertaisempi tapa ohjelmoida robottia kuin opettamalla ohjelmointi. Investointilaskelmien vertailusta nähdään taluttamalla ohjelmoinnin tulevan opettamalla ohjelmointia edullisemmaksi vaihtoehdoksi käyttökustannusten edullisuuden ansiosta.

Automaatiolaitteiden elinkaaren hallinta ydinvoimalaitoksessa

Diplomityön tavoitteena on selvittää automaatiolaitteiden elinkaaren hallintaa ottaen huomioon ydinvoimalaitoksessa toimimisen erityispiirteet. Elinkaaren hallinnan tavoitteena on laitoksen korkean turvallisuuden ja käyttökertoimen varmistaminen. Työssä käydään läpi elinkaaren vaiheita käyttäen esimerkkinä turbiinilaitoksen automaation modernisointiprojektia. Diplomityö alkaa katsauksella ydinenergia-alan viranomaisiin, säännöksiin sekä menetelmiin, joilla ydinturvallisuus varmistetaan. Työssä otetaan selvää, millaisissa tehtävissä automaatiolaitteet ja –järjestelmät ydinvoimalaitoksissa toimivat ja millä perusteilla ne kelpoistetaan käyttötarkoitukseensa. Työssä pyritään lisäksi kartoittamaan ydinvoimala-alan tarpeita erilaisilleautomaatiotekniikkaan liittyville palveluille. Esiin nousivat etenkin haasteet ohjelmistoversioiden hallinnassa.

On Doing Successful ICT Business with Russian Manufacturing Enterprises

This Master’s thesis addresses different approaches using which a foreign IT company could enter Russian manufacturing industry with its enterprise information systems and IT services. In order to define the most suitable market entry approach, several aspects related to Russian manufacturing enterprises are studied. These aspects include challenges of doing ICT business with the previously mentioned enterprises, their perception of ICT role and their ICT preferences, as well as their buying behavior related to acquisition of information systems (IS). The study results show that there are several challenges that can be faced by a foreign IT vendor when starting conducting ICT business with Russian manufacturing enterprises. The results also show that Russian manufacturing industry is still rather immature in sense of business process automation, and its IT buying behavior is rather specific and complicated. The results suggest that an efficient way to approach these enterprises is through a network of trusted partners that consists of reliable Russian IS integrators and business consultants having established connections to Russian manufacturing companies and possessing the needed competence.

Analysis of electricity distribution network operation business models and capitalization of control room functions with DMS

Electricity distribution network operation (NO) models are challenged as they are expected to continue to undergo changes during the coming decades in the fairly developed and regulated Nordic electricity market. Network asset managers are to adapt to competitive technoeconomical business models regarding the operation of increasingly intelligent distribution networks. Factors driving the changes for new business models within network operation include: increased investments in distributed automation (DA), regulative frameworks for annual profit limits and quality through outage cost, increasing end-customer demands, climatic changes and increasing use of data system tools, such as Distribution Management System (DMS). The doctoral thesis addresses the questions a) whether there exist conditions and qualifications for competitive markets within electricity distribution network operation and b) if so, identification of limitations and required business mechanisms. This doctoral thesis aims to provide an analytical business framework, primarily for electric utilities, for evaluation and development purposes of dedicated network operation models to meet future market dynamics within network operation. In the thesis, the generic build-up of a business model has been addressed through the use of the strategicbusiness hierarchy levels of mission, vision and strategy for definition of the strategic direction of the business followed by the planning, management and process execution levels of enterprisestrategy execution. Research questions within electricity distribution network operation are addressed at the specified hierarchy levels. The results of the research represent interdisciplinary findings in the areas of electrical engineering and production economics. The main scientific contributions include further development of the extended transaction cost economics (TCE) for government decisions within electricity networks and validation of the usability of the methodology for the electricity distribution industry. Moreover, DMS benefit evaluations in the thesis based on the outage cost calculations propose theoretical maximum benefits of DMS applications equalling roughly 25% of the annual outage costs and 10% of the respective operative costs in the case electric utility. Hence, the annual measurable theoretical benefits from the use of DMS applications are considerable. The theoretical results in the thesis are generally validated by surveys and questionnaires.

Modulaarinen kiinnitintekniikka alumiiniveneiden robottihitsauksessa

Tällä hetkellä hitsauksen automatisointiaste on hyvin pieni alumiinivenevalmistuksessa. Automatisointiasteen kasvattaminen on ensiarvoisen tärkeää kilpailukyvyn säilyttämiseksi, sekä edelleen nostamiseksi. Automatisointiasteen kasvattamisen esteenä ei ole teknologian puute, vaan suunnitellut tuotteet soveltuvat huonosti robotisoituun hitsaukseen. Lisäksi liitettävien osien tarkkuus on monissa tapauksissa puutteellinen, joten robottihitsaus on monessa tapauksessa mahdotonta. Robottihitsauksessa vaaditaan osien hyvää paikoittamista ja siihen tarvitaan kiinnittimiä. Kuitenkin alumiinivenevalmistuksessa valmistusmäärät ovat sen verran pieniä, että tuotekohtaisia kiinnittimiä ei kannata hankkia tai valmistaa. Siksi kiinnittimiltä vaaditaan joustavuutta ja modulaarisuutta, jotta samalla kiinnittimellä voi hitsata useita vastaavia piirteitä omaavia tuotteita. Tässä työssä tutkittiin modulaarisia kiinnittimiä, edistyneitä kiinnitinsuunnitteluprosesseja, osavalmistustarkkuuksia, tuotemoduloinnin hyödyntämistä ja alumiinin robottihitsauksen erityispiirteitä. Työssä suunniteltiin ja simuloitiin modulaarinen hitsauskiinnitin, jota käytetään tietyn alumiinivenemallin erillisenä osakokoonpanona valmistettavan jäykisterakennekonseptin hitsaamiseen. Suunnittelu ja simulointi tehtiin Delmia V5R20 -ohjelmistolla. Jäykisterakenne on modulaarinen tuoterakenne, jossa käytetään itsepaikoittavia liitoksia helpottamaan osien asettelua ja yksinkertaistamaan kiinnitintä. Kiinnitin soveltuu joustavasti erikokoisten jäykisterakenneosakokoonpanojen valmistukseen. Lisäksi suunniteltua kiinnitintä verrattiin kaupalliseen modulaariseen Demmeler -kiinnitinjärjestelmään. Jäykisterakenteen osakokoonpanon hitsaaminen robotilla lyhentää valmistusaikaa verrattuna nykytilaan, kun osat voidaan asettaa kiinnittimeen nopeasti ja luotettavasti. Samalla jäykisterakenteen tekeminen erillisenä osakokoonpanona lyhentää veneen rungon loppukokoonpanoaikaa ja mahdollistaa hitsausrobotin käytön myös veneen muiden hitsien hitsaamisessa. Modulaarisilla hitsauskiinnittimillä saavutetaan alumiiniveneiden nykyisillä valmistusmäärillä skaalaetuja, joita tuotekohtaisella kiinnittimellä ei voi saavuttaa.

On the development of object functions and restrictions for shapes made with a turret punch press

This study presents the information required to describe the machine and device resources in the turret punch press environment which are needed for the development of the analysing method for automated production. The description of product and device resources and their interconnectedness is the starting point for method comparison the development of expenses, production planning and the performance of optimisation. The manufacturing method cannot be optimized unless the variables and their interdependence are known. Sheet metal parts in particular may then become remarkably complex, and their automatic manufacture may be difficult or, with some automatic equipment, even impossible if not know manufacturing properties. This thesis consists of three main elements, which constitute the triangulation. In the first phase of triangulation, the manufacture occuring on a turret punch press is examined in order to find the factors that affect the efficiency of production. In the second phase of triangulation, the manufacturability of products on turret punch presses is examined through a set of laboratory tests. The third phase oftriangulation involves an examination of five industry parts. The main key findings of this study are: all possible efficiency in high automation level machining cannot be achieved unless the raw materials used in production and the dependencies of the machine and tools are well known. Machine-specific manufacturability factors for turret punch presses were not taken into account in the industrial case samples. On the grounds of the performed tests and industrial case samples, the designer of a sheet metal product can directly influence the machining time, material loss, energy consumption and the number of tools required on a turret punch press by making decisions in the way presented in the hypothesis of thisstudy. The sheet metal parts to be produced can be optimised to bemanufactured on a turret punch press when the material to be used and the kinds of machine and tool options available are known. This provides in-depth knowledge of the machine and tool properties machine and tool-specifically. None of the optimisation starting points described here is a separate entity; instead, they are all connected to each other.

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.