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

Reaktiivisia järjestelmiä esiintyy monissa sulautetuissa järjestelmissä kuten mikroprosessoreissa, telejä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. tietoliikenne protokollien 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 mallintarkastus algoritmeihin, osittaisjärjestysreduktio menetelmiin, propabilistiseen verifiontiin, ja 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. P. Godefroid: Partial Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, 133 p., 1995, A. Valmari: The State Explosion Problem, 100 p., 1998.

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