Informace ke kursu "Modelování a verifikace"
("Modelling and Verification")
(ZS 2009/2010)
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í):
- 11.9.2009: Poprve se
sejdeme ve stredu 16.9. v 16 hod. na A1023 .
- 28.8.2009:
V případě, že předmět nebude nasazen v rozvrhu (vzhledem k malému
počtu zapsaných), domluvíme se před zahájením semestru emailem na době a místu
konání výuky.
- 28.8.2009:
O obsahu a průběhu kursu si uděláte dobrou představu z dřívějších
stránek odkazovaných níže u průběhu výuky.
Součástí kursu je instalace a práce s jistými (volně přístupnými)
softwarovými nástroji.
V této souvislosti si troufám předpokládat,
že každý máte svůj notebook, který si přinesete, až bude potřeba
(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
(jeden student zmizel i s knihou), dám knihy po zahájení výuky
na sekretariát katedry
informatiky, kde si je můžete oficiálně vypůjčit.
(Je velmi užitečné, když máte každý svůj výtisk.)
Studijní materiály:
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.
Podmínky absolvování:
V Edisonu jsou uvedeny ú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ů).
Průběh výuky (v ZS 2009/10):
Níže budu postupně uvádět a aktualizovat informace o průběhu výuky v letošním
roce. Užitečné ale stále budou následující odkazy na dřívější běhy
kursu; tam
najdete slidy k přednáškám, zadání cvičení apod.:
MaV 2007.
MaV 2008.
-
16.9.2009:
Přednáška 1
mav-predn01-ho.pdf
Cvičení
Příklady: tut1.pdf
-
23.9.2009:
Přednáška 2
mav-predn02-ho.pdf
Cvičení
Příklady: tut2.pdf
-
30.9.2009:
Přednáška 3
mav-predn03-ho.pdf
Cvičení
Příklady: tut3.pdf
-
7.10.2009:
Přednáška 4
mav-predn04-ho.pdf
Cvičení
Příklady: tut4.pdf
-
14.10.2009:
Přednáška 5
mav-predn05-ho.pdf
Cvičení
Příklady: tut05.pdf
-
21.10.2009:
Přednáška 6
mav-predn06-ho.pdf
Cvičení
Příklady: tut06.pdf
-
28.10.2009:
Výuka není (státní svátek).
-
4.11.2009:
Doneste si notebooky (se zprovozněným (wifi)přístupem na
Internet ve škole). M. Kot vysvětlí a nabídne asistenci při
nainstalování
Pak hned následuje:
První miniprojekt (Alternating Bit Protocol) .
(Jsou potřeba notebooky s nainstalovanou CWB a Bisim-Game.)
Řešení je možné provádět (či jen vzájemně konzultovat)
ve dvojici.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
261-2).
-
11.11.2009:
Doneste si notebooky.
Dokončení prvního miniprojektu, vzájemná diskuse různých řešení,
zpracování kostry individuálních zpráv za první miniprojekt.
Definitivní zprávy za projekt pak pošlete M. Kotovi do s ním dohodnutého data.
(Ve formě pdf-souboru, ale navíc zvlášť vstup pro CWB
jako textový soubor.)
-
18.11.2009:
Přednáška 7
mav-predn07-ho.pdf
Cvičení
Příklady: tut07.pdf
-
25.11.2009:
Přednáška 8
mav-predn08-ho.pdf
Cvičení
Příklady: tut08.pdf
-
2.12.2009:
Doneste si notebooky.
M. Kot pomůže s instalací a seznámením se
s nástrojem
Pak hned následuje:
Druhý miniprojekt (Gossiping Girls) .
(Jsou potřeba notebooky s nainstalovaným nástrojem UppAal.)
Řešení je možné provádět (či jen vzájemně konzultovat)
ve dvojici.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
262-3).
-
9.12.2009:
Doneste si notebooky.
Dokončení druhého miniprojektu, vzájemná diskuse různých řešení,
zpracování kostry individuálních zpráv za miniprojekt.
Definitivní zprávy za projekt pak pošlete M. Kotovi do s ním dohodnutého data.
-
16.12.2009:
Dokončení vybraných témat kurzu s jejich případným rozšířením.
Shrnutí obsahu kurzu. Diskuse závěrečné zkoušky.