Modely a verifikace chování systémů: Porovnání verzí

Z ωικι.matfyz.cz
Přejít na: navigace, hledání
(Úkoly)
(Odkazy)
 
Řádka 40: Řádka 40:
 
* [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.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://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 ===
 
=== Nástroje ===
 
* [http://spinroot.com/ Spin] – checker, jehož vstupním jazykem je PROMELA, jazyk zápočťáku
 
* [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
 
* [http://www.cis.ksu.edu/bandera Bandera] – Javu pitvající nadstavba nad Spin

Aktuální verze z 6. 1. 2007, 16:02

Modely a verifikace chování systémů
Kód předmětu: NSWI101
Přednáší: František Plášil

přednáší:

cvičení:

Písemka[editovat | editovat zdroj]

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[editovat | editovat zdroj]

ž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[editovat | editovat zdroj]

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í[editovat | editovat zdroj]

$ 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[editovat | editovat zdroj]

Nástroje[editovat | editovat zdroj]

  • Spin – checker, jehož vstupním jazykem je PROMELA, jazyk zápočťáku
  • Bandera – Javu pitvající nadstavba nad Spin