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.