# 1 Verifikace a zajištění systémů
### IA169
###### tags: `řvss`, `řss`, `verifikace`, `ia169`

<span style="color:red">*Tam, kde sú otázniky, mi to nie je jasné, môžete to pokojne upraviť. Vopred sa ospravedlňujem za chyby a nezrozumiteľnosti, všetko som v rýchlosti ručne prepisoval z anglických slajdov, iné materiály neboli.*</span>

---

## 1. Principy, výhody, nevýhody a omezení metod pro testování systémů bez znalosti kódu a dalších technik pro formální verifikace počítačových systémů jako jsou symbolické exekuce

*Neviem, čo všetko si pod týmto názvom predstaviť. Je tu spracovaná prvá prednáška (Fundamentals of Testing) a druhá prednáška (Symbolic Execution and Concolic Testing)*

---

## 1a. Princípy, výhody, nevýhody, obmedzenia bez znalosti kódu/Fundamental Questions of Testing

Testovanie je empirické, technické skúmanie vedené s cieľom poskytnúť zúčastneným stranám informácie o kvalite testovaného produktu alebo služby.

**Časti: Missions, Strategy, Oracle, Measure Methods, Incompletness**

### Ciele (Missions)

*Prečo testujeme? Čo chceme dosiahnúť?*

**Hlavné**

- hľadanie bugov
- identifikácia faktorov, ktoré znižujú kvalitu produktu

**Vedľajšie**

- Zber dát na podporu manažérskych rozhodnutí
- Je produkt kompletný z hľadiska špecifikácie?
- Sú jednotlivé komponenty logicky a ergonomicky spojené?
- Minimalizovanie dôsledkov nízkej kvality
- Potvrdenie súladu so špecifikáciou
- ...

### Stratégia (Strategy)

*Ako postupovať pre efektívne naplnenie cieľa?*

**Stratégia je plán, ako splniť cieľ v definovanom kontexte.**

V rôznych kontextoch sa naša stratégia pre splnenie zdanlivo rovnakého cieľa môže líšiť.
- pr. tabuľkové výpočty (spreadsheet computation) pre PC hru vs. tabuľkové výpočty pre driver na RTG zariadenie

Výber stratégie ovplyvňuje:
- čo je naším cieľom?
- ako agresívne chceme detekovať bugy?
- ktoré bugy sú dôležitejšie ako ostatné?
- ako dôkladne má byť testovanie zdokumentované?

### Oracle

*Ako zistiť úspešnosť testovania?*

**Oracle (v kontexte testovania) je detekčný mechanizmus alebo princíp, pomocou ktorého zisťujeme, či produkt prešiel alebo neprešiel testom.**

- To, že tester tvrdí, že program prešiel testom, neznamená, že program je správny s ohľadom na testovanú vlastnosť. Záleží od použitého Oracle.
- V zásade môže každý test prejsť/zlyhať s vhodným Oraclom.
- Musíme poznať kontext, odhadnúť metriky, pomocou ktorých zákazník bude posudzovať problém.

**Uľahčenie testovania:**
- vyhýbať sa testom, ktoré neodhalia žiaden problém
- vyhýbať sa testom, ktoré odhalia irelevantné problémy

V prípadoch, keď nedokážeme jasne definovať ciele (*pr. ako presne sa veľkosti musia rovnať, aby sme mohli povedať, že veľkosti sú správne?*) alebo získanie úplných informácií a ich vyhodnocovanie je príliš komplikované a drahé, využijeme **heuristiku** (približné riešenie, založené na odhade, intuícii, skúsenosti, zdravom rozume).

**Heuristika**
- umožňuje zjednodušiť problém s rozhodovaním
- radí, ako postupovať v danom kontexte
- **nezaručuje** správne rozhnodnutie
- by nemala byť založená na žiadnych skrytých vedomostiach
- rôzne heuristiky môžu viesť k protichodným rozhodnutiam
- **nevýhody:**
- môže byť subjektívna
- môže spôsobiť viac problémov ako úžitku

**Konzistencia ako heuristika:** Chceme byť konzistentní s ostatnými funkciami produktu, podobnými produktami, špecifikáciou, štandardmi, očakávaniami zákazníka atď.

**Nedokonalosti pri rozhodovaní**
- *Neúmyselná slepota* - tester neberie do úvahy výstupy, ktorým nevenuje pozornosť alebo mu nie je povedané, že ich ma zahrnúť do výstupov
- *Princíp neistoty* - prítomnosť pozorovateľa môže mať vplyv na to, čo sa pozoruje.
- Z jedného testu **je nemožné** odpozorovať všetky možné výstupy.

**Automatizácia Oraclu**
- eliminuje ľudské chyby
- vedie k opakovateľným postupom
- umožňuje rýchlejšie vyhodnocovanie testov

**Definujeme akýsi súbor očakávaných výstupov (SOV), ktorý sa musí rovnať výstupom testu.**
*pr. MS Word môže byť použitý ako SOV pre testovanie WordPadu.*

Sme schopní automatizovať len **čiastočne**, nikdy neautomatizujeme úplne všetko.

**Problém automatizácie**

- Amount of Agreement (výška dohody)
- musí byť definovaný AoA
- je 99% agreement stále agreement?
- ako definujeme percento agreementu?
- False Alarms (falošný poplach)
- používanie zastaraných očakávaných výstupov
- Neodhalené chyby
- SOV vykazuje rovnakú chybu, ako výstup testu
- neúmyselná slepota

### Metódy merania (Measure Methods)

*Koľko z nášho plánu testovania bolo splneného? Ako ďaleko sme od naplnenia cieľa?*

#### <u>Pokrytie testov ako metrika/Coverage as a Measure</u>

- Pokrytím chápeme časť zdrojového kódu (riadky kódu, podmienky, volania funkcií, vetvenie...), ktorá bola skontrolované aspoň jedným testom.
- Zväčša sa jedná o percento, ktoré vyjadruje, koľko finálneho produktu bolo otestovaného
- jedným z cieľov testovania môže byť dosiahnutie daného percenta pokrytia.
- pre manažérov sa jedná o číselné vyjadrenie koľko produktu ešte zostáva na otestovanie

**Nevýhody**
- môže prehliadnúť niektoré neočakávané vstupy
- Netestuje správne časti produktu, ktoré sa spoliehajú na externé služby.

**Na čo dávať pozor**
- kompletné pokrytie **nezaručuje** kvalitu produktu
- zvykneme uprednostňovať kvantitu pred kvalitou
- zavádzajúce uspokonenie

**Kritéria pokrytia pre control-flow grafy (CFG) (grafy riadenia toku):**

- *Pokrytie statementov/Statement coverage*
- každý statement (zadanie, vstup, výstup, podmienka - to, čo je v grafe vo vnútri geometrických útvarov) je spustený aspoň v jednom teste
- hodnoty premenných nutné na dosiahnutie plného pokrytia (graf hore): (x=2, y=1, z=4, w=3); 1 test

- *Pokrytie hrán/Edge coverage*
- každá hrana grafu (vetva programu) je spustená aspoň raz
- plné pokrytie: (x=2,y=1,z=4,w=3), (x=3,y=3,z=5,w=7); 2 testy

- *Pokrytie podmienok/Condition coverage*
- každá podmienka je boolean kombinácia **elementárnych podmienok** (`x<y`, `even(x)`)
- každá elem. podmienka by mala byť vyhodnotená aspoň v jednom teste ako TRUE a v jednom ako FALSE.
- V priloženom grafe stačia 2 testy (TRUE and TRUE; FALSE and FALSE).

- *Pokrytie hrán/podmienok (Edge/Condition coverage)*
- pokrytie zároveň hrán aj podmienok

- *Pokrytie viacerých podmienok/Multiple condition coverage*
- každá true/false kombinácia musí byť prítomná aspoň v jednom teste
- exponenciálny nárast testov
- 4 testy v priloženom grafe

- *Pokrytie cesty/Path coverage*
- každá spustiteľná cesta/priebeh je vykonaná aspoň v jednom teste (v prípade uvedeného grafu 2 testy)
- počet ciest môže byť nekonečný pri neobmedzenom cykle v CFG

Kritérium A **obsahuje** kritérium B (označené A → B), ak pri plnom pokrytí (full coverage) typu A zaručíme plné pokrytie typu B

- *Cyklické pokrytie/Cycle coverage*
- počet iterácií v cykle
- žiadne pokrytie okrem *path coverage* neodráža počet iterácií v tele cyklu
- Ak je hranica *n* známa pre počet vykonaní cyklu, skúste navrhnúť testy, kde sa cyklus vykoná (*n − 1*), (*n*) a (*n + 1*)-krát.

**Pokrytie pre data-flow grafy (DFG) (grafy toku dát)**
- detekuje nepoužité premenné
- pri niektorých priechodoch/cestách môže byť premenná nastavená na konkrétny účel, no neskôr môže byť jej hodnota zneužitá na iný účel
- pokrýva cesty cez CFG, ktoré prechádzajú miestom, kde sa premenná používa, ale nie je definovaná pozdĺž všetkých prichádzajúcich ciest cez CFG.

**Weibullovo rozdelenie/Weibull Distribution**

- Počet objavených chýb za časovú jednotku.
- Môže sa využiť ako mierka pre zostávajúce množstvo testovania.


- V momente keď krivka dosiahne vrchol, je možné predpovedať zostávajúcu časť krivky, preto je možné nastaviť časový okamih, kedy očakávaný počet chýb objavených za týždeň klesne pod daný threshold (prah).

**Nedokonalosti Weibullovho rozdelenia**
- Testovanie nesleduje obvyklé použitie produktu
- Pravdepodobnosť odhalenia chyby je pri rôznych chybách iná
- Oprava môže spôsobiť ďalšie nové chyby
- Chyby sú od seba závislé
- Počet chýb v produkte sa časom mení
- **závery:**
- Weibullovo rozdelenie nie je veľmi spoľahlivé
- Možno použiť iba pri veľkých projektoch pre veľmi hrubý odhad.

**Zhrnutie**
- Existujú metódy na meranie pokroku vo fáze testovania. Tie sú ale nespoľahlivé.
- Silné zameranie na konkrétnu metódu merania môže ovplyvniť účinnosť testovania.

### Neúplnosť testovania (Incompletness of Testing)

*Uvedomujeme si, že testovanie nemôže dokázať absenciu chyby?*

- Počet testov, ktoré sa majú vykonať, je extrémne veľký.
- Zdroje na testovanie sú vždy obmedzené.

Čo **NIE JE** kompletné testovanie
- Kompletné pokrytie
- Keď testeri nenájdu žiadnu ďalšiu chybu
- Plán testovania je dokončený

Čo **JE** kompletné testovanie
- Produkt neobsahuje žiadne skryté alebo neznáme chyby.

Ak vznikne nový problém, testovanie **nemôže** byť kompletné.

**Príčiny neúplnosti**
- Počet testov je príliš veľký (nekonečný).
- Na vykonanie všetkých testov by sme museli otestovať:
- všetky možné vstupné hodnoty každej vstupnej premennej.
- všetky kombinácie vstupných premenných
- každý jeden beh systému
- všetky kombinácie HW a SW, aj tie z budúcnosti :)
- každú cestu, ako môže užívateľ systém používať
- typická argumentácia: *„Toto by zákazník s našim produktom neurobil.“*

**Zhrnutie**
- Testovanie **nemôže** dokázať absenciu chyby.
- Nie je možné otestovať všetky validné vstupy.
- Existencia plánu testovania brzdí tvorivosť/kreativitu pri testovaní

## 1b. Symbolické prevedenie a Concolic Testing/Symbolic Execution and Concolic Testing

Chceme otestovať program pre všetky možné vstupy. Je ale ťažké odhaliť chyby, ktoré sa systematicky prejavujú iba pri špecifických vstupných hodnotách.

### Testovacie stratégie

**Black-box**
- Vnútorne detaily programu (zdrojový kód) sú neznáme, resp. neberieme ich v úvahu
- analýza správania vstupov a výstupov

**White-box**
- Vnútorné detaily berieme do úvahy, napr. Code Coverage
- Vloženie chyby, zmena produktu za účelom testovania
- V podstate rozšírenie black-box testovania

### Symbolic Execution (SE)
- Spústime program tak, aby sa hodnoty vstupných premenných namiesto skutočných hodnôt označovali symbolmi.


**Vetvenie (Branching):** Vetvenie v kóde zavádza určité obmedzenia dát v závislosti na stave bodu vetvenia

**Podmienka cesty (Path Condition; PC):**
- Vzorec nad symbolmi odkazujúci na vstupné hodnoty.
- Kóduje históriu výpočtu, tj. kumulatívne obmedzenia vyplývajúce zo všetkých prechádzajúcich vetviacich bodov až do aktuálneho bodu provedení (point of execution).
- Na začiatku nastavené na **true**.

**Neuskutočniteľné cesty (Unfeasible Paths)**

- Path condition môže byť neuskutočniteľný (**UNSAT**). V takom prípade neexistujú žiadne vstupy, ktoré by chod danou cestou uskutočnili (viď obrázok)


### Symbolic Execution Tree (SET)

- SET reprezentuje všetky možné prechody programom
- získame ho "rozvinutím" CFG programu
- **Node/uzol** stromu kóduje umiestnenie programu (location), symbolickú reprezentáciu premenných (symbolic valuation) a konkrétny path condition (obrázok)


- hrana v strome zodpovedá symbolickému vykonaniu programovej inštrukcie na danom mieste
- Bod vetvenia (branching point) spôsobuje aktualizáciu path condition pre jednotlivé vetvy

**Ukážka SET**

**Vlastnosti SET**
- Žiadne uzly nie sú zlúčené, aj keď sú rovnaké
- Jedno umiestnenie programu (location) môže byť obsiahnuté v (nekonečne) mnohých uzloch stromu.
- SET môže obsahovať nekonečné cesty.
- *Path Explosion problem*
- Množstvo vetiev v SET môže byť veľmi veľké
- Množstvo ciest môže narástať exponenciálne s počtom navštívených bodov vetvenia

**Vlastnosti programov využívajúcich SET**
- identifikácia ne/realizovateľných ciest
- dôkaz o dosiahnuteľnosti daného umiestnenia programu.
- detekcia chýb (delenie nulou, out-of-array access...)

*Ak vzorec zakódovaný ako PC je vyhovujúci pre symbolický chod, model vzorca vracia konkrétne vstupné hodnoty, vďaka ktorým program bude nasledovať symbolický chod*

**Automatizované generovanie testov**
1. Vygenerujte náhodné vstupné hodnoty
2. Vykonajte s tými hodnotami prechádzku cez SET a zaznamenaj PC
3. Vytvorte novú PC z tej z bodu 2 tak, že zrušte jedno z obmedzení týkajúce sa bodu vetvenia.
4. Nájdite vstupné hodnoty vyhovujúce novej PC
5. Opakujte od bodu 2, kým nedosiahnete požadované pokrytie kódu

**Limity pre SE**
- *Nerozhodnosť*
- Použitie zložitých aritmetických operácií na neobmedzených doménach znamená všeobecnú nerozhodnosť problému spokojnosti so vzorcom (formula satisfaction problem).
- SET je nekonečný (kvôli odvíjaniu cyklov s neviazanám počtom iterácií)
- *Výpočetná zložitosť*
- path explosion problem
- Efektivita algoritmov pre uspokojenie vzorcov (formula satisfiability) na konečných doménach
- *Ďalšie limity*
- Symbolické operácie s nečíselnými premennými.
- Nie je jasné, ako zaobchádzať s dynamickými dátovými štruktúrami.
- Symbolické vyhodnocovanie volaní v externých funkciách

### Nástroje pre SAT riešenia

**Satisfiability problem - SAT (problém uspokojiteľnosti)**
- cieľom rozhodnúť, či existuje hodnota booleovských premenných výrokovej logickej formuly, vďaka ktorej je vzorec pravdivý (true)

**Vlastnosti SAT problemu**
- známy NP-úplný problém, polynomiálny algoritmus pravdepodobne nebude existovať.
- existujú ale riešenia SAT, ktoré sú veľmi účinné a vďaka množstvu heuristík dokážu vyriešiť prekvapivo náročné problémy.

**Satisfiability Modulo Theory - SMT**
- Cieľom rozhodnúť o uspokojivosti logiky prvého rádu s predikátovými a funkčnými symbolmi, které kódujú jednu alebo viacej vybraných teorií, napr.
- Aritmetika celých a desatinných čísel
- Teórie o dátových štruktúrach (zoznamy, polia, bitové vectory...)
- Inštancia SMT je zovšeobecnením boolovskej inštancie SAT, v ktorej sú rôzne množiny premenných nahradené predikátmi z rôznych základných teórií. Vzorce SMT poskytujú oveľa bohatší modelovací jazyk, ako je možné pri booleovských vzorcoch SAT (*wiki*).

**Nástroj: ZZZ/Z3**
- SAT a SMT (Satisfiability Modulo Theory) Solver
- Štandardizované binárne API na použitie v iných overovacích nástrojoch.
- od Microsoft Research
- [https://www.rise4fun.com/Z3](https://www.rise4fun.com/Z3)

**Príklad:**

**Splniteľnosť a platnosť/Satisfiability and Validity**
- Vzorec je splniteľný, iba ak je jeho negácia nesplniteľná.
- SAT Solvers nielen rozhodujú o splniteľnosti vzorcov, za priaznivých okolností nám vrátia aj konkrétne hodnoty premenných, pre ktoré je vzorec splniteľný.
- V prípade, že theorem je neplatný, Solvers nam poskytnú protipríklad (negácia je splniteľná)

### Concolic Testing
= Concrete and Symbolic Testing

**Problém**
V praxi neznáme výsledky často znamenajú nesplniteľnosť (nebol nájdený žiaden svedok). Preskakovanie ciest, o ktorých si iba myslíme, že sú nerealizovateľné, však môže viesť k neodhaleniu chýb. Na druhú stranu, vykonanie (execution) nerealizovateľnej cesty môže hlásiť neskutočné chyby.

**Parciálne riešenie**
1. Použijeme súčasne skutočné aj symbolické hodnoty, aby sme podporili rozhodnutia, ktoré sú prakticky nerozhodnuteľné SAT alebo SMT Solvermi.
- **Conc**rete and Symb**olic** Testing=Concolic Testing
2. Heuristika
3. Vyhodnotenie: UNKNOWN⇒SAT

<u>**Demo**</u>

1. input A,B
2. if (A==(B*B)%30) then
3.     ERROR
4. else
5.     return A

**Concolic testing:**
1. A=22, B=7 (náhodné hodnoty), test spustený, žiadne chyby nenájdené.
2. (22==(7*7)%30) = *false*, path condition (PC):α != (β∗β)%30
3. Syntéza vstupných dát z negácie PC:α= (β∗β)%30 – **UNKNOWN**
4. Zakomponuj konkrétne hodnoty: α= (7∗7)%30 –**SAT**, α=195 A=19, B=7
6. Test objavil chybu v programe na riadku 3.

### SAGE Tool
*len 1 informatívny slide*

**Whitebox Fuzzing**
1. Začnite s dobre formovaným vstupom (nie náhodným)
2. Skombinujte s **generačným** vyhľadávaním/generational search (?) (Nie DFS)
1. Znegujte 1:1 **každé** obmedzenie v obmedzení cesty
2. Vytvorte **veľa** detí pre každý beh rodiča
3. Vyzvite **všetky** vrstvy aplikácie skôr/Challenge all the layers of the application sooner (???)
4. Využite drahý symbolic execution.
- Vyhľadávacie priestory sú **obrovské**, hľadanie je len **čiastočné** ... napriek tomu **efektívne** pri hľadaní chýb!


## 2. Ověřování modelu pro formule LTL a CTL
*prednášky 3-6*

## 2a. Overovanie modelu LTL/LTL Model Checking

### Verifikácia reaktívnych a paralelných programov/Verification of Reactive and Parallel Programs

*Verifikácia==Overovanie

**Paralelné programy**
- Komponenty súčasne prispievajú k zmene stavu výpočtu.
- Význam pochádza z vkládania akcií (transformačných krokov) jednotlivých komponent
- **Významovú funkciu (meaning function) (?) kompozície nie je možné získať zložením významových funkcií zúčastnených zložiek.**
- Výsledok závisí na konkrétnom vkládaní (interleaving)

**Príklad nezlučiteľnosti**

- paralelný systém: `(y=x; y++; x=y)‖(y=x; y++; x=y)`
- I/O premenná $x$
- Významová funkcia oboch procesov: `λx->x+1`
- Kompozícia:`(λx->x+1)·(λx->x+1)`
- `(λx->x+1)·(λx->x+1)0 = 2`


Obecne nevieme odvodiť správnosť systému ze správnosti jeho komponent. Nemôžeme rozložit problém kontroly správnosti systému na dílčí problémy, tj. obmedziť ho iba na overenie správnosti všetkých zúčastnených komponent systému.

**Špecifikácia/Specification**
*Príklad:*
- Eventy A a B nastanú pred eventom C.
- Užívateľ nemôže zadať novú hodontu, pokiaľ systém nespracuje predošlú
- Procedúra X nemôže byť spustená zároveň procesmi P a Q (vzájomné vylúčenie/mutual exclusion)
- Po každej akcii A okamžite následuje sled akcíí B,C a D

### Model Checking
- Prístup k formálnemu overovaniu systémov.
- Založená na prieskume stavu a priestoru systému.

**Prehľad**
1. Zostavte formálny model $M$ overovaného systému.
2. Vyjadrite špecifikáciu ako vzorec (formula) *φ* vybranej temporálnej logiky
- (*Temporálna logika je odvetvie logiky, ktoré skúma logickú štruktúru výrokov o čase s ktorými klasická výroková alebo predikátová logika nedokážu plnohodnotne narábať.*)
3. Rozhodnite, či $M|=φ$, teda či *M* je model vzorca *φ*

- Ako vedľajší účinok rozhodnutia môže vzniknúť **protiklad** (voliteľné)
- Protipríkladom je sled stavov, ktoré sú svedkami porušenia vzorca (v prípade, že je systém chybný).
- **Model checking (proces rozhodovania) môže byť plne automatizovaný pre všetky konečné (a niektoré nekonečné) modely systémov.**


**Model checkers:** Softvérové nástroje, ktoré môžu rozhodnúť o platnosti vzorca nad modelom overovaného systému.
- SPIN, UppAal, SMV, Prism, DIVINE...

**Modelovacie jazyky:**
- procesy popísané ako konečné stavové automaty (finite state machines, FSM)
- Rozšírenie umožňuje používať zdieľané alebo lokálne premenné a strážiť vykonávanie prechodu booleovským výrazom.
- Niektoré prechody môžu byť synchronizované s prechodmi iných FSM/procesov

### Modelovanie a formalizácia overených systémov/Modelling and Formalization of Verified Systems
- Systém je možné chápať ako množinu stavov, ktoré sú prechádzané vykonaním pokynov programu.
- **Stav** = hodnota (alebo ohodnotenie -> valuation) modelovaných premenných.

**Atomic Propositions (AP)**
- Základné výroky popisujíce vlastnosti jednotlivých stavov, napr.: `max(x, y) ≥ 3`
- Platnosť AP pre daný stav musí byť rozhodnuteľná informaciami zakódovanými len stavom.
- Množstvo pozorovateľných udalostí a skutočností závisí od množstva abstrakcie použitej pri modelovaní systému.

### Kripkého štruktúra/Kripke Structure
**Neformálne**
Kripkeho štruktúra je variacia prechodového systému (transition system), ktorá sa používá pri kontrole modelu k reprezentácií správania systému. Skládá se z *grafu*, ktorého uzly predstavujú *dosiahnuteľné stavy* systému a ktorého hrany predstavujú *prechody stavov* (state transitions), spolu s *popisnou funkciou* (labelling function), ktorá mapuje každý uzol na množinu vlastností, ktoré majú odpovedajúci stav. *(wiki)*

- Nech AP je množina atómových prepozícií
- Kripkého štruktúra je štvorica $(S,T,I,s_0)$, kde
- $S$ je konečná množina stavov
- $T⊆S×S$ ke prechodový vzťah (transition relation)
- $I:S→2^{AP}$ je interpretácia AP (labelling function podľa wiki)
- $s_0∈S$ je počiatočný stav

**Kripkeho prechodový systém/Kripke Transition System**
- Nech *Act* je množina inštrukcií spustiteľná programom
- Kripkeho štruktúru je možné rozšíriť pomocou prechodového označenia a vytvoriť Kripkeho prechodový systém
- Kripke Transition System je pätica $(S,T,I,s_0,L)$, kde
- *$(S,T,I,s_0)$* je Kripke structure
- *L: T -> Act* je označovacia funkcia (labelling function)



**Beh systému**
- maximálna cesta (taká, ktorú nemožno predĺžiť) v grafe vyvolaná Kripkeho štruktúrou, začínajúc v počiatočnom stave.
- Nech $M=(S, T, I, s_0)$ je Kripkeho štruktúra. **Beh** je postupnosť stavov $π=s_0,s_1,s_2,...$ takých, že $∀i∈N_0*(s_i, s_{i+1})∈T$.

**Konečné cesty a behy**
- Niektoré konečné cesty $π=s_0,s_1,s_2,...,s_k$ nemôžu byť rozšíriteľné, ak $∄s_{k+1}∈S.(s_k,s_{k+1})∈T$.
- Technicky, vieme premeniť maximálnu konečnú cestu na nekonečnú opakovaním úplne posledného stavu.
- Maximálna cesta $s0,...,s_k$ bude braná ako nekonečný beh $s_0,...,s_k,s_k,s_k,...$

**Implicitný a explicitný popis systému**

Kripke structure, ktorá zachytáva správanie systému, nie je zvyčajne definovaná úplným výčtom stavov a prechodov (explicitne), ale zdrojovým kódom programu (implicitne). Implicitný popis má tendenciu byť exponenciálne stručnejší.

**State-Space Generation (Stavovo-priestorová generácia?)**
- výpočet explicitnej reprezentácie z implicitnej
- interpretácia implicitnej reprezentácie musí byť formálne presná

V praxi programovacie jazyky nemajú presnú formálnu sémantiku. Model checkers často stavia na modelovacích jazykoch

### Formalizácia vlastnosti systému/Formalizing System Properties
*Ako formálne popísať vlastnosti jedného behu?*
*Ako mechanicky overiť ich spokojnosť/uspokojenie (satisfaction)?*

- Využitie konečného automatu ako mechanického pozorovateľa behu
- Behy sú nekonečné
- Konečné automaty pre nekonečné slová (ω-regulárne jazyky/ω-regular languages)
- Podmienka prijatia Büchi - automat akceptuje slovo, ak neustále (nekonečne veľa) prechádza akceptačným stavom.

### Büchi automata/Buchi automat

Büchiho automat je v teorii automatů ω-automat, který rozšiřuje koncept konečného automatu pro nekonečné vstupy (slova nekonečné délky). Büchiho automat akceptuje slovo, pokud existuje běh automatu, který navštíví alespoň jeden koncový stav nekonečněkrát (*wiki*)

- n-tica $A=(Σ,S,s,δ,F)$, kde
- Σ je konečná množina symbolov,
- S je konečná množina stavov,
- $s∈S$ je počiatočný stav,
- $δ:S×Σ→2^S$ je prechodová funkcia (transition relation, na wiki to je transition function),
- $F⊆S$ je množina *koncových/akceptačných stavov*; automat akceptuje slovo, pokud je alespoň jeden z koncových stavů navštíven nekonečněkrát
- *(Barnat=accepting state, EN wiki=acceptance condition, CZ wiki=koncový stav)*

**Jazyk akceptovaný Büchi automatom:**
- Beh ρ automatu A nad nekonečným slovom $w=a_1a_2...$ je sekvencia stavov $ρ=s0,s1,...$ takých, že $s_0≡s$ a $∀i:s_i∈δ(s_{i−1},a_i)$
- $inf(ρ)$– Množina stavov ktoré sa vyskytnú nekonečne mnoho krát v ρ.
- Beh ρ je akceptujúci práve keď $inf(ρ)∩F!=∅$
- Jazyk akceptovaný automatom je množina všetkých slov, pre ktoré existuje akceptujúci beh.
- Označené ako $L(A)$

**Skratky pre Transition Guards (stráž medzi prechodmi)**
1. Nech $AP={X,Y,Z}$
2. Prechod označený ako {X} označuje, že *X* musí byť *true* pri spústení prechodu, zatiaľ čo Y a Z sú false.
3. Ak chceme vyjadriť, že X je true, Z je false, a pre Y nám to je jedno, musíme vytvoriť dva prechody označené ako {X} a {X, Y}.

**APs ako boolean vzorce**
- Prechody medzi dvoma rovnakými stavmi možno kombinovať a označiť boolovským vzorcom nad APs.
- Prechody {X}, {Y}, {X, Y}, {X, Z}, {Y, Z} a {X, Y, Z} je možné spojiť do jedného, označeného $X ∨ Y$. (*neviem, prečo tu nie je Z, možno chyba v materiáloch, môžete upraviť, ak tomu rozumiete*)
- Ak neexistujú žiadne obmedzenia pri uskutočňovaní prechodu, môže byť označený ako $true≡X∨¬X$.

### Linear Temporal Logic (LTL)/Lineárna časová logika

**Neformálne**
- **Vzorec/Formula φ**
- sa vyhodnotí na základe jedného behu Kripkeho štruktúry
- vyjadruje platnosť APs v stavoch pozdĺž daného behu

**Temporal operators of LTL:**
- Fφ— φ eventuálne bude platiť (Budúcnosť/(F)uture).
- Gφ— φ platí stále (Globálne/(G)lobally).
- φUψ— φ platí, kým eventuálne ψ nebude platiť (Kým/(U)ntil).
- Xφ— φ platí po vykonaní jedného prechodu, teda v ďalšom prechode (Ne(X)t/Ďalší).
- φRψ— ψ platí, kým $φ∧ψ$ neplatí (( R )elease/Prepustenie).
- φWψ— ako Until, ale ψ nikdy nemusí začať platiť ((W)eak Until).


**Syntax LTL**
Nech $AP$ je množina atomic propositions
- Ak $p∈AP$, potom p je vzorec LTL.
- Ak φ je vzorec LTL, potom $¬φ$ je vzorec LTL.
- Ak φ a ψ sú vzorce LTL, potom $φ∨ψ$ je vzorec LTL.
- Ak φ je vzorec LTL, potom $Xφ$ je vzorec LTL.
- Ak φ a ψ sú vzorce LTL, potom $φUφ$ je vzorec LTL.

Alternatívne:

$φ::=p|¬φ|φ∨φ|Xφ|φUφ$

**Syntaktické skratky:**

**Modely LTL vzorcov**
- Nech $AP$ je množina atomic propositions
- Model LTL vzorca je beh $π$ Kripkeho štruktúry
- Nech $π=s_0,s_1,s_2,...$
- Prípona behu $π$ začínajúca na $s_k$ sa označuje ako $π^k=s_k,s_{k+1},s_{k+2},...$
- K-tý stav behu sa označuje ako $π(k) =s_k$.

**Sémantika LTL**

Predpoklady:
- Nech $AP$ je množina atomic propositions
- Nech $π$ je beh Kripkeho štruktúry $M=(S,T,I,s0)$
- Nech $φ,ψ$ je syntakticky správna LTL formula
- Nech $p ∈AP$ označuje atomic proposition


**LTL Model Checking**
- systém sa berie ako množina behov
- Systém spĺňa vzorec LTL tehdy a jen tehdy, pokiaľ všetky behy systému spĺňajú formulu.
- Inými slovami, akýkoľvek beh porušující formulu je svedkom toho, že systém vzorec nespĺňa.

**Lemma**:
- Pokiaľ konečný stavový systém (finite state system) nespĺňa LTL vzorec, môže to byť svedkom **lasso-shaped** behu.
- Všimnime si, že $π^ω$ označuje nekonečné opakovanie $π$

### Prístup založený na automatoch na LTL model checking
*Snáď túto časť môžeme skipnúť, je celkom hard... Pár slajdov je dokonca šedo zafarbených, neviem, či to Barnát sám nepreskakoval.*

### Detekcia akceptačných cyklov/Detection of Accepting Cycles
Akýkoľvek automat môže nekonečne mnohokrát navštíviť akceptačný stav, iba ak obsahuje cyklus cez ten akceptačný stav.

<span style="color:red"> **Akceptačný cyklus/Accepting cycle =??**</span>
*môžete doplniť podľa vášho uváženia, ja to neviem popísať, v slajdoch nie je priama definícia*

- Detekovať akceptačný cyklus dokážeme s pomocou **Nested DFS** algoritmu pri zložitosti $O(|V| + |E|)$

*Zvyšok časti viacmenej grafové algoritmy, skipujem*

### Klasifikácia Büchi automatov

*Konečný stav == Akceptačný stav asi?*

**Konečné Büchi automaty/Terminal Büchi Automata**
- Všetky akceptačné cykly sú vlastné smyčky (self-loops) na akceptačných stavoch označených ako true.

**Slabé Büchi automaty/Weak Büchi Automata**
- Každá silne spojená komponenta automatu sa skladá buď z akceptačných alebo neakceptačných stavov

**Automat $A¬φ$**
- pre radu LTL formulí φ je $A¬φ$ konečný alebo slabý
- $A¬φ$ je typicky celkom malý
- Typ $A¬φ$ môže byť vyrátaný pred verifikáciou
- Typy komponent automatu $A¬φ$:
- **Neakceptačný (Non-accepting)** - Neobsahuje žiadne akceptačné cykly
- **Silno akceptačný (strongly accepting)** - každý cyklus je akceptačný

**<u>$A¬φ$ je konečný Buchi automat (BA)</u>**
- Pre dôkaz existencie akceptačného cyklu stačí dokázať dosiahnuteľnosť ktoréhokoľvek akceptačného stavu v $A¬φ$
- Proces overovania je redukovaný na problém dosiahnuteľnosti.

**“Bezpečnostné” vlastnosti/"Safety" properties**
- Tie vlastnosti LTL formule φ, pre ktoré $A¬φ$ je konečným BA
- Dosiahnuteľnosť je dostačujúca na dokázanie vlastnosti (proof the property)

**<u>$A¬φ$ je slabý Buchi automat (BA)</u>**
- Neobsahuje žiadne čiastnočné akceptačné komponenty
- Pre dôkaz existencie akceptačného cyklu stačí dokázať existenciu dosiahnuteľného cyklu v silne akceptačnej komponente.
- Dokáže byť detekovaná jedinou DFS procedúrou
- Existuje časovo optimálny algoritmus, ktorý sa ale nespolieha na DFS.

**"Slabé" LTL vlastnosti/"Weak" LTL properties**
- Tie vlastnosti LTL formule φ, pre ktoré $A¬φ$ je slabým BA
- Typicky, responzivita: $G (a⇒F (b))$ *(?)*

**Klasifikácia LTL vlastností**

Každá LTL formula spadá do jednu z týchto tried:
- Reactivity (reaktivita)
- Recurrence (opakovanie)
- Persistance (stálosť)
- Obligation (povinnosť/záväzok)
- Safety (bezpečnosť)
- Guarantee (záruka)

Vlastnosti *Guarantee* triedy môžu byť popísané konečným Buchi automatom.

Vlastností tried *persistance, obligation, safety* môžu byť popísanú slabým Buchi automatom

**Negácia vo verifikačnom procese ($φ→A¬φ)$)**
- $φ∈Safety⇐⇒¬φ∈Guarantee$
- $φ∈Recurrence⇐⇒ ¬φ∈Persistance$


### Vysporiadavanie sa s "výbuchom" stavového priestoru/Fighting State Space Explosion

*Boj proti štátnej vesmírnej explózii :space_invader:*

**State Space Explosion (SSE):**
Systém je bežne zložený kompozíciou paralelných procesov. V závislosti od poradia vykonávania akcií paralelných procesov vznikajú rôzne prechodné stavy. Počet dosiahnuteľných stavov môže byť **exponenciálne** väčší ako počet riadkov kódu.

**Následky**:
- Hlavná pamäť nedokáže uložiť všetky stavy automatu produktu, lebo ich je príliš veľa
- Algoritmy pre detekciu akceptačných cyklov trpia nedostatkom pamäti

**Metódy vysporiadavania sa so SSE**
- *Stavová kompresia/State compression* - lossless/lossy (bezstrátová či stratová)
- *Overovanie za behu*
- *Symbolická reprezentácia stavového priestoru*
- *Znížený počet stavov produktového automatu*
- zavedenie atomických blokov
- čiastočné poradie vykonávania akcií procesu
- vyhýbanie sa skúmaniu symetrických častí
- *paralelná a distruibuovaná verifikácia*

<u>**Partial Order Reduction**</u>
Predstavme si systém pozostávajúci z procesov A a B. A je schopný vykonávať akciu α, zatiaľ čo B je sekvencia akcií β, napr. $β_1,...,β_m$

**Unreduced State Space**

Vlastnosť, ktorú chceme verifikovať: **Dosiahnuteľnosť stavu $r$**

Behy $(αβ_1β_2...β_m),
(β_1αβ_2...β_m), ... ,(β_1β_2...β_mα)$ sú totožné s ohľadom na skúmanú vlastnosť *r*. Stačí nam teda brať do úvahy zástupcu z tejto triedy ekvivalencie, napr. $(β_1β_2...β_mα)$

Zástupcu získame odkladom akcie α.

Nevyberajte všetkých bezprostredných nástupcov počas skúmania stavového priestoru (state-space exploration), ale vyberajte opatrne iba niektorých z nich. Vybrať správnu a optimálnu podmnožinu nástupcov je rovnako ťažké ako vygenerovať celý stavový priestor. Preto sa používa heuristika.
- Zmenšený stavový priestor musí obsahovať akceptujúci cyklus a iba vtedy, ak to robí neredukovaný stavový priestor.
- Vzorec LTL nesmie používať operátor *X* (podtrieda LTL).

**Distributed and Parallel Verification/ Distribuovaná a paralelná verifikácia**

*Princíp:* Využitie agregovaného výkonu viacerých CPU, zvýšená pamäť a výpočetný výkon PC

Typická implementácia Nested DFS algoritmu sa spolieha na hashovací mechanizmus, preto sa k hlavnej pamäti pristupuje veľmi náhodne. Ak nároky na pamäť presiahnu množstvo dostupnej pamäte, nastane **[thrashing](https://cs.wikipedia.org/wiki/Memory_thrashing)**.

Preto namiesto DFS sa používajú iné grafové postupy:
- Bread-first search alebo value propagation (šírenie hodnôt?) je možné efektívne vypočítať paralelne.

### Zhrnutie - Overovanie Modelu

**Validita vlastností/Properties validity**
- Vlastnosť, ktorá sa má overiť, môže byť porušená jedným konkrétnym (aj keby mimoriadne nepravdepodobným) behom systému, ktorý je predmetom kontroly.
- Postup rozhodovania sa opiera o skúmanie stavového grafu (exploration of state space graph) systému.

**State Space Explosion**
- Ak k tomu nie sú dôvody,všetky systémové behy musia byť brané v úvahu
- počet stavov, ktoré môže systém dosiahnuť, je exponenciálne väčší, ako veľkosť popisu systému
- Dôvody: Data explosion, asynchronný paralelizmus

**Výhody Model Checkingu**
- aplikovateľné na HW, SW, Embedded systémy, Model-based development...
- *matematická presnosť* - Výsledkom rozhodovacieho postupu je $M |= φ$, len a len v takom prípade
- *Model checkery* - pri rozhodovaní nevyžaduje prítomnosť človeka, poskytuje svedkov a protipríklady

**Nevýhody Model checkingu**
- *nie vhodné na všetko*- napr. či program na výpočet faktoriálu skutočne vyráta n! pre dané n
- je ale úplne OK skontrolovať, či pre hodnotu 5 vždy vratí hodnotu 120
- *spolieha sa na konštrukciu modelu* - validita formule je garantovaná pre model, nie vymodelovaný systém (?)
- *veľkosť stavového priestoru*- kvôli SSE, praktická aplikovateľnosť je limitovaná.
- Aplikovateľné najmä na konečné statové priestory (finite state space)
- *verifikuje len to, čo bolo špecifikované* - problemy nezahrnutú vo vzorcoch nemusia byť objavené

## 2b. Overovanie modelu CTL/CTL Model Checking

**Systém ako množina behov**
- **Run/Beh** - množina stavových sekvencií.
- vlastnosti systému = vlastnosti behu
- popísateľný s **Linear-time logic/LTL**

**Systém ako rozvetvená štruktúra**
- *Computation Tree/Výpočtový strom* - rozvetvené štruktúra možných spustení z jednotlivých stavov systému
- vlastnosti systému = vlastností stromu
- popísateľný s branching-time logic/**Computation tree logic/CTL**


### Computation Tree Logic (CTL)

**Neforemne:** Pre daný uzol výpočtového stromu popisuje podstrom zakorenený v danom uzle všetky možné behy, ktoré systém ešte môže vykonať. Každý takýto beh je možným budúcim výpočtom.

**CTL formuly umožňujú**
- Špecifikáciu stavových kvalít s atómovými propozíciami.
- Kvantifikáciu možných budúcich výpočtov
- Obmedziť množinu možných budúcich výpočtov (kvantifikovanými) LTL operátormi

*Príklad:* $φ≡EF(a)$
- =Je možné vykonať budúci výpočet tak, aby $a$ nakoniec vo výpočte platilo
(*It is possible to take a future computation such that 'a' will hold true in the computation eventually*)

**Syntax CTL**
A = along (A)ll paths (inevitable) = **platí vždy**
E = along at least (there (E)xists) one path (possibly) = **platí aspoň raz**

*pre zvyšnú notáciu, pozri LTL vyššie*

Nech AP je množina atomic propositions:
- Ak $p∈AP$, potom $p$ je CTL formula
- Ak $φ$ je CTL formula, potom $¬φ$ je CTL formula
- Ak $φ$ a $ψ$ sú CTL formuly, potom $φ∨ψ$ je CTL formula
- Ak $φ$ je CTL formula, potom $EXφ$ je CTL formula
- Ak $φ$ a $ψ$ sú CTL formuly, potom $E[φUψ]$ je CTL formula
- Ak $φ$ a $ψ$ sú CTL formuly, potom $A[φUψ]$ je CTL formula

**Alternatívne:
$φ::=p|¬φ|φ∨φ|EXφ|E[φUφ]|A[φUφ]$**


**Modely CTL formuly**
- Nech AP je množina atomic propositions
- Model CTL formuly je stav s∈S Kripkeho štruktúry $M=(S,T,I,s0)$
- *pripomenutie:*
- Beh Kripkeho štruktúry je maximálna cesta začínajúca od počiatočného stavu štruktúry
- Konečné maximálne dráhy sa považujú za nekonečné behy z dôvodu nekonečného opakovania posledného stavu na ceste
- $P_M(s)$ = ($π|π$ je beh iniciovaný v stave $s$)

**Sémantika CTL**
- Nech AP je množina atomic propositions
- Nech $p∈AP$ je atomic proposition
- Nech $s∈S$ je stav kripkeho štruktúry $M= (S,T,I,s_0)$
- Nech $φ,ψ$ označujú syntakticky korektné CTL formuly


### Model Checking CTL/Overovanie Modelu CTL
Ak je platnosť vzorcov/formuly $φ$ a $ψ$ známa pre všetky stavy, je možné z nich ľahko odvodiť platnosť vzorcov $¬φ,φ∨ψ,EXφ,...$

**CTL Model Checking - Sketch**
- Nech $M=(S,T,I)$ je Kripke structure a φ CTL formula
- Označovacia funkcia (labelling function) **label: $S → 2^{2φ}$** sa počíta tak, že dáva platnosť všetkých podvzorcov φ pre všetky stavy Kripkeho štruktúry M.
- **$s_0|=φ⇐⇒φ ∈ label(s_0)$**
- Funkcia **label** sa počíta postupne pre jednotlivé podformule φ, počnúc najjednoduchšou podformulou, pokračujúc k zložitejším podformulám, končiac samotným φ.

**Sub-formuly vzorca φ**
- φ je CTL formula
- Množina všetkých podformulí/subformulí vzorca φ označujeme ako $2^φ$
- $2^φ$ je definované indukčne podľa štruktúry vzorca φ, viď obrázok:

**Ekvivalentné existenčné formy CTL**
- Je jednoduchšie dokázať platnosť existenčne kvantifikovaných [modálnych operátorov](https://en.wikipedia.org/wiki/Modal_operator) ako platnosť univerzálne kvantifikovaných
- Na účely overenia vlastností špecifikovaných CTL, je možné vyjadriť vzorec CTL v ekvivalentne expresívnej existenciálnej podobe CTL.

**Ekvivalentná CTL Syntax**
**$φ::=p|¬φ|φ∨φ|EXφ|E[φUφ]|EGφ$**

**Komplexita algoritmu pre CTL Model Checking**

- Algoritmus CTLMC vykazuje **$O(|φ||S|)$** priestorovú a **$O(|φ|(|S|+|T|))$** časovú komplexitu.

### CTL Príklad - mikrovlnná rúra
<br/>
**Transformácia a validita**

### CTL*
- rozšírenie CTL

Každé použitie temporálneho/časového operátora vo vzorci CTL musí bezprostredne predchádzať kvantifikátor, t.j. použitie modálneho operátora bez kvantifikácie nie je možné.

**Logika CTL***
Ako pri CTL, využíva rozvetvenú časovú logika (branching time logic). Narozdiel od CTL ale povoľuje samostatné využívanie modálnych operátorov

**Príklad**
$A[p∧X(¬p)]$ - je CTL*, nie je CTL

**Syntax CTL***
- Kvantifikátory E a A sú samostatnými operátormi v pravidlách konštrukcie syntaxe. Výsledkom sú dva typy vzorcov v CTL*: **path/cestné** a **state/stavové** formuly.
- Aplikácia operátorov E a A na path formulu (vzorec, ktorého model je *behom* Kripkeho štruktúry) má za následok state formulu (vzorec, ktorého model je *stavom* Kripkeovej štruktúry)

**state formula**: $φ::=p|¬φ|φ∨φ|Eψ$
**path formula**: $ψ::=φ|¬ψ|ψ∨ψ|Xψ|ψUψ$

**Sémantika CTL***
- Nech AP je set atomic propositions a p∈AP
- Nech M=(S,T,I) je Kripke structure
- Nech $φ_i$ označuje CTL* state formulu, a $ψ_i$ path formulu


### Porovnanie výpovednej sily (expressive power) LTL, CTL a CTL*
- každá LTL formula je CTL* path formula
- každá CTL formula je CTL* state formula
- Model path formule je beh Kripkeho štruktúry
- Model state formule je stav Kripkeho štruktúry
- = Nie veľmi vhodné na porovnávanie

**Dôsledky**
*Dôkazy vynecháme...*

- LTL a CTL sú neporovnateľné čo sa týka výpovednej sily
- AG(EF(q)) je CTL formula nevyjadriteľná v LTL
- FG(q) je LTL formula nevyjadriteľná v CTL
- CTL* je striktne viac výpovedný ako LTL
- každá LTL formula je CTL* formula
- CTL* formula AG(EFq) sa nedá v LTL vyjadriť
- CTL* je striktne viac výpovedný ako CTL
- každá CTL formula je CTL* formula
- CTL* formula FG(q) sa nedá v CTL vyjadriť (*pred chvíľou to bola LTL formula, teraz CTL\*, neviem, či chyba alebo nie*)
- Existujú vlastnosti vyjadriteľné v LTL aj v CTL
- CTL formula A[p U q] je rovná LTL formule *p U q*

### Ordered Binary Decision Diagrams/OBDD
- Verifikačné algoritmy ukládajú množiny stavov
- Množina stavov môže byť videná ako množina binárnych vektorov
- Množina binárnych vektorov môže byť popísaná ako **Boolean funkcia** - formula vo výrokovej logike nad danou množinou boolean premenných

**Binary Decision Tree/Binárny rozhodovací strom (BDT)**
- Nasmerovaný strom s jedným koreňovým stavom
- Každý vnútorný uzol je označený booleovskou premennou (v) a má presne dvoch nástupcob označovaných ako (low (v), high (v)).
- Každému listu je priradená binárna hodnota, tj. 0 alebo 1.
- Každá kombinácia hodnôt vstupných premenných zodpovedá presne jednej ceste od koreňa BDT po list.
- Hodnoty uložené na listoch vracajú hodnotu funkcie pre príslušné vstupné hodnoty


**Binary Decision Diagram/binárny rozhodovaná diagram (BDD)**
- BDT sú zbytočne náročné na priestor (obsahujú nadbytočné informácie).
- Acyklický smerovaný graf, ktorého vrcholy majú výstupný stupeň buď nula (list) alebo dva (vnútorný vrchol).
- Inak rovnaké vlastnosti, ako BDT


**Ordered Binary Decision Diagram/ Usporiadaný BDD (OBDD)**
- Niektoré prechodné znázornenia vypočítané počas minimalizácie BDD sú tiež platné BDD.
- Daná boolovská funkcia môže byť reprezentovaná viacerými rôznymi BDD
- Minimálny BDD vypočítaný z BDD alebo BDT s pevným poradím premenných vo vnútorných vrcholoch **je unikátny**.
- BDD s fixným usporiadaním premenných sa označuje ako **ordered/usporiadaný BDD** (OBDD)


Každý OBDD reprezentuje nejakú boolean funkciu. Boolean funkcie môžu byť komnibované/kompozované s použitím unárnych a binárnych operátorov, ako $¬,∧,∨,⇒,XOR,...$. OBDD môže byť zložený rovnako.

### Symbolický prístup ku CTL Model Checkingu
**Algorithm Idea**
- Nech M=(S,T,I) je Kripke structure a φ je CTL formula
- Labelling funkcia $label:S→2φ$ sa vyráta, hovoriac ktoré subformule z φ sú validné v ktorých stavoch *M*
- samozrejme, $s0|=φ⇐⇒φ∈label(s0)$
- Funkcia **label** sa počíta postupne pre každú subformulu φ, počínajúc nejjednoduššími subformulami (atomic propositions/atomové výroky) a končiac po výpočtu validity φ

**Realizácia**
1. Sada stavov reprezentovaných s OBDDs
2. Boolean funkcie na vyhodnotenie atomic propositions formujú počiatočné OBDDs
3. Podľa štruktúry overenej formule sa vyrátajú OBDDs pre zložitejšie podformule
4. Testovanie členstva počiatočného stavu Kripkeovej štruktúry v množine stavov vyhovujúcich overenej formule

**Pripomenutie Syntaxe CTL**
$φ::=p|¬φ|φ∨φ|EXφ|E[φUφ]|EGφ$

**Výpočet množiny stavov splňujúcich (satysfying) CTL formulu**
*Notácia:*
- F(ψ)označuje množinu stavov splňujúcich ψ
- *Succ(X)* označuje bezprostredných nástupcov stavov v množine *X*
- *Pred(X)* označuje bezprostredných predchodcov stavov v množine *X*

*Boolean funkcie pre atomic propositions:*
- atomic propositions popisujú vlastnosti stavu premenných
- at. prop. môžu byť zakódované ako boolean funkcie

*Výpočet boolean operátorov $¬$ a $∨$*
- $F(¬ψ1) =¬(Fψ1)$
- $F(φ∨ψ) =F(φ)∨F(ψ)$

### Model Checking - Zhrnutie

**Enumeratívny vs. symbolický prístup**
*Enumeratívny* - zameraný na "control-flow" (*poradie operácií atď.*)
*Symbolický* - zameraný na "data-flow" (*kde sú data smerované, ake transformácie sú prevedené atď.*)

**Výhody v súvislosti s testovaním**
- nevyžaduje zdrojový kód (môžeme aplikovať na modely)
- vhodné na testovanie paralelných programov

**Výhody v súvislosti so statickou analýzou**
- Kompletné pre systémy s konečným stavovým priestorom.
- Verifikácia temporálnych/časových vlastností

**Nevýhody**
- State space explosion

## 3. Ohraničené overovanie modelu/Bounded Model Checking (BMC)
*prednáška 8*

### Kontrola bezpečnostných vlastností cez SAT redukciu

**Safety property/bezpečnostná vlastnosť:** Bezpečnostná vlastnosť tvrdí že nič zle počas exekúcie nenastane (A safety property asserts that nothing bad happens during execution)*(oreilly)*

**Bounded Model Checking**

**Hypotéza:** Ak systém obsahuje chybu, je možné ju reprodukovať iba s malým počtom kontrolovaných krokov

**Myšlienka metódy:** Keď používame model checking pre detekciu chyby, je rozumné skontrolovať či chyba (porušenie [violation] špecifikácie) nastane v prvých *k* krokoch spustenia

**Redukcia BMC na SAT**

*Prerekvizity:*
- Množina prefixov dĺžky *k* všetkých behov Kripkeho štruktúre *M* môže byč zakódovaná Boolean formulou $[M]^k$
- Porušenie bezpečnostnej vlastnoti (safety property), ktoré môže byť pozorované do *k* krokoch systému, môže byť zakódované ako $[¬φ]^k$

*Redukcia:*
- Skontrolujeme uspokojivosť $[M]^k∧[¬φ]^k$
- uspokojivosť indikuje existenciu protipríkladu dĺžky *k*
- neuspokojivosť indikuje neexistenciu protipríkladu dĺžky *k*

**Kripke Structure ako Boolean formula**

*Prerekvizity:*
- M=(S,T,I) je Kripke structure s počiatočným stavom $s_0∈S$
- ľubovoľný stav s∈S môže byť reprezentovaný bitovým vektorom dĺžky *n*, teda stav $s=〈a_0,a_1,...,a_{n−1}$

*Zakódovanie M Boolean formulou*
- *Init(s)* - formula ktorá je uspokojivá pre ohodnotenie (valuation) premenných $a_1,a_2,...,a_n$, ktoré popisujú stav $s_0$
- *Trans(s,s')* - formula ktorá je uspokojivá pre dvojicu stavových vektorov s,s' iff (vtedy a len vtedy) ohodnotenia $a_1,a_2,...,a_n,a′_1,a′_2,...,a′_n$ popisujú stavy medzi ktorými prechod (transition) $(s,s') ∈ T$ existuje.

**Zakódovanie konečných behov M**

*Popis systémových behov dĺžky $k$*
- beh dĺžky *k* pozostáva z *k+1* stavov $s_0,s_1,...,s_k$
- množina všetkých behov dĺžky *k* štruktúry *M* je označená ako **$[M]^k$** a popísaná následovným vzorcom:


*Príklad:*

### Úplnosť BMC/Completeness of BMC

<span style="color:red">*V tejto sekcii sa dosť hovorí o grafe. Neviem, o aký graf sa jedná, v slajdoch k tomu nič nie je. Môžete doplniť, ak tomu rozumiete.*
*(A možno rovno skipnúť pri tom množstve matematickej notácie)*</span>

**Graph diameter/priemer grafu (d)** je dĺžka najdlhšej z najkratších ciest medzi každou dvojicou vrcholov v grafe.

**Úplnosť BMC na zisťovanie porušení bezpečnosti**

Porušenie nie je možné dosiahnuť pomocou cesty dĺžky *k*. Cesty kratšie ako *k* nie sú zakódované v $[M]^k$

*Horná hranica na k*
- Ak $k≥d$, kde *d* je priemer grafu (**???**), všetky možné miesta chýb (error location) sú objavené
- Priemer grafu (**???**) je ohraničený hodnotou $2^n$, kde *n* je počet bitov stavového vektoru

*Riešenie*: **Iteratívna exekúcia BMC pre každé $k∈[0,d]$**

**Automatická detekcia priemeru grafu**
- Pýtať sa užívateľa je nereálne
- Bezpečné horné ohraničenie je mimoriadne nadhodnotené
- Chceli by sme, aby verifikačná procedúra sama vedela zistiť, či by *k* malo byť ešte navýšené alebo nie

**Kostra algoritmu pre úplný BMC:**

**Ukončenie BMC - acyklické cesty**

*Notácia cesty:*

*Notácia cesty bez cyklu (acyklickej):*

*Podmienka ukončenia v kostre algoritmu BMC*
- Žiadna ďalšia acyklická cesta z počiatočného stavu už neexistuje, nasledujúca formula je neuspokojivá:

$Init(s_0)∧loopFree(s_{[0..i+1]})$

- **Platí symetricky pre spätnú dosiahnuteľnosť z chybových stavov.**


*Kritérium ukončenia s vyššou účinnosťou*
- Pri aplikácií spätnej dosiahnuteľnosti zo stavov $¬φ$ nemusia byť brané v úvahu cesty, ktoré navštevujú iné stavy $¬φ$.
- Symetricky platí aj pre doprednú dosiahnuteľnosť s viacerými počiatočnými stavmi: pre detekciu úplnosti nie je potrebné brať do úvahy cesty, ktoré navštívia iné počiatočné stavy.


**BMC nezačínajúce s k=0**
- Pre malé hodnoty *k*, SAT dotazy nevrátia ani protipríklad, ani neumožnia ukončenie.
- BMC chceme začať s k>0.

*Originálny test na existenciu protipríkladu:*

$SAT(Init(s_0)∧path(s_{[0..k]})∧ ¬φ(s_k))$

musíme zmeniť, aby sme nevynechali protipríklady kratšie ako počiatočnú hodnotu *k*

*Nový test na existenciu protipríkladu:*

$SAT(Init(s_0)∧path(s_{[0..k]})∧ all.φ(s_k))$

**Acyklické vs najkratšie cesty v BMC**
Acyklická cesta môže byť oveľa dlhšia, ako priemer grafu.


- BMC je korektné, ak *loopFree* nahradíme *shortest*
- Predikát *shortest* ale potrebuje kvantifikátory a nie je až taká čistá SAT aplikácia

### LTL a BMC

LTL je dobre definovaný iba pre nekonečné behy. Na hodnotenie LTL na konečných cestách používame logiku s tromi hodnotami (true, false, cannot say). O platnosti niektorých vzorcov LTL nemožno rozhodnúť na nijakej konečnej ceste (napr. *GF a*).

Cykly, ktoré pozostávajú iba z niekoľkých stavov, BMC rozvinú na acyklické dráhy dĺžky *k*. Povolíme kódovanie laso-shaped ciest. To je, **(k,l)-cyklické cesty.**

**(k,l)-cyklické behy**

- Ak π je k-l cyklický, π je taktiež (k+1, l+1) cyklický
- Považovanie konečných ciest za (k, k)-cyklické je nesprávne (mohlo by to vytvoriť neexistujúci chod v N).
- Každá cesta dĺžky *k* je buď acyklická alebo (k,l)-cyklická

**BMC pre LTL**
- Zostrojíme boolovský vzorec [M, φ, k], ktorý je uspokojivý, ak má Kripkeova štruktúra M chod π taký, že π |= kφ.
- $[M,φ,k]≡[M]^k∧[φ,k]$

*Kódovanie*


**LTL triky v BMC**

*Fragment **LTL-X***
- Znižuje počet prechodov (menšia inštancia SAT).
- podobný partial order reduction

### Závery o BMC

**Výhody BMC**
- Redukuje na štandardný SAT problém, pokroky v SAT solving pomáhajú s BMC.
- Často nachádza protipríklady minimálnej dĺžky (nie vždy).
- Booleovské vzorce môžu byť kompaktnejšie ako reprezentácia OBDD

*Verifikácia HW*
- Vďaka k-indukcii veľmi úspešná metóda.

*Verifikácia SW*
- V současné době je podle Software Verification Competition(TACAS 2014), BMC v souvislosti s SMT je v současné době mezi nejlepšími metodami ověřování softwaru (ve skutečnosti padělání).

**Nevýhody BMC**
- Obecne není úplné (not complete)
- Veľké inštancie SAT sú stále neriešiteľné.

*Verifikácia SW*
- Kódovanie celého CFG (control-flow graph) ako inštancie SAT je v súčasnosti nereálne
- K-indukcia nemôže byť použitá (graf je nekompletný, žiadné zadné hrany [back edges] grafu)
- Problémy s analýzou dynamických dátových štruktúr
- Analýza slučky (loop analysis) je náročná
- Neefektívne pre úplnú aritmetiku (čiastočne vyriešené SMT).

## 4.Abstrakcia prechodových systémov/Abstract Interpretation
*prednáška 11*

**Analýza programu**
- Odvodiť vlastnosti programu zo zdrojového kódu a...
- využiť ich na programovú optimalizáciu (program optimization)
- využiť ich na **programovú verifikáciu** (program verification)

*Nerozhodnuteľnosť*
- Platnosť všetkých zaujímavých vlastností programu napísaných vo všeobecnom programovacom jazyku je algoritmicky nerozhodnuteľná.

**Abstrakcia:** Skrytie podrobností s cieľom zjednodušiť analýzu. Zameriava sa na správne, aj keď neúplné riešenie.

*Použitie:*
- Vytvoriť (zvyčajne konečný stavový) model overovaného systému. (Nasledovaný napr. Model checkingom)
- Spustenie systému v kontexte abstrakcie - **abstraktná interpretácia.**

*Ďalšie prístupy:*
- testovanie - fixkná vstupná množina hodnôt
- BMC - obmedzený prieskum celého stavového priestoru
- Symbolic Execution - praktická nerozhodnuteľnosť (practical undecidability)

### Datova a predikátová abstrakcia /Data and Predicate Abstraction

**Data Abstraction**
*Abstraction:* mapovanie konkrétnych stavov na abstraktné
*Konkretizácia:* mapovanie abstraktných stavov na konkrétne

**Abstract Transition System(ATS)/Abstraktný prechodový systém**

*Prechody*
- príkaz v programovom kóde: `A := A + A`
- Konkrétna sémantika:
- `<PC:12, A:15, B:0> -> <PC:13, A:30, B:0>`
- Abstraktná sémantika:
- `<PC:12, A:Odd, B:Even> -> <PC:13, A:Even, B:Even>`

*Nedeterminizmus v ATS*
- Abstraktný stav: `<PC:13, A:Even, B:Even>`
- kod: `A:=A div 2`

**Vzťah mezi abstraktnými a konkrétnymi prechodovými systémami**
*approximation/aproximácia:* a value or quantity that is nearly but not exactly correct.
*over-approximation:* An approximation that is higher than the true value.
*under-approximation:* An approximation that is lower than the true value.

*Over-approximation*
- Každý beh konkrétneho systému je prítomný v konkretizácii nejakého abstraktného behu (beh abstrahovaného prechodového systému)
- Môžu existovať behy, ktoré sú obsiahnuté v konkretizácii nejakého abstraktného behu, ale nie sú povolené v konkrétnom prechodovom systéme

*Under-approximation*
- Každý beh prítomný v konkretizácii ľubovoľného abstraktného behu je existujúci beh konkrétneho prechodového systému.
- Môžu existovať behy konkrétnych prechodových systémov, ktoré nie sú prítomné pri konkretizácii abstraktného behu

**Verifikácia aproximovaných prechodových systémov**

*Verifikácia over-approx. systémov*
- Absencia chyby v ATS dokazuje absenciu chyby v CTS (concrete transition system/konkrétny prechodový systém)
- Chyba v ATS môže, ale nemusí indikovať chybu v CTS
- Chyba v ATS, ktoré nie je chybou v CTS, sa označuje ako *false positive* (spurious error, false alarm)

*Verifikácia under-approx. systémov*
- Chyba v ATS dokazuje prítomnosť chyby v CTS
- Absencia chyby v ATS nedokazuje absenciu chyby v CTS
- Chyba v CTS, ktorá nie je prítomná v ATS je označovaná ako *false negative*

**Predikátová abstrakcia**
*Predikáty* - boolean výrazy o hodnotách premenných.
Príklad definície ATS: *〈Program Counter, Validity of selected predicates〉*

*Množstvo abstrakcie*
- množstvo predikátov ovplyvňuje presnosť abstrakcie
- *menej predikátov* -> veľká nejednoznačnosť, menší stavový priestor
- *viac predikátov* -> väčšia presnosť, väčší stavový priestor

**Poznámky ku predikátovej abstrakcii**

*Analýza abstraktných behov vedúcich k chybe:*
- Rozhodnutie o platnosti behu (je to false alarm?)
- Odobranie nových predikátov na spresnenie abstrakcie

*Veľkosť ATS:* Veľkosť stavového priestoru rastie **exponenciálne** s počtom predikátov

*Možné riešenie (neviem čoho, asi tej veľkosti?):* Predikáty sú viazané na konkrétne umiestnenia programu.

## 5. Metóda CEGAR/CEGAR Approach
*11. prednáška*

*CEGAR works by iteratively constructing and refining abstractions until a proper precision is reached (wiki)*

**Princíp CEGAR metódy**
- Vzhľadom na počiatočnú množinu predikátov je systém abstrahovaný (abstracted) predikátovou abstrakciou.
- ATS (over-approximation) je overený model checking procesom
- V prípade, že sa nahlásený protipríklad považuje za falošný, analyzuje sa s cieľom odvodiť nové predikáty a spresniť abstrakciu predikátov.
- Proces sa opakuje, pokiaľ nenájdeme skutočný protipríklad alebo pokiaľ systém nie je úspešne overený

*Poznámky:*
- Odvodiť nové predikáty je veľmi ťažké.

**Schéma CEGAR metódy**

### Základy abstraktnej interpretácie a statickej analýzy programov
*Neviem, či to ešte súvisi s CEGARom, je to v rovnakej prednáške*

Reprezentácia programu - **Flow-graph** (FG)
- "špeciálna verzia" control-flow grafu (CFG)
- každá hrana je strážená jedným guardom alebo definuje jedno priradenie

*Cieľ:* Vypočítať vlastnosti jednotlivých vrcholov FG
- *príklady:*
- Zistite rozsah hodnôt, ktoré môže mať konkrétna premenná v danom umiestnení programu.
- Vypočítajte množinu aktívnych premenných v danom umiestnení programu.

**Všeobecný pohľad na abstraktnú interpretáciu**

*Rozklad vlastnosti*
- Vlastnosť, ktorá sa má overiť všeobecným postupom analýzy programu, je možné rozložiť na hodnoty lokálnych údajov priradené k jednotlivým vrcholom ( C )FG.
- Výsledok overenia je zložený alebo odvodený od lokálnych hodnôt k vrcholom FG

*Zlepšenie hodnoty (Value Improvement)*
- Je definované, ako hrana ( C )FG zlepšuje (lokálne aktualizuje) rozkladanú hodnotu vlastnosti, ktorá sa má overiť.
- Aplikácia lokálnych aktualizácií postupne (monotónne) vylepšuje (aproximuje) celkové riešenie

**Všeobecný algoritmus pre výpočet abstraktnej interpretácie**

*Inicializácia*
- Spočiatku je každému vrcholu priradená vhodná hodnota.
- Každá hrana grafu je zaznačená ako *nespracovaná (unprocessed)*

*Výpočet*
1. Vyberte nespracovanú hranu grafu a vykonajte lokálnu aktualizáciu relevantnú pre hranu a súvisiace vrcholy. Ak aktualizácia vylepšila riešenie, označte hranu ako *nespracovanú* znova.
2. Opakujte, kým existujú nespracované hrany, teda kým sa nedosiadne *pevný bod (fix point)*

**Abstraktná interpretácia (AI)**
- Výber správneho nastavenia môže mať za následok overenie (výpočet) mnohých zaujímavých vlastností programu. Toto sa často kombinuje s určitou datovou abstrakciou pre premenné.
- AI môžeme vykonať na čiastočne odvinutých (unwinded) grafoch

*Parametre*
- Aká abstraktná doména je použitá
- Smer update funkcie/funkcie aktualizácie (vpred, vzad, oba).
- Čo update funkcia robí
- Ako sú hodnoty zlúčené cez viac prichádzajúcich hrán.
- Poradie spracovania nespracovaných hrán.
- Detekcia ukončenia

**Relevantné otázky abstraktnej interpretácie**

*Existuje fix-point?*
Zloženie domén hodnôt spojených s vrcholmi často vytvára úplnú mriežku. Knaster-Tarskiho veta hovorí, že každá monotónna funkcia nad takouto doménou má pevný bod.

*Skončí niekedy výpočet?*
Ak v zložení lokálnych domén neexistuje nekonečne stúpajúca postupnosť možných riešení, tak **áno**. V opačnom prípade nemusí byť ukončená.

**Widening/Rozšírenie**
- Pomocná transformácia medziproduktov taká, že zachováva správnosť a zároveň bráni existencii dlhej (možno nekonečnej) vzostupnej postupnosti hodnôt v príslušnej doméne.

*Príklad:*
Majme hranice presnosti, v ktorých chceme poznať rozsah možných hodnôt nejakej premennej. Za hranicami presnosti sa hodnoty rozšíria do nekonečna, tj. $+∞$ alebo $−∞$.

**Narrowing/Zúženie**
- Používanie rozšírenia môže viesť k veľmi nepresným výsledkom. Urýchľuje však analýzu slučiek.
- Po rozšírení môžu nadhodnotené hodnoty podliehať zúženiu (podobná, ale dvojitá technika).
- Po W + N možno vypočítať iný fixný bod.
- *pr.* interval [0,+∞] bude po narrowingu zmenšený na [0,n].