{{predmet|Modely a verifikace chování systémů|František Plášil|SWI101}}
přednáší:
* [[František Plášil]]
* [[Jiří Adámek]]
cvičení:
* [[Jan Kofroň]]
== 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 ==
* [http://nenya.ms.mff.cuni.cz/~adamek/fm/ web předmětu]
* [http://urtax.ms.mff.cuni.cz/~novap2am/poznamky/chovani.sxw poznámky z přednášky] (OpenOffice)
* [http://urtax.ms.mff.cuni.cz/~novap2am/poznamky/chovani_cviceni.sxw poznámky z cvičení] (OpenOffice)
* [http://vanocnibesidka.wz.cz/other/skola/modelchecking/smv.html nějaké řešení úlohy DEKKER na zápočet]
* [http://vanocnibesidka.wz.cz/other/skola/modelchecking/trainstation_spin_promela.html nějaké řešení úlohy TRAINSTATION na zápočet]
=== Nástroje ===
* [http://spinroot.com/ Spin] – checker, jehož vstupním jazykem je PROMELA, jazyk zápočťáku
* [http://www.cis.ksu.edu/bandera Bandera] – Javu pitvající nadstavba nad Spin
