TCS / Teaching / Tik-79.186
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Tik-79.186 Reaktiiviset järjestelmät (2 ov)

Kevät 2000


Reaktiivisia järjestelmiä esiintyy monissa sulautetuissa järjestelmissä kuten mikroprosessoreissa, telekommunikaatiojärjestelmissä, sekä tietoverkoissa. Niille keskeinen piirre on jatkuva toiminta ja reagoiminen ympäristöstä tuleviin tapahtumiin.

Reaktiivisten järjestelmien mallinnus ja verifiointi on tullut osaksi jokapäiväistä järjestelmäkehitystä jo mikropiirien osalta. Samoja tekniikoita voidaan myös käyttää mm. tietoliikenneprotokollien suunnittelun ja toteutuksen apuvälineenä.

Vuoden 1997 "tietotekniikan Nobel", A. M. Turing-palkinto, jaettiin reaktiivisten järjestelmien verifioinnin pioneerille Amir Pnuelille:

"It is time that formal verification (of both software and hardware systems) be demoted from an art practiced by the enlightened few to an activity routinely and mundanely performed by a cadre of Verification Engineers (a new profession), as a standard part of the system development process."

Kurssin sisältönä on reaktiivisten järjestelmien mallinnus, ominaisuuksien spesifionti temporaalilogiikalla, ja niiden verifiointi. Lisäksi tutustutaan mallintarkastusalgoritmeihin, osittaisjärjestyksiin perustuviin reduktiomenetelmiin, propabilistiseen verifiontiin, sekä kyseisten menetelmien teoreettiseen perustaan.

Kurssin suoritus: Seminaariesitelmät ja kotitehtävä.

Luennot: ke 16.30-18 sali TB353 (TT-talo).

Harjoitukset: ke 18-19 sali TB353 (TT-talo).

Kirjallisuus: Alan väitöskirjoja ja tieteellisiä artikkeleita, mm. A. Valmari: The State Explosion Problem, 100 p., 1998.

Luennoitsija: TkL Keijo Heljanko, puh. 451 3256, e-mail: Keijo.Heljanko@hut.fi, vastaanotto ma 13-14 huone TB352.

  • Kevään 2000 alustava ohjelma

  • Keijo.Heljanko@hut.fi, Last modified January 27, 2000.