Informace ke kursu "Modelování a verifikace"
("Modelling and Verification")
(ZS 2007/2008)
Oficiální číslo a název kursu:
: 456-358/1: Modelování a verifikace (MaV)
(předmět má standardní stránku v KATISu; je tam i odkaz
na tuto web-stránku)
Přednášející: doc. Petr Jančar (A1046),
Petr.Jancar@vsb.cz ,
Cvičení
vede přednášející, s občasnou pomocí kolegů:
Ing. Martin Kot
Martin.Kot@vsb.cz
Ing. Zdeněk Sawa
Zdenek.Sawa@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í):
- 14.1.2008: zkouška v termínech 28.1. a 22.2. (vypsáno v
Katisu) proběhne na A1023 od 9 hodin. Nástup jednotlivých
zkoušených je v půlhodinových intervalech (9.00, 9.30, 10.00,
10.30, ....) podle času přihlášení (kdo se dříve přihlásí, jde
dříve; pokud se vzájemně dohodnete na výměně pořadí, nemusíte
mi to předem oznamovat).
- 7.1.2008: hromadná konzultace ke zkoušce proběhne
14.1.2008 od 12.30 na A1023.
- 7.1.2008: Individuální písemné zprávy za druhý projekt
(pdf-soubor, plus odladěné soubory pro UppAal)
pošlete emailem M. Kotovi do 20.1.
- 21.12.2007: Informace k průběhu zkoušky jsou zde:
zk-prubeh.pdf
- 21.12.2007: dodal jsem slidy k předn. 7 a 8, kde jsem
upravil definice "clock constraints" (a "extended clock
constraints", to se projevilo i v zadání tutoriálu 8)
a opravil jsem definici "region graph".
- 19.12.2007: informace o zkoušce dodám v pátek 21.12.
- (19.10.2007)
Je možné, že obecně budou v úterý po přednášce na webu
mírně upravené slidy oproti středeční verzi před přednáškou.
-
(10.10.2007) Bylo započato postupné budování stránky kursu podle
probíhající výuky.
-
(2.4.2007) Zatím jsou všechny základní informace pouze v Katisu.
Na této stránce se další informace budou objevovat později.
Průběh výuky (v ZS 2007/08):
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.
Poznámka.
Poskytnuté slidy jsou jen základem přednášky a základem pro vaše
vlastní poznámky. Budou pochopitelně doplňovány diskusí, příklady na
tabuli, apod.
I náplň cvičení se bude opírat hlavně o příklady použité v kursech na
univerzitě v Aalborgu. Většinou později dodám i řešení, ale podstatná
je samozřejmě vaše
aktivní účast při řešení příkladů na cvičení (kde si
spolu můžeme vyjasňovat související problémy).
V každém případě řešte nejdříve příklady sami , a pak
se teprve podívejte na uvedené řešení! (Jako vždy, jedině vlastním
popráním se s problémem můžete dojít k hlubšímu pochopení.)
-
8.10.2007:
Přednáška 1
mav-predn01-ho.pdf
Cvičení
Příklady: tut1.pdf
Řešení: tut1-sol.pdf
-
15.10.2007:
Přednáška 2
mav-predn02-ho.pdf
Cvičení
Příklady: tut2.pdf
Řešení: tut2-sol.pdf
-
22.10.2007:
Přednáška 3
mav-predn03-ho.pdf
Cvičení
Příklady: tut3.pdf
Řešení: tut3-sol.pdf
-
29.10.2007:
Doneste si notebooky , kdo můžete (se zprovozněným (wifi)přístupem na
Internet ve škole). M. Kot vysvětlí a nabídne asistenci při
nainstalování
Toto proběhne 7.15 - 8.45 na J401 , a pak normálně
12.30 - 14.00 na E322 .
-
5.11.2007:
Přednáška 4 (opět 7.15 - 8.45 na A1023 ).
mav-predn04-ho.pdf
Cvičení
Příklady: tut4.pdf
Řešení: tut4-sol.pdf
-
12.11.2007:
Notebooky nejsou potřeba.
Přednáška 5 ( 7.15 - 8.45 na A1023 ).
mav-predn05-ho.pdf
Cvičení
Příklady: tut05.pdf
Řešení: tut05-sol.pdf
-
19.11.2007:
Notebooky nejsou potřeba.
Přednáška 6 ( 7.15 - 8.45 na A1023 ).
mav-predn06-ho.pdf (verze
15.11. 9 hod.)
Cvičení
Příklady: tut06.pdf
Řešení: tut06-sol.pdf
-
26.11.2007:
První miniprojekt (Alternating Bit Protocol) .
Ráno 7.15 - 8.45 na J401 , pokračování 12.30 - 14.00 na E322 .
Doneste si notebooky s nainstalovanou CWB a Bisim-Game.
Doufám, že se případně domluvíte na dvojicích
pro společné řešení - stačí jeden notebook pro dvojici.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
261-2).
-
3.12.2007:
Opět 7.15 - 8.45 na J401 , pokračování 12.30 - 14.00 na E322 .
Dokončení individuálních zpráv za první miniprojekt.
Doneste si notebooky.
Instalace a
seznámení se s nástrojem
Zprávy za projekt pošlete M. Kotovi do 9.12.
(Ve formě pdf-souboru, ale navíc zvlášť vstup pro CWB
jako textový soubor.)
-
10.12.2007:
Notebooky nejsou potřeba.
Přednáška 7 ( 7.15 - 8.45 na A1023 ).
mav-predn07-ho.pdf
(upraveno 21.12.)
Cvičení
Příklady: tut07.pdf
Řešení: tut07-sol.pdf
-
17.12.2007:
Notebooky nejsou potřeba.
Přednáška 8 ( 7.15 - 8.45 na A1023 ).
mav-predn08-ho.pdf
(upraveno 21.12.)
Cvičení
Příklady: tut08.pdf
(upraveno 21.12.)
Řešení: tut08-sol.pdf
-
7.1.2008:
Druhý miniprojekt (Gossiping Girls) .
Ráno 7.15 - 8.45 na J401 , pokračování 12.30 - 14.00 na E322 .
Doneste si notebooky s nainstalovaným nástrojem UppAal.
Doufám, že se případně domluvíte na dvojicích
pro společné řešení - stačí jeden notebook pro dvojici.
Doneste si knihy (speciálně se jedná o zadání projektu na str.
262-3).