{{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-xzfsmv.r\mathrm{2.5.3.}tar.gz$ cd smv/

ParseError: KaTeX parse error: Expected group after '_' at position 17: …repalce malloc _̲_malloc -- stor…

$ 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

Nástroje

• Spin – checker, jehož vstupním jazykem je PROMELA, jazyk zápočťáku

• Bandera – Javu pitvající nadstavba nad Spin