Spesifioinnin ja verifioinnin perusteet
Esitiedot
Esitietoina oletetaan Tietoliikenne I ja Rinnakkaisohjelmistot.
Kurssi on kuitenkin varsin formaali, joten sen kykenee suorittamaan
ilman kyseisten kurssien tietoja, jos omaksuu abstrakteja
asioita helposti.
Kurssin sisältö
- Tilasiirtymäsysteemit ja prosessien mallinnus niiden avulla.
- AB-protokolla ja sen esitys tilasiirtymäsysteeminä.
- Yhteistilaverkko.
- Heikko bisimulaatioekvivalenssi.
- Ekvivalenssipohjainen verifiointi.
- Perus-Lotos.
- Johdatus täyteen Lotokseen.
- Protokollien spesifiointia ja verifiointia Lotoksella.
- Johdatus mallintarkastukseen.
Materiaali
Ei ole olemassa yksittäistä oppikirjaa, joka kattaisi kaikki kurssilla
vaadittavat asiat. Luennot on koottu monisteeksi, joka on saatavilla
kurssisivun kautta.
Erilliskuulustelun vaatimukset
Erilliskuulusteluissa vaaditaan yllä mainitut asiat siinä laajuudessa,
kuin niitä on käsitelty monisteessa.