Formal Methods Forum

Spring 2001

This is a seminar on formal methods in computer science and engineering organized by the Laboratory for Theoretical Computer Science at HUT. We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science building.

For further information, please contact Ilkka Niemelä.

Program

• 26.1.2001 FT Mika Rautila (Stonesoft): Konsistenssituloksia joukko-opissa

  Tiivistelmä: Gödelin ensimmäisen epätäydellisyysteoreeman mukaan riittävän vahva efektiivinen, konsistentti teoria $T$ on epätäydellinen. Epätäydellisyys tarkoittaa, että on olemassa teorian $T$ kielen lause $\varphi$ siten, ettei se eikä sen negaatio ole johdettavissa teoriasta $T$. Zermelo-Frankel -joukko-opissa (ZFC) esimerkki tällaisesta kaavasta on kontinuumihypoteesi (CH), joka väittää, että kontinuumin mahtavuus on $\aleph_1$. 30-luvulla Gödel osoitti, käyttämällä määrittelemäänsä konstruoitavien joukkojen universumia (sisäinen malli L), että jos ZFC on konsistentti, niin myös teoria ZFC + CH on konsistentti. Tulos osoittaa, ettei kontinuumihypoteesin negaatiota voi johtaa joukko-opissa (jos joukko-opin teoria on konsistentti). Paul Cohen osoitti 60-luvulla keksimänsä pakotuskonstruktion avulla, ettei myöskään kontinuumihypoteesia voi johtaa ZFC:sta. Sisäiset mallit ja pakotusrelaatio ovat modernin joukko-opin keskeisiä työkaluja tutkittaessa joukko-opillisten väittämien keskinäisiä suhteita.

• 2.3.2001 Veera Lehtonen (Smarttrust): Vikasietoisen äänestysjärjestelmän toteutus

  Tiivistelmä: Viimeisen kahdenkymmenen vuoden aikana on kehitetty useita erilaisia menetelmiä sähköiseen äänestykseen. Diplomityössä vertaillaan seitsemää ehdotettua menetelmää ja tutkitaan niiden soveltuvuutta ympäristöön, jossa äänestäminen tapahtuu mobiililaitteella. Työssä selvitetään näiden menetelmien tietoturvaominaisuuksia, käytettävyyttä ja tehokkuutta. Mobiililaitteen käyttäjän kannalta on tärkeää, että äänestäminen ei vaadi raskaita operaatioita eikä useiden viestien lähetystä ja vastaanottamista.

  Diplomityötä varten on toteutettu Cramerin, Gennaron ja Schoenmakersin suunnittelema äänestysmenetelmä. Tämän menetelmän etuna on, että äänestäjän tarvitsee lähettää vain yksi viesti. Työssä kuvataan toteutettua järjestelmää ja arvioidaaan toteutustyötä sekä itse järjestelmää.

• 16.3.2001 Pauli Väisänen (Helsingin Yliopisto/matematiikan laitos): Peleistä logiikassa

  Tiivistelmä: Tarkoitukseni on valaista erilaisten pelien roolia mallien tutkimuksessa, erityisesti esittelemällä Helsinkiläisen logiikan tutkimusryhmän (www.math.helsinki.fi/~logic/) käyttämiä menetelmiä. Partiaali-isomorfismien ja Ehrenfeucht-Fraisse pelien avulla voidaan monien teorioiden (tai malliluokkien) malleja luokitella tai osoittaa luokittelun mahdottomuus. Käytettävissä olevan ajan puitteissa pyrin myös antamaan kytkennän tietojenkäsittelyteoriaan, lähinnä esittelemällä ns. äärellistä malliteoriaa (yhteys tietokantateoriaan ja vaativuusteoriaan). Esitiedoksi riittää peruslogiikan tuntemus.

• 4.5.2001 Louise Lorentsen (University of Aarhus): Modelling Feature Interaction Patterns in Nokia Mobile Phones using Coloured Petri Nets

  Abstract: The talk presents the ideas and first results of a project on the modelling of important patterns of feature interactions of Nokia mobile phones using Coloured Petri Nets (CP-nets or CPN). MAFIA is a joint project between Nokia Research Center and the CPN group from the University of Aarhus.

  A modern mobile phone supports many features: voice and data calls, text messaging, personal information management (phonebook and calendar), WAP browsing, games, etc. All these features are packaged into a handset with a small display and a special purpose keypad. The limited user interface and the seamless intertwining of logically separate features cause many problems in the software development of the user interface of mobile phones. In the development of the user interface software for a mobile phone, it is important to identify and clearly specify the right interactions between the separate features of the mobile phone at an early stage of the development. This helps to avoid costly delays in the integration phase of a set of independently developed features. Feature interaction means a dependency or interplay of features. The feature interactions can be conceptually simple usage dependencies or more complex combinations of independent behaviors. The types and the number of interactions a feature has with other features are direct indicators of the cost of developing the feature which is important information for the planning and management of the development effort.

  In the talk we present a categorization of feature interactions and describe our approach to modelling feature interaction patterns using Coloured Petri Nets. We will give an on-line demonstration of the CPN model created in the project with focus on the extensions made to the CPN model to enable simulations to be controlled and visualised without showing the underlying CP-Nets.

• 25.5.2001 Maarit Hietalahti: Tehokas avaimenluonti ad-hoc verkoissa

  Tiivistelmä: Ad-hoc verkko tarkoittaa tarpeen vaatiessa pystytettävää, usein tilapäistä verkkoa, jolla ei ole keskitettyjä verkkopalveluja. Verkon muodostavat liikkuvat päätelaitteet, jotka ottavat yhteyksiä toistensa kautta. Tästä seuraa se, että yhteydet ovat epävakaita ja verkon rakenne muuttuu yhtenään. Luottamuksellisuus, turvallisen kommunikaation tärkeä perusominaisuus, voidaan saavuttaa salaamalla viestit julkisella avaimella tai yhteisellä symmetrisellä avaimella. Näistä symmetrisen avaimen menetelmä on yleensä nopeampi. Ryhmälle viestijöitä on mahdollista saada yhteinen avain siten, että jokainen jäsen ottaa osaa avaimen luomiseen.

  Tämän diplomityön tarkoituksena on löytää tehokas ja turvallinen avaimenluontiprotokolla ad-hoc verkossa viestiville laitteille. Ad-hoc verkon tilapäisluonne aiheuttaa erityisvaatimuksia protokollalle, mitä ei ole aiemmin kunnolla huomioitu kirjallisuudessa. Tässä työssä esitettävä yksityiskohtainen kirjallisuustutkielma olemassaolevista protokollista pyrkii korjaamaan tämän puutteen. Siinä osoitettiin, että mikään kirjallisuuden protokolla ei sellaisenaan sovellu kaikkiin ad-hoc-verkon tilanteisiin. Siksi päätuloksena esitetään uusi avaimenluontiprotokolla, jota voi käyttää epävakaassa verkkotopologiassa. Protokollan turvallisuus ja tehokkuus on vertailukelpoinen kirjallisuuden protokollien kanssa. Se pohjautuu samoihin turvallisuusolettamuksiin kuin kirjallisuuden protokollat ja saavuttaa optimiarvon viestien määrän suhteen ja on lähes optimaalinen muiden käytettyjen mittareiden suhteen. Erityisesti tämän protokollan etuna on, että se toimii missä hyvänsä verkkotopologiassa, jossa kuhunkin osanottajaan on ainakin yksi linkki.

• 8.6.2001 Dr. Helger Lipmaa: Personal Account of Cryptography, Research and their Combination
  Obs.! The talk is held at 2 p.m. in hall T4.

  Abstract: I'll be appointed to be a professor of cryptology from this August. In this talk I will give a short overview of how did this happen. How and when did I get interested in this field, and what I've done afterwards. I will also give my personal view of why cryptology is a good area of research.

• 12.6.2001 Prof. Wolfgang Reisig (Humboldt-Universität zu Berlin, Institut für Informatik) Recent Results on Distributed Algorithms
  Obs.! The talk is held at 2 p.m. in hall T4.

  Abstract: Distributed Algorithms solve basic organizatorial problems in distributed systems. To model and to verify such algorithms, fundamentally new techniques are required. The lecture surveys recent results in this area, gained in three Ph.D. theses and a habilitation thesis at my chair.

• 15.6.2001 Prof. Patric Östergård: Ten-odd years at DSL/TCS - Did I learn anything?
  Obs.! The talk is held at 2 p.m. in hall T4.

  Abstract: I joined the laboratory in 1989 and have since then, apart from a one-year visit in Eindhoven, The Netherlands, been a member of the laboratory. In 2000 I was appointed professor in Information Theory at the Department of Electrical and Communications Engineering, where I'll move on August 1. In this farewell lecture, I'll briefly mention some things that I have learnt along the years. Hopefully, I will in this way be able to communicate some valuable ideas and thoughts to the younger people in the laboratory.