T. Kärkkäinen
Kurssi: Formaalit menetelmät 2001

OHJEET SEMINAARITYÖN TEKEMISEKSI

Kurssiin kuuluu seminaarityö, jonka laskennallinen vaativuus on noin 20 h. Työ tehdään alla olevan listan pohjalta itse valitusta aiheesta ja sen voi tehdä joko yksin tai pareittain (20+20 h). Seminaaritöiden palautus- ja opponointitilaisuus järjestetään 7.5. 12-17 Ag B221.1, jossa jokaisella ryhmällä on puoli tuntia aikaa esitellä omaa työtänsä.

Harjoitustöitä ohjataan kerran viikossa keskiviikkoisin 12-14 mikroluokassa Ag B113.1. Muina aikoina tapahtuvasta neuvonnasta tulee sopia ohjaajien (T&K K) kanssa erikseen.

Seminaarityöstä kirjoitetaan 5-10 sivun mittainen työselostus, jossa kuvataan alkuperäinen ongelma, käytetyt menetelmät sekä aikaansaannokset (määritykset ja mahdolliset ohjelmakoodit).
Ensimmäisen viikon aikana työn tekijä sopii ohjaajan kanssa työn aiheen sekä laatii itse itselleen aikataulun ja esisuunnitelman, jonka mukaan työn tekeminen lomitetaan muuhun opiskeluun. Seminaarityöt esitarkistetaan huhtikuun lopussa, johon mennessä siis täytyy olla (mahdollisimman) lopullinen versio työstä valmiina.

Perusaihe: Ensimmäisissä harjoituksissa tehtyjen käyttötapauksien pohjalta kuvaa niissä esitettyä järjestelmää valitun formaalin menetelmän (Z, PVS, Estelle, ...) mukaisella tavalla. Jos aikaa, intoa ja taitoa riittää, voit myös implementoida kuvaamasi systeemin esim. STL:n avulla.
Tomi Heikkinen: Käyttötapaukset & Z

Z ja STL: Suunnittele ja toteuta rajapinta, jonka avulla Z:n skeemoista voidaan generoida STL-koodia (mahdollisimman) automaattisesti.
Petri Eskelinen ja Esko Heiskanen: C++-koodin generointi Z-kielen skeemoista

``Laboratorioinsinöörikoulutus'': Kurssilla jaettiin lista olemassaolevista formaaleista työkaluista, joista suuri osa on saatavilla ilmaiseksi. Aiheena on itse valita jokin formaali ilmaisjakelutyökalu ja asentaa se. Kun (jos) tämä on onnistunut, kuvataan lyhyesti (vaikkapa esimerkkien avulla) se, mitä kyseisellä työkalulla voi tehdä.
Niko Luojumäki ja Sami Äyrämö: PVS

Automaattijatkot: Kurssin lopussa sivuttiin lyhyesti kuvauskieliä, joiden avulla kuvattiin automaattipohjaisten järjestelmien toimintaa. Aiheena on esitellä jollakin kuvauskielellä jonkin hieman monimutkaisemman järjestelmän toiminnan kuvaus. Lähteeksi löytyy valmiit kopiot ESTELLE, LOTOS, SDL -kirjasta.
Jouni Niemelä: LOTOS-jatkot
Antti Viinikka: EESTELLE-jatkot

Oma aihe: Tee seminaarityö valitsemastasi aiheesta, joka liittyy kurssilla käsiteltyihin teemoihin. Tässä tapauksessa aihe tulee hyväksyttää kurssin pitäjällä, jonka kanssa sovitaan tarkemmasta sisällöstä.
Antti-Juhani Kaijanaho: Z-skeemojen animointi Haskellin avulla (Haskell-infoa)
Lassi Hietala: Z/EVES