Modely a verifikace chování systémů

From ωικι.matfyz.cz

Modely a verifikace chování systémů

Kód předmětu: SWI101 (http://is.cuni.cz/studium/predmety/index.php?do=predmet&kod=NSWI101) Přednáší: František Plášil

přednáší:

• František Plášil
• Jiří Adámek

cvičení:

• Jan Kofroň

Table of contents

1 Písemka 2 Úkoly 3 Poznámka ke kompilaci smv 3.1 Řešení 4 Odkazy 4.1 Nástroje

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 (http://nenya.ms.mff.cuni.cz/~adamek/fm/)
• poznámky z přednášky (http://urtax.ms.mff.cuni.cz/~novap2am/poznamky/chovani.sxw) (OpenOffice)
• poznámky z cvičení (http://urtax.ms.mff.cuni.cz/~novap2am/poznamky/chovani_cviceni.sxw) (OpenOffice)
• nějaké řešení úlohy DEKKER na zápočet (http://vanocnibesidka.wz.cz/other/skola/modelchecking/smv.html)
• nějaké řešení úlohy TRAINSTATION na zápočet (http://vanocnibesidka.wz.cz/other/skola/modelchecking/trainstation_spin_promela.html)

Nástroje

• Spin (http://spinroot.com/) – checker, jehož vstupním jazykem je PROMELA, jazyk zápočťáku
• Bandera (http://www.cis.ksu.edu/bandera) – Javu pitvající nadstavba nad Spin