Zadání

Specifické techniky pro verifikaci softwarových systémů, abstraktní interpretace, metody abstrakce a aproximace, redukce částečným uspořádáním, metody zjemňování abstrakcí (např. CEGAR – protipříkladem řízené zjemňování abstrakcí).

Vypracování

Upozornění: bez nároku na úplnost a korektnost. Podle hesla „lepší něco než nic“. Ale snaha byla o co nejlepší výsledek.

Abstraktní interpretace

  • metoda symbolického MC/statická analýza
  • místo nad skutečnými doménami proměnných se program interpretuje nad abstraktními

Jen pro úplnost:

  • abstraktní doména musí tvořit úplný svaz
  • místo každé instrukce definujeme monotónní funkci

An abstract interpretation I of a program P with n program locations is a tuple I = <L, ◦, ≤, T, ⊥, F> where (L, ≤) is a complete lattice, T and ⊥ are one and zero of (L, ≤), ◦ is equal either to [průsek nebo spojení] operation, and F is a monotone function on product lattice (Ln , ≤) defining the interpretation of basic instructions.

Metody abstrakce a aproximace

Redukce částečným uspořádáním

Princip redukce: Při generování grafů se místo funkce všech přímých následníků uvažuj pouze někteří přímí následníci vrcholu. V důsledku toho je počet vygenerovaných stavů produktového automatu menší.

Technická realizace: Optimální způsob výběru následníků je obtížný. Nástroje implementují různé heuristiky. Redukovaný stavový prostor musí zachovávat přítomnost akceptujícího cyklu. Formule nesmí obsahovat operátor X (podtřída LTL).

Metody zjemňování abstrakcí

CEGAR – protipříkladem řízené zjemňování abstrakcí

  • idea: verifikujeme overaproximovaný model systému – pokud splňuje specifikaci, v pořádku; pokud ne a nejde o falešný protipříklad, „OK“; jinak přidáme do abstrakce predikáty, které odpovídající chování odstraní (netriviální)
  • metoda ale nemusí nikdy skončit

Předměty

Související otázky

You could leave a comment if you were logged in.
mgr-szz/in-pds/7-pds.txt · Poslední úprava: 2016/07/27 23:42 autor: xm
Nahoru
CC Attribution-Noncommercial-Share Alike 3.0 Unported
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0