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), ensimmäinen tilaisuus 17.1-2001.

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

Kirjallisuus: E.M. Clarke, O. Grumberg, and D.A. Peled: Model Checking, 314 pp., MIT Press 1999. Lisäksi tieteellisiä artikkeleita.

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

Assistentti: DI Timo Latvala, puh. 451 2895, e-mail: tlatvala@cc.hut.fi.