Modely a verifikace chování systémů
Z ωικι.matfyz.cz
| Modely a verifikace chování systémů | ||||
|
přednáší:
cvičení:
Písemka
10. ledna se místo přednášky (tj. od 10.40 v S1) píše písemka. Přehled očekávaných otázek je v poznámkách.
Úkoly
- železniční stanice v Promele
- vlaky, pasažéři, tratě, ...
- verifikovat vlastnosti: vlaky nehavarují, pasažéři se dostanou, kam chtějí, a podobné
- rozsah – má to být model, tj. nějaká abstrakce, abychom tím zase nezabili měsíc
- chce nějakou dokumentaci
- Kofroňovi na mail do konce semestru
- Dekkeruv algoritmus v smv
- Docel jednoduché
Poznámka ke kompilaci smv
Narazil jsem na drobný problém při kompilaci smv.. Mají tam nějak předeklarovanou funkci malloc což se
- Jednak tluče s build in malloc
- Druhak se to špatně vkládá do souboru s gramatikou a nejde to přeložit
Řešení
$ tak -xzf smv.r2.5.3.tar.gz $ cd smv/ $ repalce malloc __malloc -- storage.h $ replace malloc __malloc -- *.c *.h $ make
A už mě to jelo...
Odkazy
- web předmětu
- poznámky z přednášky (OpenOffice)
- poznámky z cvičení (OpenOffice)
- nějaké řešení úlohy DEKKER na zápočet
- nějaké řešení úlohy TRAINSTATION na zápočet
