= 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í).
==== Algoritmus pro verifikaci modelu pomocí LTL ====
* Jedná se o explicitní verifikaci.
'''Vstup''': Kripkeho struktura <math>M</math>, jeden stav z této struktury, LTL formule <math>φ</math>
'''Výstup''': informace o tom, jestli je LTL formule v daném stavu splněna
# Vytvoříme negaci <math>φ</math>.
# Z <math>\neg φ</math> vytvoříme Büchiho automat <math>A_{\neg φ}</math>.
# Z Kripkeho struktury <math>M</math> vytvoříme Büchiho automat <math>A_M</math>.
# Tyto dva automaty zkombinujeme na automat <math>A = A_M \cap A_{\neg φ}</math>.
# Ověříme, jestli automat <math>A</math> přijímá jazyk <math>\emptyset</math>. Pokud tomu tak je, tak je formule <math>φ</math> splněna, jinak ne.
Tento algoritmus je podrobně rozepsán na slajdech.
==== Algoritmus pro verifikaci modelu pomocí OBDD ====
* Jedná se o symbolickou verifikaci.
'''Vstup''': Kripkeho struktura, CTL formule
'''Výstup''': Jestli je CTL formule splněna (ve kterém stavu???)
# Magickým způsobem se Kripkeho struktura převede na OBDD.
# Ještě magičtějším způsobem se na OBDD převede i CTL formule.
#* Pro logické formule je to jednoduché.
#* EX se převede nějak divně.
#* EG a EU se převedou pomocí pevného bodu.
# Nějak se ty dvě OBDD asi dají dohromady (konjunkcí?).
# Očekával bych, že se vyhodnotí splnitelnost výsledného OBDD kontrolou izomorfnosti s OBDD formule „nepravda“ (viz popis OBDD dále).
Kdo chcete, mrkněte se na to podrobněji, mě už se do toho nechtělo.
=== Binární rozhodovací diagramy ===
* Víme co je '''binární rozhodovací strom''' (BDT) pro nějakou logickou formuli (ve vrcholech proměnné, na hranách 1 nebo 0, v každé hladině jedna proměnná, v listech vyhodnocení výrazu).
* '''Binární rozhodovací diagram''' (BDD) je zobecněním binárního rozhodovacího stromu, kdy můžou být synové sdílení.
* '''Seřazené binární rozhodovací diagramy''' (OBDD) jsou BDD, které splňují:
*# Je jednoznačně určené pořadí proměnných.
*# Neobsahují izomorfní podstromy nebo duplicitní vrcholy.
* OBDD můžeme z BDD vytvořit aplikací tří transformací:
*# Sloučíme duplicitní listy.
*# Sloučíme duplicitní vnitřní vrcholy (odstraňujeme, dokud tam jsou).
*# Odstraníme nerozhodující vrcholy (ty, jejichž oba odkazy ukazují na stejného syna).
* OBDD je jednoznačné, tedy:
** Ekvivalenci dvou formulí zjistím tak, že z nich udělám OBDD a zkontroluji, jestli jsou izomorfní.
** Splnitelnost formule ověřím tak, že zkontroluji její ekvivalenci s formulí „nepravda“.
* Velikost OBDD je závislá na pořadí proměnných. Nalézt (nebo dokonce ověřit) optimální pořadí je NP-úplný problém. Proto máme různé heuristiky.
* Kripkeho strukturu je možné převést na OBDD.
=== Partial order reduction ===
* Kombinací dvou paralelních STS (state transition system) vznikne mnoho stavů, které jsou ale ve skutečnosti z pohledu verifikace duplicitní. Metoda Partial order reduction se snaží tyto duplicitní stavy zase sloučit.
{{TODO|Podrobněji popsat.}}
== Specifikace chování real-time systémů, timed automata. ==
=== Timed automata ===
{{TODO|Takové ty grafy s čmáranicema.}}
== Procesové algebry. ==
{{TODO|Bůh ví, co tu má být.}}
== Statická analýza programů. ==
{{TODO|Svazy a práce s nimi}}
== Model checking programů. ==
{{TODO|Asi přehledová otázka}}
