= Zdroje =
* [http://d3s.mff.cuni.cz/teaching/system_behaviour_models/ Slajdy z přednášky Modely a verifikace chování systémů]
* [http://d3s.mff.cuni.cz/teaching/program_analysis_verification/ Slajdy z přednášky Analýza programů a verifikace kódu]
= Zpracování jednotlivých otázek =
== Matematické struktury pro modelování chování systémů (přechodové systémy, Kripkeho struktury). ==
* Zdroj: [http://d3s.mff.cuni.cz/teaching/system_behaviour_models/ Slajdy z přednášky Modely a verifikace chování systémů] (odkazováno jako „slajdy“)
=== LTS (labeled transition system) ===
* graf
** Ve vrcholech nic není,
** na hranách jsou příkazy (většinou vstupní, tedy příkazy programu, ale můžou být i výstupní).
==== Pojmy ====
* '''trace''' = něco jako cesta v konečném automatu, ale na rozdíl od cesty může být trace nekonečná.
* '''kvaziuspořádání trace''' (trace preorder) = je-li <math>A \le_t B</math>, pak v <math>B</math> jsou všechny trace z <math>A</math> proveditelné
* '''vstupní popisek''' = popisek na hraně začínající ''otazníkem'' – značí vstupní příkaz od uživatele
* '''výstupní popisek''' = popisek na hraně začínající ''vykřičníkem'' – značí výstup z programu
* '''ekvivalence chování''' = <math>A</math> a <math>B</math> mají ekvivalentní chování, pokud platí <math>A \le_t B \and B \le_t A</math> (Mám-li předem danou trace, tak ji můžu provést buď v obou LTS nebo ani v jednom.)
* '''simulační kvaziuspořádání''' = je-li <math>A \le_s B</math>, pak pro každý stav <math>a</math> z <math>A</math> existuje stav <math>b</math> v <math>B</math> takový, že všechny proveditelné trace z <math>a</math> jsou proveditelné i z <math>b</math> (Je to silnější než kvaziuspořádání trace.)
* '''simulační ekvivalence''' = <math>A</math> a <math>B</math> jsou simulačně ekvivalentní, pokud platí <math>A \le_s B \and B \le_s A</math> (Chování jednoho LTS můžu simulovat LTS druhým a naopak.)
* '''(silná) bisimulační ekvivalence''' = viz slajdy
''Poznámka'': Jsou-li LTS deterministické, jsou ekvivalence chování, simulační ekvivalence a (silná) bisimulační ekvivalence ekvivalentní.
=== Kripkeho struktura ===
* graf
** Ve vrcholech jsou stavy programu (ohodnocení proměnných),
** na hranách nic není.
** Pro každý vrchol existuje alespoň jedna přechodová hrana do nějakého (klidně stejného) vrcholu. Důležité je, aby neexistoval stav, ze kterého by se nedalo pokračovat dál.
''Poznámka'': Tady se neříká ''trace'', ale ''cesta''. Stále však může být nekonečná.
=== State transition system ===
* kombinace LTS a Kripkeho struktury
* graf
** Ve vrcholech jsou stavy programu (ohodnocení proměnných),
** na hranách jsou příkazy.
== Specifikace vlastností systému pomocí temporálních logik (LTL, CTL, CTL*). ==
* Zdroj: [http://d3s.mff.cuni.cz/teaching/system_behaviour_models/ Slajdy z přednášky Modely a verifikace chování systémů] (odkazováno jako „slajdy“)
Úvod do temporálních logik viz [[Analýza a návrh softwarových systémů#Temporální logika|otázka Temporální logika v jiném okruhu]]
=== CTL (computation tree logic) ===
Logika, kde jsou formule složené z klasických logických formulí a zvláštních operátorů.
==== Selektory cest ====
* '''A''' = všechny cesty z daného bodu
* '''E''' = alespoň jedna cesta z daného bodu
==== Selektory stavů na vybrané cestě ====
* '''X''' = následující stav
* '''G''' = všechny stavy
* '''F''' = některý z budoucích stavů
* '''U''' = pro některý z budoucích stavů platí druhá formule a ve všech předešlých platí první formule
* Tyto selektory se '''vždy''' používají v párech jako operátory: AXφ, AGφ, AFφ, AφUψ, EXφ, EGφ, EFφ, EφUψ
* Úloha verifikace modelu spočívá v rozhodnutí, jestli je formule v CTL splněna na zadané Kripkeho struktuře.
* Splněnost formule <math>φ</math> ve stavu <math>s</math> na struktuře <math>M</math> (<math>M, s \models φ</math>) se definuje induktivně podle velikosti formule.
* Formuli <math>AG AF p</math> čteme jako „Pro každou cestu (c1) platí, že pro každý stav (s1) na této cestě (c1) platí, že na všech cestách (c2) z tohoto stavu (s1) existuje stav (s2), pro který platí <math>p</math>.“
** Někdy jde čtení zjednodušit, ale je potřeba při tom dávat pozor.
** Např. nelze říci: „Pro všechny následující stavy platí, že někdy v budoucnu bude platit <math>p</math>.“ V tomto vyjádření chybí druhý selektor cesty. Toto vyjádření by se tedy spíše hodilo na LTL formuli <math>G F p</math> (viz dále).
* Všechny formule jdou vyjářit jen pomocí operátorů EX, EG a EU.
=== LTL ===
* Podobné jako CTL, ale jsou „jen“ lineární, tedy zvažují každou cestu samostatně.
* Výhodou oproti CTL je, že se dají přeložit na Büchiho automat.
* Na začátku je jakoby implicitní '''A''', takže formule musí platit pro všechny cesty.
* Používají se jen selektory X, G, F a U jako samostatné operátory.
* Pro porozumění rozdílu mezi CTL a LTL doporučuji slajdy, kde je rozdíl demonstrován mj. na formuli <math>AG EF φ</math>.
* Splněnost formule se opět definuje induktivně podle její velikosti.
=== CTL* ===
* Sloučení CTL a LTL.
* Používají se jednotlivé selektory z CTL jako operátory. Lze tedy napsat např. <math>E(Xr \and Fs)</math>, tedy „Existuje cesta taková, že pro následující stav (na ní) platí <math>r</math> a dále na této cestě existuje stav, pro který platí <math>s</math>.“
* CTL* je vlastní nadmnožinou CTL i LTL (<math>CTL \subsetneq CTL^* \and LTL \subsetneq CTL^*</math>). CTL a LTL jsou neporovnatelné (<math>CTL \nsubseteq LTL \and LTL \nsubseteq CTL</math>).
== Základní verifikační úlohy: equivalence checking a model checking. ==
=== kontrola ekvivalence ===
{{TODO}}
=== kontrola modelu ===
{{TODO}}
== Algoritmy pro model checking a různé metody optimalizace: BDDs, partial order reduction. ==
* Zdroj: [http://d3s.mff.cuni.cz/teaching/system_behaviour_models/ Slajdy z přednášky Modely a verifikace chování systémů] (odkazováno jako „slajdy“)
=== Algoritmy pro model checking ===
* Dělíme na symbolické a explicitní.
* Explicitní vytváří v paměti všechny stavy.
* Symbolické popíšou skupiny stavů formulemi a potom s určitou skupinou pracují najednou – šetří to paměť.
==== Algoritmus pro verifikaci modelu pomocí CTL ====
* Jedná se o explicitní verifikaci.
'''Vstup''': Kripkeho struktura, CTL formule
'''Výstup''': Pro každý stav Kripkeho strukutry rozhodnutí, jestli tam CTL formule platí.
''Poznámka'': Každou CTL formuli lze přepsat tak, že bude používat jen operátory <math>\neg</math>, <math>\and</math>, <math>EX</math>, <math>EG</math> a <math>EU</math>.
# Z CTL formule vytvoříme strom podformulí.
# Ve stromě postupujeme odspoda a postupně projdeme každý vrchol.
# Pro každý vrchol stromu zjistíme, ve kterých stavech Kripkeho struktury platí a tuto informaci do stavů poznamenáme.
#* Toto je pro <math>\neg</math>, <math>\and</math> a <math>EX</math> snadné.
#* Pro ostatní operátory algoritmus popíšeme dále.
# Až projdeme celý strom, máme ve stavech poznamenáno, jestli pro ně platí původní formule.
===== Algoritmus pro EφUψ =====
# Všechny stavy, kde platí ψ obarvíme a zároveň k nim poznamenáme, že formuli EφUψ splňují.
# Dokud máme obarvené stavy, tak opakujeme
## Vybereme obarvený stav a zrušíme jeho obarvení.
## Projdeme jeho sousedy '''proti''' směru hran:
### Platí-li v sousedovi φ, obarvíme ho a poznamenáme k němu, že formuli EφUψ splňuje.
===== Algoritmus pro EGφ =====
# Najdeme netriviální silně souvislé komponenty Kripkeho struktury (tedy takové části grafu, ve kterých můžeme do nekonečna přecházet mezi vrcholy) takové, že ve všech jejich stavech platí φ. (Můžeme si dovolit ignorovat stavy, které φ splňují a nedá se z nich nikam jít, protože Kripkeho struktura takové stavy nemá (viz její popis výše).)
# Z těchto komponent postupujeme '''proti''' směru hran:
## Splňuje-li stav φ, poznamenáme si k němu, že splňuje EGφ.
## Pokud stav φ nesplňuje, už z něj dál nepokračujeme.
===== Spravedlnost =====
* U některých struktur můžeme přijít na to, že neumíme sestavit formuli tak, aby vyjadřovala to, co chceme, protože se nám automat může do nekonečna cyklit ve stavu, ve kterém se ve skutečnosti nějakou dobu cyklí, ale nikdy ne do nekonečna.
* Potřebujeme zajistit to, aby se braly v úvahu jen spravedlivé (fair) cesty.
** Spravedlivá cesta je taková, která nekonečně mnohokrát (v originále dle mého soudu nepřesně „infinitely often“) prochází stavem z množiny spravedlivých stavů.
** Množina spravedlivých stavů je většinou určena CTL formulí (stavy, kde platí).
{{TODO|Nějaký symbolický algoritmus nad OBDD}}
=== BDDs ===
{{TODO}}
=== partial order reduction ===
{{TODO}}
== Specifikace chování real-time systémů, timed automata. ==
=== timed automata ===
{{TODO}}
== Procesové algebry. ==
{{TODO}}
== Statická analýza programů. ==
=== svazy ===
{{TODO}}
== Model checking programů. ==
{{TODO}}
