Informace ke kursu "Modelování a verifikace"
("Modelling and Verification")
(ZS 2008/2009)
Oficiální číslo a název kursu:
: 456-358/1: Modelování a verifikace (MaV)
(předmět má standardní stránku v Edisonu; je tam i odkaz
na tuto web-stránku)
Přednášející: prof. Petr Jančar (A1046),
Petr.Jancar@vsb.cz ,
Cvičení
vede přednášející nebo cvičící
Ing. Martin Kot
Martin.Kot@vsb.cz
Acknowledgement.
The course is based on the book
Reactive Systems: Modelling, Specification and Verification
by Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen,
Jiří Srba,
Cambridge University Press, August 2007.
Petr Jančar gratefully acknowledges the help of materials provided
by the authors of the book at the web-page
www.cs.aau.dk/rsbook,
including the latex-sources of the slides provided by J. Srba;
the slides (with slight modifications and/or extensions) are also used
in our course, as well as the suggested tutorials.
Aktuální důležité informace (v obráceném chronologickém pořadí):
- 29.9.2008:
Do Edisonu byly zavedeny úkoly k absolvování.
Do zápočtu se počítají dva projekty (CWB a UPPAAL), za něž lze získat
dohromady 30 bodů. (V krajním případě je zápočet udělen i za jeden
projekt, za minimálně 10 bodů.)
Zkouška je písemná a ústní, za max. 70 bodů (požadované minimum 25
bodů).
- 29.9.2008:
Pro pořádek zde opakuji (mírně upravenou) zprávu,
kterou jsem zaslal studentům emailem na začátku
semestru:
Předmět bude mít podobnou náplň jako loni,
tedy jak je to patrno z
MaV 2007.
První dva týdny povede veškerou výuku M. Kot
(já jsem nepřítomen).
Domluvili jsme se, že začnete instalací a prvním seznámením se
se softwarovými nástroji, což se loni konalo až ve 4. a 9. výukovém
týdnu (podívejte se tam).
Troufám si předpokládat, že každý máte svůj notebook, který si přinesete
(se zprovozněným (wifi)přístupem na Internet ve škole),
stačí ale pracovat po dvojicích (a mít alespoň počítač doma, kde si to
můžete nainstalovat).
Mám na sebe půjčeny knihy k předmětu. Po špatné zkušenosti z loňska
(jeden student zmizel i s knihou), dám knihy na sekretariát katedry
informatiky, kde si je můžete oficiálně vypůjčit.
(Je velmi žádoucí, ať máte každý svůj výtisk.)
Požadavky k absolvování vám vysvětlí M. Kot.
Do Edisonu je dám až koncem září.
Průběh výuky (v ZS 2008/09):
Základním materiálem kursu je kniha
Reactive Systems: Modelling, Specification and Verification
autoři: Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen,
Jiří Srba
vydavatel: Cambridge University Press, August 2007
Autoři knihy zřídili webovskou stránku
www.cs.aau.dk/rsbook
která obsahuje odkazy na další související a velmi užitečné materiály.
Mj. tam lze nalézt i zdroje slidů (nezištně poskytnuté Jiřím Srbou),
které jsou využity jako základ prezentačních slidů i u našeho kursu.
Níže budu podle potřeby doplňovat informace o průběhu výuky v letošním
roce. Užitečný ale stále bude následující odkaz na loňský rok, tam
najdete slidy k přednáškám, zadání cvičení apod.:
MaV 2007.
-
17.9.2008:
Instalace a seznámení se s CWB (viz 4: 29.10.2007 v MaV 2007)
-
24.9.2008:
Instalace a seznámení se s UppAal (viz 9: 3.12.2007 v MaV 2007)
-
1.10.2008:
Přednáška a cvičení 1 (viz MaV 2007, podobně dále)
-
8.10.2008:
Přednáška a cvičení 2
-
15.10.2008:
Přednáška a cvičení 3
-
22.10.2008:
Přednáška a cvičení 4
-
29.10.2008:
Přednáška a cvičení 5
-
5.11.2008:
Přednáška a cvičení 6
-
12.11.2008:
První miniprojekt (Alternating Bit Protocol) .
Doneste si notebooky s nainstalovanou CWB a Bisim-Game.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
261-2).
-
19.11.2008:
Dokončení individuálních zpráv za první miniprojekt.
Diskuse a doplnění dosud probrané látky.
-
26.11.2008:
Přednáška a cvičení 7
-
3.12.2008:
Přednáška a cvičení 8
-
10.12.2008:
Druhý miniprojekt (Gossiping Girls) .
Doneste si notebooky s nainstalovaným nástrojem UppAal.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
262-3).
-
17.12.2008:
Dokončení individuálních zpráv za druhý miniprojekt.
Diskuse a doplnění probrané látky.
Diskuse k formě zkoušky.