Zdroje

Zpracování jednotlivých otázek

Tato stránka je psaná tak, že se jen z ní asi nic nenaučíte, ale může být použita k zopakování před státnicemi nebo ke snazšímu pochopení toho, co není ze slajdů jasné.

Proto tady taky docela šetřím matikou a snažím se věci spíš popsat lidsky. Nikomu však samozřejmě nebráním, aby tuto stránku přpracoval do nějaké užitečnější podoby.****

Matematické struktury pro modelování chování systémů (přechodové systémy, Kripkeho struktury).

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 AtBA \le_t B, pak v BB jsou všechny trace z AA 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í = AA a BB mají ekvivalentní chování, pokud platí

    ParseError: KaTeX parse error: Undefined control sequence: \and at position 11: A \le_t B \̲a̲n̲d̲ ̲B \le_t A

    (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 AsBA \le_s B, pak pro každý stav aaAA existuje stav bbBB takový, že všechny proveditelné trace z aa jsou proveditelné i z bb (Je to silnější než kvaziuspořádání trace.)

  • simulační ekvivalence = AA a BB jsou simulačně ekvivalentní, pokud platí

    ParseError: KaTeX parse error: Undefined control sequence: \and at position 11: A \le_s B \̲a̲n̲d̲ ̲B \le_s A

    (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*).

Úvod do temporálních logik viz <Analýza%20a%20návrh%20softwarových%20systémů#Temporální%20logika>

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 φφ ve stavu ss na struktuře MM (M,sφM, s \models φ) se definuje induktivně podle velikosti formule.

  • Formuli AGAFpAG AF p č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í pp.“

    • 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 pp.“ V tomto vyjádření chybí druhý selektor cesty. Toto vyjádření by se tedy spíše hodilo na LTL formuli GFpG F p (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 AGEFφAG EF φ.

  • 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ř.

    ParseError: KaTeX parse error: Undefined control sequence: \and at position 6: E(Xr \̲a̲n̲d̲ ̲Fs)

    , tedy „Existuje cesta taková, že pro následující stav (na ní) platí rr a dále na této cestě existuje stav, pro který platí ss.“

  • CTL* je vlastní nadmnožinou CTL i LTL (

    ParseError: KaTeX parse error: Undefined control sequence: \and at position 22: …ubsetneq CTL^* \̲a̲n̲d̲ ̲LTL \subsetneq …

    ). CTL a LTL jsou neporovnatelné (

    ParseError: KaTeX parse error: Undefined control sequence: \and at position 20: …\nsubseteq LTL \̲a̲n̲d̲ ̲LTL \nsubseteq …

    ).

Základní verifikační úlohy: equivalence checking a model checking.

verifikace ekvivalence

  • Úkol ověření, jestli jsou dva programy/modely ekvivalentní (dávají stejné vystupy).

  • Jedno z možných řešení je převést oba programy/modely na OBDD a zkontrolovat jejich ekvivalenci.

    • Podrobnější popis viz následující otázka.

verifikace modelu

  • Úvod viz poslední otázka.

  • Podrobnější algoritmy verifikace viz následující otázka.

Algoritmy pro model checking a různé metody optimalizace: BDDs, partial order reduction.

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 ¬\neg,

ParseError: KaTeX parse error: Undefined control sequence: \and at position 1: \̲a̲n̲d̲

, EXEX, EGEG a EUEU.

  1. Z CTL formule vytvoříme strom podformulí.

  2. Ve stromě postupujeme odspoda a postupně projdeme každý vrchol.

  3. Pro každý vrchol stromu zjistíme, ve kterých stavech Kripkeho struktury platí a tuto informaci do stavů poznamenáme.

    • Toto je pro ¬\neg,

      ParseError: KaTeX parse error: Undefined control sequence: \and at position 1: \̲a̲n̲d̲

      a EXEX snadné.

    • Pro ostatní operátory algoritmus popíšeme dále.

  4. Až projdeme celý strom, máme ve stavech poznamenáno, jestli pro ně platí původní formule.

Algoritmus pro EφUψ
  1. Všechny stavy, kde platí ψ obarvíme a zároveň k nim poznamenáme, že formuli EφUψ splňují.

  2. Dokud máme obarvené stavy, tak opakujeme

    1. Vybereme obarvený stav a zrušíme jeho obarvení.

    2. Projdeme jeho sousedy proti směru hran:

      1. Platí-li v sousedovi φ, obarvíme ho a poznamenáme k němu, že formuli EφUψ splňuje.

Algoritmus pro EGφ
  1. 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).)

  2. Z těchto komponent postupujeme proti směru hran:

    1. Splňuje-li stav φ, poznamenáme si k němu, že splňuje EGφ.

    2. 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 MM, jeden stav z této struktury, LTL formule φφ

Výstup: informace o tom, jestli je LTL formule v daném stavu splněna

  1. Vytvoříme negaci φφ.

  2. Z ¬φ\neg φ vytvoříme Büchiho automat A¬φA_{\neg φ}.

  3. Z Kripkeho struktury MM vytvoříme Büchiho automat AMA_M.

  4. Tyto dva automaty zkombinujeme na automat A=AMA¬φA = A_M \cap A_{\neg φ}.

  5. Ověříme, jestli automat AA přijímá jazyk \emptyset. Pokud tomu tak je, tak je formule φφ 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???)

  1. Magickým způsobem se Kripkeho struktura převede na OBDD.

  2. 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.

  3. Nějak se ty dvě OBDD asi dají dohromady (konjunkcí?).

  4. 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í:

    1. Je jednoznačně určené pořadí proměnných.

    2. Neobsahují izomorfní podstromy nebo duplicitní vrcholy.

  • OBDD můžeme z BDD vytvořit aplikací tří transformací:

    1. Sloučíme duplicitní listy.

    2. Sloučíme duplicitní vnitřní vrcholy (odstraňujeme, dokud tam jsou).

    3. 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.

Specifikace chování real-time systémů

{{TODO|Nevím, neznám, neumím, nechci umět, nechci dostat.}}

Timed automata (já budu nazývat časovým automatem)

{{TODO|Nechť se do toho pustí ještě někdo jiný, já už na to nemám sílu, tak sem píšu jen jednoduchý (a možná nepřesný) přehled.}}

  • Časový automat (ČA) je automat, který vznikne z Büchiho automatu zohledněním času a to takto:

    • Máme několik časových proměnných z R\mathbb{R}.

    • Všechny časové proměnné narůstají stejně rychle.

    • Časované slovo se zapisuje jako dvojice (w,t)(w, t), kde ww je uspořádaný seznam písmen aia_i (slovo) a tt je uspořádaný seznam časů tit_i, přičemž čas tit_i odpovídá času přechodu pomocí písmene aia_i.

      • Hodnoty tit_i jsou hodnoty jakéhosi globálního časovače, který běží stejně rychle jako časové proměnné, ale nikdy se nenuluje.

    • Na každém přechodu může být určena podmínka používající časové proměnné, za které může být přechod proveden.

    • Na každém přechodu můžou být některé časové proměnné resetovány (nastaveny na 0). Provede se až po kontrole podmínky.

  • Množina všech ČA:

    • je uzavřená na sjednocení a na průnik (ten se dělá podobně bláznivým způsobem jako u Büchiho automatů).

    • není uzavřená na doplněk.

  • Převod ČA na Büchiho automat:

    • Chceme-li z časových automatů vytvořit Büchiho automat, který bude přijímat stejná slova (až na časování), vytvoříme ho podle hodinových oblastí. Ty se vytvoří následovně:

      1. Podíváme se, které hodnoty se používají v podmínkách na přechodech.

      2. Podle těchto hodnot vytvoříme diagram hodinových oblastí (viz slajdy).

      3. Z diagramu oblasti extrahujeme jako významné body hrany a plochy.

    • Mezi hodinovými oblastmi se dá udělat relace „následník“: (a,b)R    (a, b) \in R \iff z aa se do bb můžu dostat tím, že nechám plynout čas.

    • Stavy nového automatu jsou pak dvojice (stav z původního automatu, hodinová oblast).

    • Mezi těmito stavy vedou hrany. Jak se na ně přijde, to už tady musí popsat někdo jiný.

Procesové algebry.

  • Zdroj: Slajdy z přednášky Modely a verifikace chování systémů (odkazováno jako „slajdy“)

  • Procesové algebry slouží k modelování (paralelních) procesů.

  • Operátor „.“ (tečka) značí zřetězení akcí.

  • Operátor „+“ značí výběr z jedné z možností.

  • δ\delta je symbol pro konec (je u něj napsáno deadlock, ale myslím si, že by to měl být spíš úspěšný konec).

  • ϵ\epsilon (epsilon) je symbol pro neúspěšný konec.

  • Výrazy se dají pojmenovávat a potom se na ně odkazovat (dá se to chápat jako volání funkce, nebo jako stav, do kterého přejdu).

  • Operátor „||“ značí paralelní provádění dvou procesů => libovolné proložení akcí.

    • Lze jej nahradit výčtem možností proložení.

  • γ\gamma značí synchronizaci dvou akcí – tam, kde se tyto akce provádí za sebou se dá cesta zkrátit nově definovanou akcí.

  • τ\tau určuje seznam akcí, které jsou vnitřní. – Dají se nahradit za τ\tau bez parametrů, které říká: „Tady se dělá něco interního“. Více τ\tau za sebou se potom dá nahradit (ale ne ty, které rozhodují výběr cesty – změnilo by to smysl).

  • \partial určuje seznam akcí, které nelze provádět samostatně, ale jen jako součást synchronizace.

  • Procesové algebry mají axiomy.

    • +: komutativita, asociativita, idempotence, neutrální prvek

    • .: pravá distributivita, asociativita

  • Procesovými algebrami jdou modelovat automaty na nápoje.

  • druhy algeber

    • MPT (minimal process theory): +, δ\delta, .(ale jen unární operátor)

    • TSP (theory of sequential processes): +, δ\delta, ϵ\epsilon, ., pojmenovávání, parametrizace

    • ACP (algebra of communicating processes): +, δ\delta, ϵ\epsilon, ., pojmenovávání, parametrizace, ||, γ\gamma, τ\tau, \partial

  • Algebry jdou převést na LTS pomocí pravidel. Tyto pravidla jsem ale nepochopil, nicméně převod je intuitivně vidět z příkladů na slajdech.

  • Na slajdech je všechno shrnuto v příkladu ABP. Je to trochu komplikované, ale když si pořádně uvědomíte, co které písmenko znamená, pochopíte to.

Statická analýza programů.

{{TODO|Některé části jsou popsány příliš krátce a celkově je to docela chaotické}}

  • využití:

    • optimalizace kódu

      • detekce nepoužívaných proměnných

      • detekce výrazů počítaných vícekrát

    • kontrola/verifikace kódu

      • nalezení (některých) dereferencí nulových ukazatelů

      • nalezení použití neinicializovaných proměnných

  • Oproti verifikaci:

    • Nepracuje nad stavy, ale nad grafem toku řízení – nezkouší spustit program, ale podle toho, jak program vypadá usuzuje na to, jaké bude mít vlastnosti.

      • Někdy nemusí brát v potaz ani tok řízení, ale pouze deklarace např. odvozování datových typů.

    • Ne vždy umí zaručit správnost programu – výsledky jsou tedy v jistém smyslu bližší testování (ale postupy zase formální verifikaci)

      • Odpovídá ano/ne/nevím.

    • Zvládnutelná nad libovolným programem (nezabývá se mnoha stavy).

    • Použitelná nad otevřenými programy (komponenty, objekty, moduly)

  • Dělíme na:

    • intraprocedurální (pracuje jen uvnitř procedury)

      • velice časté

    • interprocedurální (meziprocedurální)

      • zvažuje i volání procedur

      • např. analýza toho, jestli mi může z metody vyběhnout výjimka – musím zvážit, jestli volané procedury nějakou vyvolávají.

      • Další možné použití (příklad neznám): Analýza ukáže, že když bude některý parametr null, tak se stane něco nepěkného. Podívá se, jestli se někde procedura (možná) volá s null a pokud ne, žádnou chybu nenahlásí.

  • hlavní prostředky:

    • svaz

      • uspořádání ve svazu: reflexivní, tranzitivní, antisymetrické

      • největší společný potomek, nejmenší společný předek

    • (ne)rovnice

      • Pro svaz končené výšky můžeme mít soustavu nn rovnic: i=1...n:xiFi(x1,...,xn)\forall i=1...n: x_i \subseteq F_i(x_1, ..., x_n).

        • Nerovnice se dají přepsat na rovnice i=1...n:xi=xiFi(x1,...,xn)\forall i=1...n: x_i = x_i \cap F_i(x_1, ..., x_n) díky xy    x=xyx \subseteq y \iff x = x \cap y.

        • Pro každý příkaz programu máme proměnnou xix_i (často množinu), která obsahuje nějakou užitečnou informaci (třeba proměnné, které jsou v tomto kroku inicializované).

        • Tato proměnná se dá funkcí FiF_i spočítat podle ostatních množin (typicky těch příkazů, které v diagramu toku řízení dotyčnému příkazu předchází nebo jej následují). Např. inicializované proměnné získám průnikem (chci aby byly určitě inicializované) inicializovaných proměnných ve všech předchozích příkazech a přidáním proměnných, které dotyčný příkaz inicializuje.

  • postup analýzy:

    1. Soustavu rovnic vyřešíme pomocí pevných bodů (u všech proměnných postupujeme s jejich hodnotami odspoda, dokud nenarazíme na pevný bod).

      • Tento postup nejde použít u funkcí, které nejsou monotónní. U takových musíme soustavu vyřešit jinak.

      • V našem příkladu tedy začneme s prázdnými množinami proměnných.

    2. Vyřešením soustavy dostaneme pro každý příkaz programu hledanou vlastnost.

      • V našem příkladu máme seznam inicializovaných proměnných. A s tím už se dá snadno zjistit, že se někde používá potenciálně neinicializovaná proměnná.

    • Podobný postup se dá použít i pokud děláme analýzu, která nezávisí na toku řízení. Tam ale nebudeme mít (asi) proměnné pro příkazy, ale pro něco jiného (třeba proměnné v programu).

  • dělení analýzy

    • podle směru

      • dopředná (hodnota xix_i záleží na xix_i pro besprostředně předcházející příkazy).

      • zpětná (hodnota xix_i záleží na xix_i pro besprostředně následující příkazy).

    • podle aproximace

      • may“ – vrací informaci, která platí alespoň pro jednu cestu programu (ve funkci se používá sjednocení).

      • must“ – vrací informaci, která platí pro všechny cesty programu (ve funkci se používá průnik).

  • analýza haldy

  • meziprocedurální analýza

    • Na slajdech jsou poměrně rozsáhle popisovány transformace CFG (diagram toku řízení). V podstatě jde o to sloučit CFG více funkcí dohromady, protože potom se na tom dá dělat meziprocedurální analýza jakoby to byla jedna procedura.

      • Problémem můžou být ukazatele na funkce. Jejich eliminace se řeší na začátku pomocí svazu (jak jinak), kdy zjistíme, na které funkce můžou které ukazatele ukazovat.

Model checking programů.

  • Zdroj 1: Slajdy z přednášky Modely a verifikace chování systémů

  • Zdroj 2: Slajdy z přednášky Analýza programů a verifikace kódu

  • (Neboli modelová čekačka na programy.)

  • Je to metoda verifikace programů.

  • Oproti testování kontroluje programy tak, že prochází všechny možné stavy => dokazování správnosti, ne hledání chyb

    • Hranice mezi verifikací modelů a testováním je neostrá – existuje mnoho metod na pomezí.

  • Vstup: program (nebo jeho model) a případně seznam předpokladů, které by měl splňovat

  • Výstup: rozhodnutí, jestli program/model předpoklady splňuje a případně protipříklad

  • Dělíme na:

    • Explicitní – v paměti vytváří všechny stavy a jednotlivě u nich kontroluje podmínky.

      • Použití nad otevřeným programem (přijímá vstupy od uživatele, jejichž doména je velká) generuje hodně stavů.

    • Symbolický – stavy sdružuje do skupin, které jsou (obvykle) popisovány logickou formulí a jejich vlastnosti se kontrolují hromadně. Šetří to paměť (a prý i čas).

  • Modely: LTS, Kripkeho struktura, STS

  • Temporální logiky: CTL, LTL, CTL*

  • Problémy:

    • Jak převést program na model, abychom neudělali chybu?

      • generovat program z modelu (=> neefektivní program)

      • verifikovat přímo program (=> hodně stavů)

    • Jak snadno zapsat požadavky na program?

      • temporální logiky

      • zapsat program v „přívětivějším“ jazyce (funkcionální, specifikační) a zkontrolovat ekvivalenci

    • Co dělat s množstvím stavů, které program má?

      • seskupit podobné stavy (partial order reduction, symbolická verifikace)

      • hešování stavů (nemusíme je držet všechny v paměti) => stále problém s časem

      • neprocházet všechny (bounded model checking) => přiblížení se k testování

    • Jak z protipříkladu zjistit, kde je chyba v programu?

      • někdy to není snadné

    • I když vyřešíme všechny předchozí problémy, pořád nevíme, jestli jsme vyrobili opravdu to, co zadavatel chce. => validace