Modely a verifikace programů

Zdroje

• Slajdy z přednášky Modely a verifikace chování systémů
• Slajdy z přednášky Analýza programů a verifikace kódu

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

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

• K čemu to je je jasné z otázky.

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 $ A \le_t B $, pak v $ B $ jsou všechny trace z $ A $ 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í = $ A $ a $ B $ mají ekvivalentní chování, pokud platí $ A \le_t B \and 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 $ A \le_s B $, pak pro každý stav $ a $ z $ A $ existuje stav $ b $ v $ B $ takový, že všechny proveditelné trace z $ a $ jsou proveditelné i z $ b $ (Je to silnější než kvaziuspořádání trace.)
• simulační ekvivalence = $ A $ a $ B $ jsou simulačně ekvivalentní, pokud platí $ A \le_s B \and 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*).

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

Úvod do temporálních logik viz 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 $ φ $ ve stavu $ s $ na struktuře $ M $ ($ M, s \models φ $) se definuje induktivně podle velikosti formule.
• Formuli $ AG 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í $ p $.“
  • 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 $ p $.“ V tomto vyjádření chybí druhý selektor cesty. Toto vyjádření by se tedy spíše hodilo na LTL formuli $ G 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 $ 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ř. $ E(Xr \and Fs) $, tedy „Existuje cesta taková, že pro následující stav (na ní) platí $ r $ a dále na této cestě existuje stav, pro který platí $ s $.“
• CTL* je vlastní nadmnožinou CTL i LTL ($ CTL \subsetneq CTL^* \and LTL \subsetneq CTL^* $). CTL a LTL jsou neporovnatelné ($ CTL \nsubseteq LTL \and LTL \nsubseteq CTL $).

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.

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

• K čemu je model checking viz poslední otázka.

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 $, $ \and $, $ EX $, $ EG $ a $ EU $.

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 $, $ \and $ a $ EX $ 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 $ M $, 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_{\neg φ} $.
3. Z Kripkeho struktury $ M $ vytvoříme Büchiho automat $ A_M $.
4. Tyto dva automaty zkombinujeme na automat $ A = A_M \cap A_{\neg φ} $.
5. Ověříme, jestli automat $ A $ 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.

Tato část je neúplná a potřebuje rozšířit. Podrobněji popsat.

Specifikace chování real-time systémů, timed automata.

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

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

Tato část je neúplná a potřebuje rozšířit. Nevím, neznám, neumím, nechci umět, nechci dostat.

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

Tato část je neúplná a potřebuje rozšířit. 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 $ \mathbb{R} $.
  • Všechny časové proměnné narůstají stejně rychle.
  • Časované slovo se zapisuje jako dvojice $ (w, t) $, kde $ w $ je uspořádaný seznam písmen $ a_i $ (slovo) a $ t $ je uspořádaný seznam časů $ t_i $, přičemž čas $ t_i $ odpovídá času přechodu pomocí písmene $ a_i $.
    • Hodnoty $ t_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) \in R \iff $ z $ a $ se do $ b $ 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ů.

• Zdroj: Slajdy z přednášky Analýza programů a verifikace kódu (odkazováno jako „slajdy“)

Tato část je neúplná a potřebuje rozšířit. 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 $ n $ rovnic: $ \forall i=1...n: x_i \subseteq F_i(x_1, ..., x_n) $.
      • Nerovnice se dají přepsat na rovnice $ \forall i=1...n: x_i = x_i \cap F_i(x_1, ..., x_n) $ díky $ x \subseteq y \iff x = x \cap y $.
      • Pro každý příkaz programu máme proměnnou $ x_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í $ F_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 $ x_i $ záleží na $ x_i $ pro besprostředně předcházející příkazy).
    • zpětná (hodnota $ x_i $ záleží na $ x_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