Teknillinen korkeakoulu, 
     Tietojenkäsittelyteorian laboratorio

T-79.146 Logiikka tietotekniikassa: erityiskysymyksiä I (2 ov)

Kevät 2005

Opintojakson tavoitteena on perehtyä modaalilogiikkojen malli- ja todistusteoriaan, todistusmenetelmiin ja laskennallisiin ominaisuuksiin sekä tämäntyyppisten logiikkojen ajankohtaisiin sovellutuksiin tietotekniikassa. Tämän kevään teemana on temporaalilogiikan sovellutukset rinnakkaisissa ja hajautetuissa järjestelmissä.

Temporaalilogiikka on noussut keskeiseksi lähestymistavaksi rinnakkaisten ja hajautettujen järjestelmien, kuten tietoliikenne- ja ohjausjärjestelmien, kehitystyössä. Se tarjoaa käyttökelpoisen menetelmän spesifioida ko. järjestelmiä ja sen pohjalta on kehitetty tehokkaita automaattisia työkaluja järjestelmien oikeellisuuden varmentamiseen. Tällaisten formaalien menetelmien käyttö lisääntyy teollisuudessa voimakkaasti:

The use of formal verification tools is well established and becoming more so. Simulation- and emulation-based methodologies aren't sufficient to guarantee correctness with today's complex chips. (Carl Pixley, Motorola Inc. in IEEE Spectrum, Jan 1997, p. 61)

Opintojaksolla tutustutaan keskeisimpien sovellutuksissa käytettävien temporaalilogiikkojen (CTL, LTL) semanttiseen pohjaan, ilmaisuvoimaan, laskennalliseen vaativuuteen ja käytettävien automaattisten työkalujen (mallintarkistimet, teoreemantodistimet) toteutusperiaatteisiin sekä sovellutuksiin.

Opintojakso soveltuu kaikille logiikasta ja formaaleista menetelmistä kiinnostuneille sekä jatko-opiskelijoille mukaanlukien HeCSEn (Helsinki Graduate School in Computer Science and Engineering) opiskelijat. Kurssi koostuu luennoista, laskuharjoituksista ja kotitehtävistä. Kurssin suorittaminen edellyttää kotitehtävien ratkaisemista ja tentin suorittamista.