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

Z ωικι.matfyz.cz
Přejít na: navigace, hledání
(+písemka)
(Úkoly)
Řádka 17: Řádka 17:
 
* chce nějakou dokumentaci
 
* chce nějakou dokumentaci
 
* Kofroňovi na mail do konce semestru
 
* Kofroňovi na mail do konce semestru
 +
 +
 +
== 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 ==
 
== Odkazy ==

Verze z 12. 12. 2006, 17:58

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

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


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

Nástroje

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