T-79.179 Rinnakkaiset ja hajautetut digitaaliset järjestelmät (3 ov)

Rinnakkaiset ja hajautetut järjestelmät ovat merkittävä tietokoneiden käyttökohde. Muun muassa tietoliikenteen yhteyskäytäntöjen, asiakas-palvelin-järjestelmien, sulautettujen järjestelmien ja prosessinohjauksen suunnittelijat tarvitsevat näkemystä rinnakkaisuudesta ja hajautuksesta ja siihen liittyvistä ilmiöistä. Suunnittelussa törmätään vaikeisiin ajoitusongelmiin, joiden ratkaisemisessa on hyötyä järjestelmällisistä, formaaleista menetelmistä ja tehokkaista työkaluohjelmistoista.

Opintojakson tavoitteena on johdattaa opiskelija tuntemaan muutamia näiden järjestelmien mallinnuksessa ja analyysissä käytettyjä formalismeja ja menetelmiä. Luennot käsittelevät pääasiassa Petri-verkkojen, aikalogiikan ja prosessialgebran perusteita sekä niiden käyttöä. Lisäksi opintojaksoon liittyy laskuharjoituksia ja pakollisia kotitehtäviä, joissa harjoitellaan mallinusmenetelmiä ja esitellään teorian sovelluskohteita. Kotitehtävien ratkaisemisessa käytetään Tietojenkäsittelyteorian laboratoriossa kehitettyä korkean tason Petri-verkkojen Maria-analyysiohjelmistoa.

Yleistä

Kurssiesite
Ilmoittautuminen: Kurssille ilmoittaudutaan TOPI-järjestelmän välityksellä.
Keskusteluryhmä: opinnot.tik.rhj
Kurssin suorittaminen: 5 pakollista kotitehtävää ja tentti.

Aineisto

Ethän kuormita ATK-keskuksen tulostimia näillä. Jos haluat monisteet paperilla, tilaa opetusmonisteet.

Luennot, ma 16–18 T2, Marko Mäkelä

luento 1, 20.1.2003 (kalvon 1-23 kuva korjattu 14.4.2003)

Johdanto: PDF, Postscript

luento 2, 27.1.2003

Paikka–siirtymä-verkot: PDF, Postscript

luento 3, 3.2.2003 (korjattu 17.3.2003, kalvon 3-16 kuva korjattu 14.4.2003)

Korkean tason verkot: PDF, Postscript

luento 4, 10.2.2003

Johdatus Maria-työkaluun: PDF, Postscript

luento 5, 24.2.2003

Aikalogiikka ja mallintarkastusmenetelmät: PDF, Postscript

luento 6, 3.3.2003

Saavutettavuusanalyysin toteuttaminen ja tehostaminen: PDF, Postscript

luento 7, 10.3.2003

Rakenteellinen analyysi: PDF, Postscript

luento 8, 17.3.2003

Stokastinen analyysi: PDF, Postscript

luento 9, 24.3.2003 (kalvon 9-9 yläkuva korjattu 24.3.2003)

Prosessialgebra: PDF, Postscript

kertausluento, 28.4.2003

luennot 1–9 sekä kotitehtävien mallivastauksia
Maria-ohjelmiston käyttöohje
Laskuharjoitukset, pe 10–12 T2, Jukka Honkola

laskuharjoitus 1

31.1.2003: PDF, Postscript. Vastaukset: PDF, Postscript.

laskuharjoitus 2

7.2.2003: PDF, Postscript. Vastaukset: PDF, Postscript.

laskuharjoitus 3

14.2.2003: PDF, Postscript. Vastaukset: PDF, Postscript.

laskuharjoitus 4 (Maari-C)

21.2.2003: PDF, Postscript. Vastaukset: Maria-tiedostoja.

laskuharjoitus 5

28.2.2003: PDF, Postscript. Vastaukset (korjattu 4.3.2003): PDF, Postscript.

laskuharjoitus 6 (Maari-C)

7.3.2003: PDF, Postscript. Vastaukset: PDF, Postscript.

laskuharjoitus 7

14.3.2003: PDF, Postscript. Vastaukset (korjattu 14.3.2003): PDF, Postscript.

laskuharjoitus 8 (Maari-C)

28.3.2003: PDF, Postscript. Vastaukset: PDF, Postscript.
Oheislukemista

Mallintarkastus

Advanced Tutorial on Model Checking, Javier Esparza and Stephan Merz: PDF

Kotitehtävät

Kurssilla on viisi pakollista kotitehtävää, jotka arvostellaan. Koska kukin kotitehtävä on 10 pisteen arvoinen, jaossa on yhteensä 50 pistettä. Kurssin hyväksytty suorittaminen edellyttää hyväksytyn tenttisuorituksen sekä vähintään 25 kotitehtäväpistettä. Jos kotitehtäväpisteitä on paljon, ne vaikuttavat kurssista annettavaan arvosanaan korottamalla tentin hyväksyttyä arvosanaa enintään kahdella pykälällä. Tarkat pisterajat ilmoitetaan myöhemmin.

Kotitehtävien tulokset julkaistaan kurssin kotisivulla ja opinnot.tik.rhj-ryhmässä.

Kurssin läpäiseminen edellyttää hyväksytyn tenttisuorituksen lisäksi puolet kotitehtäväpisteistä eli 25 pistettä. Jos kotitehtävistä saa enemmän kuin 30 pistettä, tentin arvosana voi nousta enintään kahdella numerolla.

Kotitehtävät eivät ole ryhmätöitä. Yleisiä ratkaisuperiaatteita voi toki pohtia ryhmässä, mutta kukin palauttaa oman ratkaisunsa.

Kotitehtävä 1, 27.1.2003: Yksinkertainen asiakas–palvelin-järjestelmä: PDF, Postscript; Vaihtoehto: käytä Maria-työkalua jonkin pulman mallintamiseen ja ratkaisemiseen. Kysy luennoitsijan (Marko Mäkelä) hyväksyntä pulmallesi ja palauta vastauksesi luennoitsijalle.
Kotitehtävä 2, 10.2.2003, palautus 10.3.2003 klo 16.00: Turvallisuuskriittisen järjestelmän suunnitteleminen ja tarkistaminen: PDF, Postscript
Kotitehtävä 3, 10.2.2003, palautus 24.3.2003 klo 16.00: Vaihtuvan bitin yhteyskäytännön mallintaminen: PDF, Postscript. Korjaus 20.3.2003: poistettu 3. kohdan viimeinen kysymys, joka oli jäänyt tehtävänantoon vahingossa. Kaikkien 3. kohdassa tehtävien saavutettavuusgraafien pitäisi olla vahvasti yhtenäisiä.
Kotitehtävä 4, 3.3.2003, palautus 7.4.2003 klo 16.00: Aikalogiikkaa ja invarianttilaskentaa: PDF, Postscript.
Kotitehtävä 5, 24.3.2003, palautus 24.4.2003 klo 16.00: Prosessialgebraa ja suorituskyvyn määrittämistä: PDF, Postscript, siirtymäjärjestelmä. Lisäys 22.4.2003: sum(Q,2) ei toimi Octave 2.0:ssa. Sen sijaan sum(Q') toimii.

Maria-esimerkkejä

Eräät luennolla esitetyt korkean tason verkot ovat saatavissa Maria-ohjelmiston ymmärtämässä muodossa.

Lautturin ongelma: kaalinpää, vuohi ja susi
Pääsylippualgoritmi: n prosessin keskinäinen poissulkevuus jaetun muistin järjestelmässä)

Muita esimerkkejä

Dekkerin algoritmi TVT-muodossa: Katso myös, miten Maria tarkastaa LTL-kaavoja kytkiessään LSTS-malleja rinnan.

Tentti

Kursseilla T-79.179 ja T-79.231 on yhteinen tentti.

12.5.2003: PDF, Postscript.
5.9.2003: PDF, Postscript. Arvosteluun voi tutustua 19.9.2003 saakka Innopoli 2:n huoneessa C 318 sopimuksen mukaan.

Marko Mäkelä