FEI archív 2010/2011 > 4. ročník

FŠS - Formálne špecifikácie systémov

<< < (2/2)

Faust:
do kedy treba koreckovi poslat ten "referat" ?

azalie:
cawko. mam dotaz. co treba psiat k tymto teoretickym otazkam???

B jazyk, definicia vlatnosti
sysntax struktury MASCHINE N(p) a jeho vlastnosti
Jazyk „guarded commands“.
Sémantika Machine N(p):štruktúra povinného dôkazu korektnosti špecifikácie stroja Machine N(p).(Proof Obligation for
Machine N(p)
Mechanizmus ";" dokaz jeho korektnosti, platnosti pre vlastnosti 1-4

Neviem kde najdem odpoved v tom koreckovom PDF. dik za odpoved

Faust:
mna by zaujimalo ake boli otazky na 1.termine, moze niekto napisat? dik

Faust:
btw kde najdem teoriu k tejto otazke? vektorove aditivne systemy. Vztah VAS a petriho sieti ..v tych podkladoch od korecka tam take nieje ak sa nemylim

jan:
Heslo do moodle: jahodka

Skúška: otázky boli tie čo sú hore
Zadanie: každý mal urobiť referát na nejakú tému (napr. Petriho siete v biochémii)
DU: Urobiť B-MACHINE ten čo je dole
K cvičeniu: na cvičení sa chodí k tabuli, kto chce. Systém  je taký, že za aktivitu je napr. 10 bodov, smerodajné je koľko krát bol maximálne niekto pri tabuli, keď to bude napr. 5, tak sa vypočíta cena jedného počítania pri tabuli ako 10/5=2 body. Takže ten čo bol pri tabuli tých 5 krát, dostane full, čiže 10 bodov a keď sa niekomu nechcelo a bol tam len raz, dostane 2 body (1 účasť x 2 body = 2 body).

Príprava na skúšku:
- Základným učebným materiálom je [1], toto treba prečítať celé, kapitoly 2.6.2, 2.6.3, väčšinu kapitoly 2.7 a v kapitole 3.3 "Príkaz DO" som ja osobne preskočil.
- Z literatúry [2] treba hlavne kapitoly 3 (tá je ale preložená v literatúre [1]) a asi 4 a 7.
- Z literatúry [3] treba tiež len niečo, podľa toho čo povie na prednáške.
- Literatúra [4]. Toto si treba pozrieť a použiť na doplnenie informácií, ktoré nie sú v [1][2][3], ale väčšna je v [1], keďže Ing. Korečko písal [1] podľa prednášok Prof. Hudáka a Prof. Hudák tieto materiály [4] používa na prednáškach.
- Čo sa týka príkladov, na cvičení sa počítajú príklady z [5] + treba vedieť urobiť kód B-MACHINE (viď. dole) + nakresliť PS obedujúcich filozofov (odrázok hore).

Archív zo všetkými materiálmi:
http://www.uloz.to/9389262/zhrnutie-rar

Učebné materiály

Zo stránky Ing. Korečka (http://hornad.fei.tuke.sk/~korecko/fss/):
[1] SK_FSpodklady.pdf - http://hornad.fei.tuke.sk/~korecko/fss/SK_FSpodklady.pdf
[2] Materiál k jednej prednáške - An Introduction to the Theoretical Aspects of Coloured Petri Nets - http://hornad.fei.tuke.sk/~korecko/fss/CPNtheory.pdf

Doplňujúce materiály od Prof. Hudáka (v archíve):
[3] Materiál k jednej prednáške - Štefan Hudák - Rozšírenia Petriho Sietí - habilitačná práca.pdf (https://docs.google.com/leaf?id=0B9X-L5lO6y2YOWVmZjhkMDctOWIzZC00Njc2LTkyNmEtZjdhNWU2OTNiMWJm&hl=en_US&authkey=CMyAtZsG)

Z moodlu od Prof. Hudáka (aj v archíve)
[4] - 6 súborov pdf

Na cvičenie (len v archíve):
[5] cvika2007 zosvetlene.pdf

Možno sa tiež zíde (len v archíve):
[6] prednasky2007.pdf

Okruhy otázok:
[7] Tematické okruhy ku skúške z predmetu Formálne špecifikácie systémov; akad. rok 2010/2011 - FSSTemySkOtazok.doc
[8] Teoretické otázky pre študentov ŠpZ - http://hornad.fei.tuke.sk/~korecko/fss/FSS_SpZ_teoretOtazky.pdf

Potrebný softvér:

B-MACHINE
[9] ProB - http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download
[10] Atelier B - http://www.atelierb.eu/index-en.php

Petriho siete
[11] PNtool 2 (školský projekt) - http://hornad.fei.tuke.sk/~korecko/fss/index.html

Farebne Petriho siete
[12] CPN tools - http://cpntools.org/


príklad B-MACHINE z cvičenia:

vysvetlenie zápisu B-MACHINE(abstraktného stroja) a jeho klauzúl (CONSTRAINTS, ...) je v literatúre [1] na stranách 61-64


--- Code: ---MACHINE Scalar( max_val )

 CONSTRAINTS max_val:NAT & max_val>=0

 ABSTRACT_VARIABLES val

 INVARIANT  val : 0 .. 10

 INITIALISATION val := 0

 OPERATIONS

     retVal <-- getVal =
     BEGIN
         retVal := val
     END ;

     setVal ( amount ) =
     PRE amount : NAT THEN
         IF amount <= max_val & amount >= 0 THEN val := amount END
     END ;

     incVal ( amount ) =
     PRE amount : NAT THEN
         IF val < max_val THEN val := val + 1 END
     END ;

     decVal ( amount ) =
     PRE amount : NAT THEN
         IF val > 0 THEN val := val - 1 END
     END ;

     maximum <-- maxVal ( xx ) =
     PRE xx : INT THEN
         IF xx > val THEN maximum := xx ELSE maximum := val END
     END ;

     incORdecVal ( amount ) =
     PRE amount : NAT THEN
                CHOICE
                    IF val > 0 THEN val := val - 1 END
                OR
                    IF val < max_val THEN val := val + 1 END
                END
     END
 END

--- End code ---

Navigácia

[0] Index správ

[*] Predchádzajúca strana