581366-1 Spesifioinnin ja verifioinnin perusteet (2 ov)

Ajankohtaista

  • 8.6. pidetyn erilliskokeen tulokset

  • Kurssin tulokset

  • Monisteen sivulle 20 on tullut suurehko muutos: leveyssuuntainen saavutettavuusverkko-algoritmi on muuttanut muotoaan, korjattu versio
  • Kurssimateriaalia ja aihepiiriin liittyviä linkkejä täältä
  • spin executablet toimivat ainakin laitoksen Linuxeissa, kopioi tiedostot esim. ~/bin -hakemistoosi
  • laskarimallivastauksia

    • Opetus

  • Luennot: Matti Luukkainen 17.01.-23.02. ma ja ke 10-12 D122
  • Laskuharjoitukset: Harri Mansikka 24.01.-04.03. ryhmä 1 ti 18-20 C221, ryhmä 2 ke 12-14 DK117
  • Kurssikoe: pe 11.3. klo 14-18 A111 ja B123

    • Asema opetuksessa

  • Hajautettujen järjestelmien ja tietoliikenteen linjalla pakollinen laudatur-kurssi.
  • Sopii hyvin esim. Ohjelmistotuotannon tai Algoritmilinjan valinnaiseksi laudatur-kurssiksi

    • Yleistä

  • Yleisellä tasolla kurssilla liikutaan formaalin spesifioinnin ja verifioinnin piirissä, eli tavoitteena on määritellä yksikäsitteisesti järjestelmän toiminnan halutut piirteet ja todeta eksaktein matemaattisin menetelmin ohjelman vastaavan spesifikaatiotaan. Järjestelmän luotettavuudesta vakuuttuminen ei siis pääasiassa perustu virhealttiiseen testaamiseen.
  • Oikeellisuuden todistamista ei kurssilla suoriteta käsin, vaan keskitytään automaattiseen, eli tietokoneavusteisesti tehtävään verifiointiin.
  • Kurssilla luodaan yleiskatsaus aikalogiikkaan ja automaattiteoriaan, sekä niiden käytännön sovelluksiin rinnakkaisten ja reaktiivisten järjestelmien kuvaamisessa ja verifioinnissa. Erityisesti painotetaan äärellistilaisia rinnakkaisjärjestelmiä, niiden ominaisuuksien algoritmista verifiointia, sekä verifiointiin liittyvää laskennallisen kompleksisuuden hallintaa.
  • Vaikka kurssi nojaa vahvasti teoreettiseen ainekseen, tulee asioiden käsittelytapa olemaan 'käytännönläheinen', ja runsaasti konkreettisia esimerkkejä sisältävä.

    • Esitiedot

  • Kurssin sisällön omaksumista helpottaa matemaattisen ajattelutaidon omaaminen, eli kurssista Ohjelmien ja laskennan perusmallit, sekä matematiikan laitoksen kursseista Logiikka ja Diskreetti matematiikka yms. on kurssin suorittamisen kannalta hyötyä
  • Esimerkkien ymmärtämisen kannalta Rinnakkaisohjelmistot-kurssista on suurta hyötyä

    • Sisältö

  • Johdanto, Promela-kieli, Rinnakkaisohjelman tila ja suoritukset (luentomoniste sivut 1-13)
  • Rinnakkaisohjelman toiminnan malli, saavutettavuusverkko, lukkiumien ja tilaväittämien verifiointi (luentomoniste sivut 14-29)
  • Lineaarinen temporaalilogiikka (luentomoniste sivut 29-33)
  • Reiluus ja sen esittäminen temporaalilogiikan avulla. Datariippumattomuus. (luentomoniste sivut 33-43)
  • Äärelliset automaatit äärettömillä syötteillä (Thayse 89 sivut 171-179)
  • LTL-kaavojen verifiointi automaattiteoriaa soveltaen (luentomoniste sivut 44-55)
  • Muistinhallinta Spinissä (Holzmann 91 luku 13, Holzmann 97)
    •

    Oppimateriaali

  • Kurssimateriaalia ja aihepiiriin liittyviä linkkejä
  • Luentomoniste
  • Spin-sivulta löytyvät Promela- ja Spin-ohjeet.
  • Thayse (ed.), From modal logic to inductive databases, sivut 171-179, 1989.
  • Holzmann, Design and Validation of Computer Protocols, luku 13, 1991.
  • Holzmann, The Model Checker Spin, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997
  • Kalvokopioita kurssimapissa

    • Arvostelu

  • Kurssikoe 50 pistettä (ks. ajankohta ja koepaikka laitoksen www-sivulta)
  • Laskarit 10 pistettä
    • Page updated Jun 10, 2005