Helsingin yliopisto Tietojenkäsittelytieteen laitos
 

Tietojenkäsittelytieteen laitos

Tietoa laitoksesta:

 

581366-1 Spesifioinnin ja verifioinnin perusteet (4 op, 2 ov), Kevät 2008

Information in English at the end of this page.

Yleistä kurssista

  • Kurssin sisältö

  • Kurssin oppimistavoitteet

  • Luennot 14.1. - 22.2.2008 ke 10-12, pe 12-14, D122, ke 20.2 10-12 ei ole luentoa, korvaava luento on 11.2 14-16 salissa CK110
    luennoitsija Päivi Kuuppelomäki.

  • Luentomateriaalina käytetään Timo Karvin monistetta ps-tiedostona ja pdf-tiedostona

    Yhtä kurssille sopivaa oppikirjaa ei ole. Seuraavassa kirjallisuuslistassa on muutamia oppikirjoja ja artikkeleita, joista on hyötyä:

    1. A.W.Roscoe: The Theory and Practice of Concurrency, Prentica-Hall 1998
    2. S.Schneider: Concurrent and Real-time Systems: the CSP Approach, Wiley 1998.
    3. C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall 1985.
    4. R. Milner, Communication and Concurrency, Prentice-Hall 1989.
    5. K. Turner (Ed.), Using Formal Description Techniques, Wiley 1993.
    6. T. Bolognesi, E. Brinksma, Introduction to the ISO Spesification Language LOTOS, Computer Networks and ISDN Systems, 14, s. 25-59, 1987.
    7. M. Tienari, Johdanto tilakoneformalismin käyttöön tietoliikenneprotokollien spesifioinnissa ja analyysissä, Tietojenkäsittelytieteen laitoksen julkaisu B-1989-1.
    8. M. Tienari Lecture notes of an introductory course in formal specification of computer communication protocols University of Helsinki, Department of Computer Science, D-2003-421.
    9. J. Fernandez, An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13:219-236, 1989/90 (luku 4) pdf

  • Kurssikoe Ke 27.2 klo 16-19 A111. Tarkista aika ja paikka www-sivulta Kurssikokeet kevätlukukaudella 2008. Muutamaa päivää ennen koetta.

  • Harjoitukset 12.1.-22.2. pe 10-12 B119. Harjoitukset ovat pakollisia, ja niistä saa lisäpisteitä. Vähintään harjoituksista on tehtävä 40% ja 40% tuottaa yhden pisteen, 80% 10 pistettä.

  • Kurssiin liittyy yksi kurssikoe ja neljä erilliskoetta. Kurssikokeessa maksimipistemäärä on 50, johon lisätään harjoituspisteet. Ensimmäinen erilliskoe on kesällä, sen jälkeen kaksi syksyllä ja vielä yksi seuraavana keväänä. Erilliskokeissa ei harjoituspisteitä oteta huomioon.
  • Ajankohtaista

  • [29.2.2008] Kurssikokeen tulokset. Pyytäisin vastaamaan kurssikyselyyn ja antamaan palautetta erityisesti luennolla tehdyistä tehtävistä. Oliko niistä hyötyä ja miten niitä voisi kehittää edelleen. Muu palaute on myös tervetullutta.
  • 11.2.2008 CK110 klo 14-16 käydään läpi CADP-ohjelmistoa ja harjoitellaan sen käyttöä ja LOTOS-ohjelmointia.
  • 11.2.2007 CADP-pikaopas päivitettynnä on nyt saatavilla. CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package"):n kotisivu löytyy osoitteesta http://www.inrialpes.fr/vasy/cadp/
  • Harjoitukset

  • Harjoitus 1, 18.1.2008 pdf
  • Harjoitus 2, 25.1.2008 pdf vastauksia pdf
  • Harjoitus 3, 1.2.2008 pdf vastauksia pdf
  • Harjoitus 4, 8.2.2008 pdf vastauksia pdf
  • Harjoitus 5, 15.2.2008 pdf vastauksia pdf
  • Harjoitus 6, 22.2.2008 pdf vastauksia pdf
  • How to do in English in English

    One student has asked how to do this course in English. Please send me an email if you do not speak Finnish and want to take the course.

    You should have at least following material:

    1. T. Bolognesi, E. Brinksma, Introduction to the ISO Spesification Language LOTOS, Computer Networks and ISDN Systems, 14, s. 25-59, 1987. pdf
    2. M. Tienari Lecture notes of an introductory course in formal specification of computer communication protocols University of Helsinki, Department of Computer Science, D-2003-421. (You can buy this from yliopistopaino, Exactum, 1st floor)
    3. J. Fernandez, An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13:219-236, 1989/90 (chapter 4) pdf
    4. Timo Karvi's lecture notes in Finnish. There are examples that you can look even if you cannot Finnish.
    There is more material
    1. A.W.Roscoe: The Theory and Practice of Concurrency, Prentica-Hall 1998
    2. S.Schneider: Concurrent and Real-time Systems: the CSP Approach, Wiley 1998.
    3. C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall 1985.
    4. R. Milner, Communication and Concurrency, Prentice-Hall 1989.
    5. K. Turner (Ed.), Using Formal Description Techniques, Wiley 1993.

    Exercises

  • Exercise 1, 18.1.2008 (Only in Finnish) pdf
  • Exercise 2, 25.1.2008 pdf
  • Exercise 3, 1.2.2008 pdf
  • Exercise 4, 8.2.2008 pdf
  • Exercise 5, 15.2.2008 pdf
  • Exercise 6, 22.2.2008 pdf