= 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í.
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).
=== 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 ===
=== kontrola modelu ===
== Algoritmy pro model checking a různé metody optimalizace: BDDs, partial order reduction. ==
=== algoritmy pro modelchecking ===
=== BDDs ===
=== partial order reduction ===
== Specifikace chování real-time systémů, timed automata. ==
=== timed automata ===
== Procesové algebry. ==
== Statická analýza programů. ==
=== svazy ===
== Model checking programů. ==
