IV113 Validace a verifikace
Symbolický přístup k metodě ověřování modelu
Jiří Barnat
Problém stavové exploze při ověřování modelu
Requirements
Specification
Property
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelingFormalization
IV113 Úvod do validace a verifikace: Symbolický MC str. 2/31
Problém stavové exploze při ověřování modelu
Verification Failure
Requirements
Specification
Property
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelingFormalization
IV113 Úvod do validace a verifikace: Symbolický MC str. 2/31
Motivace
Pozorování
Stav modelovaného systému je určen valuací proměnných.
Každá proměnná má konečnou doménu, její hodnotu lze
uložit s využitím pevně stanoveného počtu bitů.
Stav je v paměti počítače reprezentován jako bitový
vektor (a1, . . . , an) fixní délky n.
Množiny stavů
Algoritmy pro verifikaci uchovávají množiny stavů.
Množinu stavů lze chápat jako množinu binárních vektorů.
Množinu binárních vektorů lze popsat boolovskou
funkcí.
IV113 Úvod do validace a verifikace: Symbolický MC str. 3/31
Boolovské funkce
Boolovské funkce
Jsou formule výrokové logiky, nad konečnou množinou
proměnných typu Bool.
Příklad
Stav systému je dán valuací 4 proměnných (a1,b1,a2,b2)
každé do 2 hodnotové domény {0,1}.
Stav systému je chybový, pokud se shodují proměnné
a1 a b1 a proměnné a2 a b2.
Popište množinu chybových stavů boolovskou funkcí.
Některá možná řešení
IV113 Úvod do validace a verifikace: Symbolický MC str. 4/31
Boolovské funkce
Boolovské funkce
Jsou formule výrokové logiky, nad konečnou množinou
proměnných typu Bool.
Příklad
Stav systému je dán valuací 4 proměnných (a1,b1,a2,b2)
každé do 2 hodnotové domény {0,1}.
Stav systému je chybový, pokud se shodují proměnné
a1 a b1 a proměnné a2 a b2.
Popište množinu chybových stavů boolovskou funkcí.
Některá možná řešení
(a1 ∧ b1 ∧ a2 ∧ b2) ∨ (a1 ∧ b1 ∧ ¬a2 ∧ ¬b2)∨
(¬a1 ∧ ¬b1 ∧ ¬a2 ∧ ¬b2) ∨ (¬a1 ∧ ¬b1 ∧ a2 ∧ b2)
a1 ⇔ b1 ∧ a2 ⇔ b2
IV113 Úvod do validace a verifikace: Symbolický MC str. 4/31
Reprezentace boolovských funkcí
Binární rozhodovací stromy (BDTs)
Orientovaný strom s právě jedním kořenem.
Každý vnitřní vrchol je označen binární proměnnou (v) a
má právě 2 následníky (low(v), high(v)).
Každý list je označen binární hodnotou (0,1).
Kódování boolovské funkce pomocí BDT
Každá kombinace hodnot vstupních proměnných odpovídá
právě jedné cestě z kořene stromu do listu.
Hodnoty uložené v jednotlivých listech udávají hodnoty
funkce pro jednotlivé vstupy.
IV113 Úvod do validace a verifikace: Symbolický MC str. 5/31
Binární rozhodovací strom ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2)
IV113 Úvod do validace a verifikace: Symbolický MC str. 6/31
Reprezentace boolovských funkcí
Nevýhoda BDTs
BDTs jsou zbytečně prostorově náročné (obsahují
redundantní informace).
Příklad
Identifikujte isomorfní podstromy BDT z předchozího
příkladu.
Binární rozhodovací diagram (BDD)
Acyklický graf, jehož vrcholy mají výstupní stupeň vždy
buď 0 (listy) nebo 2 (vnitřní vrcholy).
Vrcholy BDD mají stejné atributy jako vrcholy BDT.
IV113 Úvod do validace a verifikace: Symbolický MC str. 7/31
Vytvoření (minimálního) BDD
Inicializace
Pro danou boolovskou funkci uvaž nějaké BDD (BDT).
Eliminace nedosažitelných vrcholů
Odstraň vrcholy nedosažitelné z kořene BDD.
Eliminace duplikátních listů
1) Odstraň až na jeden stejně označené listy BDT.
2) Všechny hrany eliminovaných stejně označených listů přepoj do
zbývajícího stejně označeného listu.
Opakovaně aplikuj následující transformace
Eliminace duplikátních (vnitřních) vrcholů
Pokud v BDD existují stejně označené vnitřní vrcholy u, v
takové, že low(v) = low(u) a high(v) = high(u), tak odstraň
vrchol u a hrany původně vedoucí do vrcholu u přepoj do
vrcholu v.
Eliminace zbytečných testů
Eliminuj vnitřní vrchol v, pokud low(v) = high(v) a hrany
původně vedoucí do v přepoj do vrcholu low(v).
IV113 Úvod do validace a verifikace: Symbolický MC str. 8/31
BDD pro ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2)
IV113 Úvod do validace a verifikace: Symbolický MC str. 9/31
Kódování boolovské funkce pomocí BDD
Tvrzení
Každý vrchol v binárního rozhodovacího diagramu kóduje
nějakou boolovskou funkci Fv (x1, . . . , xn).
Výpočet Fv (x1, . . . , xn) pro konkrétní hodnoty h1, . . . , hn.
Je-li vrchol v list, pak
Fv (h1, . . . , hn) = 1, pokud je list v označen hodnotou 1.
Fv (h1, . . . , hn) = 0, pokud je list v označen hodnotou 0.
Je-li vrchol v vnitřní vrchol označený proměnou xi , pak
Fv (h1, . . . , hn) = Flow(v)(h1, . . . , hn), pokud hi == 0.
Fv (h1, . . . , hn) = Fhigh(v)(h1, . . . , hn), pokud hi == 1.
IV113 Úvod do validace a verifikace: Symbolický MC str. 10/31
Uspořádání proměnných v BDD — OBDD
Pozorování
Každý mezivýsledek výpočtu minimálního BDD je BDD.
Výpočet minimálního BDD lze začít v libovolném BDD.
Pro danou boolovskou funkci existují různá BDD.
Kanonická forma BDD
Minimální BDD vzniklé z BDT s předem daným pořadím
proměnných je určeno jednoznačně.
BDD s fixovaným pořadím proměnných se označují jako
Ordered BDD (OBDD).
Kanonizace
Kanonizaci BDD, které respektuje pořadí proměnných lze
provést v čase O(n), kde n je velikost původního BDD.
[Transformace se aplikují nejprve na vrcholy, které jsou
označeny větší proměnnou.]
IV113 Úvod do validace a verifikace: Symbolický MC str. 11/31
Různá OBDD dle různého uspořádání proměnných
IV113 Úvod do validace a verifikace: Symbolický MC str. 12/31
Operace restrikce na OBDD
Pozorování
Každé OBDD reprezentuje nějakou boolovskou funkci.
Boolovské funkce lze skládat pomocí unárních a binárních
logických operátorů (¬, ∧, ∨, =⇒ , XOR, . . .).
Skládání lze přenést na OBDD.
Aplikace operací na OBDD – funkce Apply
Máme OBDD O a O , která odpovídají funkcím f a f .
Chceme proceduru Apply(O, O , ), která vypočítá OBDD
odpovídající složení funkcí f a f logickým operátorem .
IV113 Úvod do validace a verifikace: Symbolický MC str. 13/31
Operace restrikce
Operace restrikce
Fxi ←b(x1, . . . , xn) = F(x1, . . . , xi−1, b, xi+1, . . . , xn)
Vytvoří boolovskou funkci s menším počtem proměnných.
Realizace na OBDD
Pokud je kořen r označen proměnnou xi , novým kořenem
se stává vrchol
low(r) pokud b = 0
high(r) pokud b = 1
Pokud vrchol v má hranu vedoucí do vrcholu t označeným
proměnou xi , tak se tato hrana přepojí do:
low(t) pokud b = 0
high(t) pokud b = 1
OBDD se minimalizuje (vrcholy xi jsou nedosažitelné).
IV113 Úvod do validace a verifikace: Symbolický MC str. 14/31
Shannonova expanze
Shannonova expanze
Pro aplikaci libovolného binární logického operátoru lze
využít tzv. Shannonovu expanzi:
F = (¬x ∧ Fx←0) ∨ (x ∧ Fx←1)
Pokud F = f f , kde je binární logická operace, pak
f f = (¬x ∧ (fx←0 fx←0)) ∨ (x ∧ (fx←1 fx←1))
IV113 Úvod do validace a verifikace: Symbolický MC str. 15/31
Ostatní operace na OBDD
Apply(O, O , )
Nechť v, v jsou kořenové uzly O, O , označené proměnnými x, x .
Pokud v a v jsou listy označené hodnotami h a h , pak vrať list
označený hodnotou h h .
Jinak, pokud
x = x pak vrať nový vrchol w označený proměnnou x, kde
low(w) = Apply(low(v), low(v ), )
high(w) = Apply(high(v), high(v ), )
x < x pak vrať nový vrchol w označený proměnnou x, kde
low(w) = Apply(low(v), O , )
high(w) = Apply(high(v), O , )
x < x pak vrať nový vrchol w označený proměnnou x , kde
low(w) = Apply(O, low(v), )
high(w) = Apply(O, high(v), )
IV113 Úvod do validace a verifikace: Symbolický MC str. 16/31
Operace negace a test na prázdnost
Pozorování
Pokud OBDD X realizuje funkci FX , tak OBDD Y
realizující funkci ¬FX se vytvoří kopií OBDD X a
přeznačením listů kopie duální hodnotou.
Test na prázdnost
OBDD mají kanonický tvar.
Kanonické OBDD reprezentující prázdnou množinu je
vždy tvořeno pouze listem označeným hodnotou 0.
Test na přítomnost stavu v množině
Vytvořím OBDD realizující jednoprvkovou množinu s
dotazovaným stavem.
Aplikuji operaci ∧ na dané OBDD.
Provedu test na prázdnost.
IV113 Úvod do validace a verifikace: Symbolický MC str. 17/31
Sekce
Symbolická reprezentace Kripkeho struktury
IV113 Úvod do validace a verifikace: Symbolický MC str. 18/31
Kódování přechodové funkce KS pomocí OBDD
Pozorování
Stav Kripkeho struktury M = (S, T, I) je popsán n
binárními proměnnými a1, . . . , an.
Každou podmnožinu stavů Kripkeho struktury je možné
zachytit pomocí OBDD s n proměnnými.
Podobně přechodovou relaci T ⊆ S × S je možné kódovat
boolovskou funkcí s 2n proměnnými.
Zjednodušení reprezentace OBDD
Hrany vedoucí do listu 0 je možné vynechat.
Neexistence hrany indikuje přechod do listu 0.
IV113 Úvod do validace a verifikace: Symbolický MC str. 19/31
Příklad
M = ({00, 01, 11}}, {(11, 00), (11, 01), (01, 00)}, I)
11 01
00
T lze popsat pomocí F(a, b, a , b )
F(a, b, a , b ) =
(a∧b ∧¬a ∧b )∨(a∧b ∧¬a ∧¬b )∨(¬a∧b ∧¬a ∧¬b )
Zakreslete OBDD pro F je-li dáno a < b < a < b .
IV113 Úvod do validace a verifikace: Symbolický MC str. 20/31
Následníci množiny stavů
Pozorování
Mějme M = (S, T, I) a OBDDT (a, b, a , b ).
Mějme množinu stavů X zadanou pomocí OBDDX (a, b).
Z OBDDT a OBDDX lze vytvořit OBDDX (a , b ), které
reprezentuje množinu následníků množiny X, tj.
X = {v ∈ S | u ∈ X ∧ (u, v) ∈ T}.
IV113 Úvod do validace a verifikace: Symbolický MC str. 21/31
Následníci množiny stavů
Výpočet OBDDX (intuitivně)
OBDDX = Apply(OBDDT , OBDDX , ∧)
Modifikuj OBDDX tak, aby na každé cestě byl vrchol a .
V OBDDX smaž všechny vrcholy a a b.
Postupně vol všechny vrcholy označené a jako kořeny a
vypočti k nim minimální OBDD.
Množinu vypočtených OBDD spoj pomocí operace ∨.
Výsledné OBDD minimalizuj.
Přejmenuj čárkované proměnné na nečárkované.
Příklad
Spočítejte reprezentaci následníků množiny {00, 11}.
IV113 Úvod do validace a verifikace: Symbolický MC str. 22/31
Předchůdci množiny stavů
Podobně lze počítat předchůdce dané množiny
(intuitivně).
Přeznač proměnné v OBDDX na čárkované.
OBDDX = Apply(OBDDT , OBDDX , ∧)
Modifikuj OBDDX tak, aby na každé cestě byl vrchol a .
Vrcholy a , ze kterých neexistuje cesta do listu
ohodnoceným 1 nahraď novým listem ohodnoceným 0.
Ostatní vrcholy a nahraď listem ohodnoceným 1.
Smaž staré listy a ostatní vrcholy označené čárkovanou
proměnnou a minimalizuj OBDD.
Příklad
Spočítejte OBDD reprezentující množinu stavů {00}.
Spočítejte OBDD reprezentující předchůdce dané množiny.
IV113 Úvod do validace a verifikace: Symbolický MC str. 23/31
Sekce
Symbolický přístup k verifikaci CTL
IV113 Úvod do validace a verifikace: Symbolický MC str. 24/31
Připomenutí
Pozorování
Znám-li pro každý stav platnost formulí ϕ a ψ, snadno
odvodím platnost formulí ¬ϕ, ϕ ∨ ψ, EX ϕ, . . . .
Idea algoritmu pro CTL Model Checking
Je dána Kripkeho struktura M = (S, T, I) a formule ϕ.
Spočítám značkovací funkci label : S → 2ϕ
, která o
každém stavu s ∈ S Kripkeho struktury M řekne jaké
podformule formule ϕ platí v daném stavu.
Platí, že s0 |= ϕ ⇐⇒ ϕ ∈ label(s0).
Funkci label budu počítat postupně pro jednotlivé
podformule formule ϕ, a to od nejjednodušších podformulí
(atomické propozice) ke složitějším (až po podformuli ϕ).
IV113 Úvod do validace a verifikace: Symbolický MC str. 25/31
Symbolický přístup
Myšlenka
Budu si kompaktně pamatovat/budovat množiny stavů,
ve kterých platí jednotlivé podformule verifikované CTL
formule.
Explicitní počítání funkce label nahradím manipulací
s těmito kompaktními reprezentacemi.
Realizace
Množiny stavů udržovány pomocí OBDD struktur.
Výchozím bodem jsou OBDD pro jednotlivé AP.
Podle struktury formule počítám OBDD pro jednotlivé
podformule.
Otestuji přítomnost iniciálního stavu v množině stavů
splňující verifikovanou formuli.
IV113 Úvod do validace a verifikace: Symbolický MC str. 26/31
Atomické propozice a logické operátory
Připomenutí syntax CTL
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ
Výpočet množiny stavů splňující CTL formuli
Značení
F(ψ) označme (funkci popisující) množinu stavů splňující ψ.
Succ(X) označme všechny následníky množiny stavů X.
Pred(X) označme všechny předchůdce množiny stavů X.
Boolovské funkce pro atomické propozice
Atomická propozice se vyjadřuje o platnosti proměnných.
Atomická propozice je boolovská funkce.
Výpočet logických operátorů (¬, ∨)
F(¬ψ1) = ¬(Fψ1)
F(ϕ ∨ ψ) = F(ϕ) ∨ F(ψ)
IV113 Úvod do validace a verifikace: Symbolický MC str. 27/31
Temporální operátory EX(ϕ), E[ϕ U ψ] a EG(ϕ)
Množina splňující EX(ϕ)
F(EX(ϕ)) = Pred(F(ϕ))
Množina splňující E(ϕ U ψ)
F(E(ϕ U ψ)) = X,
kde X je nejmenší pevný bod rekurzivního předpisu
X = F(ψ) ∪ (F(ϕ) ∩ EX(X))
Množina splňující EG (ϕ)
F(EG ϕ) = X,
kde X je největší pevný bod rekurzivního předpisu
X = F(ϕ) ∩ EX(X)
IV113 Úvod do validace a verifikace: Symbolický MC str. 28/31
Výpočet pevných bodů
Nejmenší pevný bod f (x)
proc LFP(f )
X = ∅
Xold = ∅
do
Xold = X
X := f (X)
while (X = Xold)
end
Největší pevný bod f (x)
proc GFP(f )
X = S
Xold = S
do
Xold = X
X := f (X)
while (X = Xold)
end
IV113 Úvod do validace a verifikace: Symbolický MC str. 29/31
Sekce
Ověřování modelu – shrnutí
IV113 Úvod do validace a verifikace: Symbolický MC str. 30/31
Ověřování modelu – shrnutí
Enumerativní × symbolický přístup
Enumerativní – orientován na "control-flow"
Symbolický – orientován na "data-flow"
Výhody oproti testování
Není třeba zdrojový kód (aplikovatelné ve fázi návrhu).
Aplikovatelné na paralelní programy.
Výhody oproti statickým metodám
Metoda je úplná, tj. vždy dává přesné výsledky.
Možno verifikovat temporální vlastnosti.
Nevýhoda
Problém stavové exploze.
IV113 Úvod do validace a verifikace: Symbolický MC str. 31/31