Hardver- és szoftverrendszerek verifikációja

Description

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