Hardver- és szoftverrendszerek verifikációja

A verifikáció szükségessége......Page 7
Verifikációs módszerek......Page 8
Szoftver verifikáció......Page 9
Hardver verifikáció......Page 11
Modell-ellenőrzés......Page 12
A modellezési fázis......Page 13
Az elemzési fázis......Page 15
A modell-ellenőrzés előnyei......Page 17
A modell-ellenőrzés hátrányai......Page 18
Egyszerű átmeneti rendszerek......Page 20
Utak átmeneti rendszerekben......Page 21
Címkézett átmeneti rendszerek......Page 22
Paraméterezett átmeneti rendszerek......Page 23
Átmeneti rendszerek homomorfizmusai......Page 24
Szekvenciális áramkörök......Page 26
Boole változók......Page 27
Korlátos pufferek......Page 28
Szekvenciális programok......Page 30
A Peterson algoritmus......Page 31
Petri hálók......Page 33
Átmeneti rendszerek szabad szorzata......Page 35
Szinkron és aszinkron rendszerek......Page 36
Szinkronizációs vektorok......Page 37
A szinkronizált szorzat definíciója......Page 38
Definíció......Page 39
Az alternáló bit protokoll......Page 40
Időzített rendszerek......Page 44
Időzített átmeneti rendszerek......Page 45
Időzített automaták......Page 46
Az időzített automaták szintaxisa......Page 47
Az időzített automaták szemantikája......Page 50
Időzített automaták szorzata......Page 52
Kijelentés logika (Propositional Logic)......Page 56
Lineáris temporális logika (Linear Temporal Logic)......Page 58
HML logika (Hennessy-Milner logika)......Page 61
Dicky logika......Page 62
CTL (Computation Tree Logic)......Page 64
CTL* logika......Page 68
LTL, CTL és CTL* logikák kifejezőerejének összehasonlítása......Page 69
TCTL logika (Timed Computation Tree Logic)......Page 70
A modell-ellenőrzés alapfeladata......Page 74
A CTL modell-ellenőrzés algoritmusa......Page 75
CTL modell-ellenőrzési algoritmus megvalósítása......Page 77
Halmaz reprezentálása ROBDD-vel......Page 80
Műveletek ROBDD-k felett......Page 84
Szimbolikus CTL modell-ellenőrzés......Page 87
LTL automata-elméleti alapú modell-ellenőrzés......Page 90
Tabló-módeszer alapú modell-ellenőrzés......Page 95
TCTL modell-ellenőrzés......Page 97
A SPIN fejlesztése és alkalmazásai......Page 104
Processzusok......Page 105
Adat objektumok......Page 107
Üzenet csatornák......Page 109
Szinkron és aszinkron üzenetküldés, randevú csatornák......Page 110
Összetett utasítások......Page 111
Ciklikus esetválasztás......Page 112
Else és timeout......Page 113
Megszakíthatatlan (atomi) lépések......Page 114
Verifikáció a SPIN segítségével......Page 115
Címkék......Page 116
Végállapot címkék......Page 117
Elfogadási címkék......Page 118
Soha állítások......Page 119
LTL formulák......Page 121
Az alternáló bit protokoll modellje......Page 122
UPPAAL......Page 123
Modellek megadása az UPPAAL-ban......Page 124
Automata sablonok szerkesztése......Page 125
Szinkronizációk......Page 126
Értékadások......Page 127
Sürgősség és elkötelezettség......Page 128
Specifikáció az UPPAAL-ban......Page 129
Példák......Page 130
Irodalomjegyzék......Page 131