Transcript formal verification(2).

1
Formal Verification(2)
경종민
[email protected]
2
Proof theory – sequent calculus(1/3)
•
Definition
– Sequent is a pair of finite set of formulas written as
Γ → Δ where Γ, Δ are a set of formulas, respectively.
•
Axiom
1. X → X ; identity
2. F → ; false holding
3. → T ; tautology
•
Sequent calculus rule
– Structural rule
•
•
•
If Γ1 ⊆ Γ2, Δ1 ⊆ Δ2
Premises: Γ1 → Δ1
Conclusion: Γ2 → Δ2
3
Proof theory – sequent calculus(2/3)
• Sequent calculus rule
– Negation rule1
• Premises: Γ → Δ, X
• Conclusion: Γ, ~X → Δ
– Negation rule2
• Premises: Γ, X → Δ
• Conclusion: Γ → Δ, ~X
– Implication rule
• Premises: Γ,X → Δ, Y
• Conclusion: Γ → Δ, X⇒Y
4
Proof theory – sequent calculus(3/3)
•
Ex) show A ⇒ (B ⇒ A)
1.
2.
3.
4.
5.
A→A
: Axiom 1
A, B → A
: Structural rule
A→B⇒A
: Implication rule
→ A⇒ (B ⇒ A) : Implication rule
A⇒ (B ⇒ A) is tautology : axiom 3
5
4. Temporal logic
• Why is TL necessary?
– Predicate logic is for static situation only, while
hardware often requires timing (temporal) evaluation
– Two choices;
• Explicit introduction of time variable t into predicate logic
• Generalization of predicate logic to encompass temporal
domain
• Kinds
– Linear temporal logic
– Branching temporal logic
6
History of TL
• Burstall, Pnueli and others proposed using temporal logic
(TL) for reasoning about programs (early 1970’s)
• Pnueli was the first to use TL for reasoning about
concurrency (1977)
• Clarke and Emerson in the early 1980’s developed a way to
automate temporal logic reasoning (CTL); Quielle and
Sifakis also gave a model checking algorithm around this
time
• Language containment approach to model checking
(Kurshan)
• Symbolic model checking (implicit representation of the
state space) – McMillan, 1987
7
Linear Temporal Logic
• Temporal operator
Classical Symbol Meaning
Symbol
○
X
Next
◇
F
Eventually (in the future)
□
G
Always (globally)
∪
U
Strong until
W
Weak until
8
Syntax of LTL
• If p is an atomic proposition, and f1 and f2 are LTL
formulas, then the set of LTL formulas consists of:
p
~f1, f1 & f2, f1 | f2, f1 ⇒ f2
X f1
G f1
F f1
f1 U f2 (f2 must become true in the future)
f1 W f2 (f2 may not become true permanently)
9
Example
Request
Acknowledge
• G((req ) ⇒ (req U ack))
– “whenever the request signal becomes true, it must
remain true until it is acknowledged”
• G((req ) ⇒ (F ack))
– “every request must eventually be acknowledged”
10
Example
• G((ack ) ⇒ (ack U (~req)))
– “whenever the acknowledgement signal becomes true, it
must remain true until the request signal returns to false”
• G((ack ) ⇒ (F (~req)))
– “it is always the case that the request signal will
eventually return to false after the request is
acknowledged”
• G((~req ) ⇒ (~req U ~ack))
– “whenever the request signal is false, it will remain false
until the acknowledgement signal is also false”
11
Example
• G((~req ) ⇒ F (~ack))
– “it is always the case that the acknowledgement signal
will eventually return to false after the request signal
returns to false”
• G((~ack ) ⇒ (~ack U req))
– “it is always the case that once false, the
acknowledgement signal will remain false until there is a
request”
• G((~ack ) ⇒ (F req))
– “whenever the acknowledgement signal is false, there
will eventually be a request”
12
Semantics of LTL
• In the satisfaction relation M ╞ F, M is a Kripke
structure, F is a property in temporal logic, and
we will define another ╞
• Kripke structure
– Let AP be a set of atomic propositions. A Kripke
structure M over AP is a four-tuple, M= (S, S0, R, L)
where
• S is a finite set of states.
• S0 ⊆ S is the set of initial states.
• R ⊆ S x S is a transition relation that must be ‘total’, that
is ∀s  S.∃s’.R(s, s’).
• L : S → 2AP is a function that labels each state with the set
of atomic propositions true in that state.
13
Path
• LTL formulas are evaluated relative to paths.
– Time function in predicate logic or higher order logic
formulation
• An LTL formula describes a set of paths for which
the formula holds.
• A path from a state s is an infinite sequence p =
s1s2s3 … such that ∀i.R(si, si+1).
– Use pi to denote the suffix of p starting at si.
14
Semantics of LTL
• M, p ╞ g means the LTL formula g holds on path
p = s1s2s3 … in the Kripke structure M= (S, S0,R,
L). The relation ╞ is defined inductively as follows:
M, p ╞ p iff p  L(s1) (where p is an atomic proposition)
M, p ╞ ~g iff M , p ╞ g
M, p ╞ g1 & g2 iff M, p ╞ g1 and M, p ╞ g2
M, p ╞ X g iff M, p2 ╞ g
M, p ╞ G g iff ∀i ≥ 1,M, pi ╞ g
M, p ╞ F g iff ∃i ≥ 1,M, pi ╞ g
M, p ╞ g1 U g2 iff ∃ i.i ≥ 1,M, pi ╞ g2 and ∀ j.1≤ j < i
⇒ M, pj ╞ g1
15
Limitations of LTL(why CTL?)
• An LTL formula g is satisfied in a state s of a
model M if g is satisfied on EVERY path starting at
s.
• How do we say there is some path where a
formula is true?
– For example, “from any state, there is always a way to
get to a state where p is true” is impossible to express
as an LTL formula.
– It is motivation of CTL
16
Computational Tree Logic(CTL)
• Same temporal operators of LTL are used.
• Additional two path quantifiers;
– A means ‘for all computation paths’
– E means ‘for some computation paths’
• In CTL, we talk about a formula being true of a
state rather than a path.
17
Syntax of CTL
• If p is an atomic proposition, and f1 and f2 are
CTL formulas, then the set of CTL formulas
consists of:
– p
– ~f1, f1 & f2, f1 | f2, f1 ⇒ f2
Every temporal operator must be preceded by a Path
Quantifier;
– AXf1, EXf1
– AGf1, EGf1
– AFf1, EFf1
– A[f1Uf2], E[f1Uf2]
18
Semantics of CTL
• CTL formulae are evaluated with respect to a
Kripke structure M= (S, S0,R, L) and a state s (p =
s1s2s3…)
M,s ╞
M,s ╞
M,s ╞
M,s ╞
M,p ╞
M,s ╞
M,s ╞
p iff p  L(s) (where p is an atomic proposition)
~f iff M,s ╞ f
f1 & f2 iff M,s╞ f1 and M,s╞ f2
f1 | f2 iff M,s╞ f1 or M,s╞ f2
f iff s is first state of p and M, s ╞ f
EX f iff ∃ path p from s such that M,p ╞ f
AX f iff ∀ path p from s such that M,p ╞ f
19
Semantics of CTL
M,s ╞ EF f iff ∃ path p from s, ∃ k ≥ 1 such that
M, pk ╞ f
M,s ╞ AF f iff ∀ paths p from s, ∃ k ≥ 1 such that
M, pk ╞ f
M,s ╞ EG f iff ∃ path p from s such that
∀ k ≥ 1, M, pk ╞ f
M,s ╞ AG f iff ∀ paths p from s such that
∀ k ≥ 1, M, pk ╞ f
M,s ╞ E[f1 U f2] iff ∃ paths p from s, ∃ k ≥ 1 such that
M, pk ╞ f2 and ∀j < k M, pj ╞ f1
M,s ╞ A[f1 U f2] iff ∀ paths p from s, ∃ k ≥ 1 such that
M, pk ╞ f2 and ∀j< k M, pj╞ f１
20
LTL vs CTL(CTL is not necessarily
more expressive than LTL)
• In LTL, we could write: FG
p, which means “on all
paths, there is some state
from which p will forever
hold”.
• There is no equivalent of
this in CTL. For example, in
the following model, FG p
holds, but AF(AG p) does
not:
p
~p
p
p
p
p
~p
~p
p
p
~p
p
p
~p
p
p
p
p
21
LTL vs CTL
• Note that all top-level LTL formulas can be
thought of as having the path quantifier A in front
of them.
• CTL is a branching time logic. LTL is a linear time
logic. In a branching time logic, there are path
quantifiers. In CTL, all the temporal operators
must be immediately preceded by a path
quantifiers. In LTL, we can have arbitrarily nested
temporal operators.
• An LTL formula is true/false relative to a path.
• A CTL formula is true/false relative to a state.
22
Model check methodology
Modify
Implementation
Counter
example
Analyzer
Spec
Not meet
Required property
(≈ Spec)
Meet
Verified
implementation
23
Model checking procedure
Kripke structure
Implementation
Initial
state (S0)
Parsing
Analyzing
I/O
Latch
Information
Parsing
Analyzing
Atomic
propositions
Required property
(≈ Spec)
Search state space
by traversing FSM
Reachable
states (S)
Transition
relation (R)
Labeling
Function (L)
24
How to perform model checking
• Start with Kripke structure, check all properties at
initial state(s)
– Apply atomic proposition to all states, build complex
properties from them.
• Popular algorithms
– Automata theoretic approach
• Spin (Bell Lab), Cospan (cadence)
– Explicit CTL model checking
• Murf (Stanford)
– Symbolic CTL model checking
• Cadence SMV, NuSMV,
25
Symbolic model checking
• Keeping states, transition relations
– 100 bits of internal state needs up to 100*2^100 bits
storage
• Using logical formula to represent set of states,
transition relations, atomic propositions
– Logical formula are represented using BDD for storage
reduction (compared to representation as ‘list’)
– Can handle hundreds of state variables
• Use the model checking algorithm over sets of
states.
• Operations in this algorithm are then represented
as operations on logical formulas.
26
What to verify with MC?
• Application-independent properties
– Completeness
– Consistency
– Absence of deadlock and livelock (unescapable from a
‘small’ set of states)
• Application-dependent properties
–
–
–
–
–
Liveness (“Some event must appear.”)
Safety
Pre/post conditions
Invariant
Comparison to specification
27
Example – BUS arbiter(1/5)
• Spec. of Arbiter
req1
gnt1
BUS
arbiter
req2
gnt2
req3
gnt3
BUS
master1
BUS
master2
BUS
master3
–
–
–
–
First request, first serve
No starvation (liveness)
Only one ‘gnt’ at a time (safety)
‘gnt’ must go high within 50
cycles (safety)
• Spec. of BUS master
– ‘req’ must stay high until the
BUS is released
– Hold BUS less than 10 cycles
– Must wait for ‘gnt’ at least 50
cycles
28
Example – BUS arbiter(2/5)
• Abstract model of BUS master
– Inputs of BUS arbiter are not actually random.
• Model checking may generate false negative (‘false alarm’)
with random inputs
– Use ‘non-deterministic value’($ND) for modeling nondeterministic behavior
~$ND
Idle
req1
BUS
gnt1 Master1
(abstract)
$ND
bad
$ND
$ND | counter = 10
counter = 50
Wait
req
req1= state == req | state == wait
Otherwise
gnt1
Otherwise
29
Example – BUS arbiter(3/5)
• Non-determinism
req1
BUS
gnt1 Master1
$ND1
(abstract)
– All combinations of $ND1, $ND2,
$ND3 make all possible transaction
conditions with valid spec.
• Temporal properties
BUS
arbiter
req2
BUS
gnt2 Master2
$ND2
• AG (req1 ⇒ AF (gnt1))
(abstract)
req3
BUS
gnt3 Master3
(abstract)
– No starvation
– Only one ‘gnt’ at a time
$ND3
• AG ~((gnt1 & gnt2) | (gnt2 & gnt3)
| (gnt3 & gnt1))
– ‘gnt’ must go high within 50 cycles.
• AG ( ‘state of bus master’ != bad)
30
Example – BUS arbiter(4/5)
• How to generate Kripke structure;
• Compute reachable states S and transition relation R
Initial state
($ND1, $ND2, $ND3)
S0
(0,0,0)
(0,0,1)(0,1,0)
Sa
(1,1,1)
Sb
Calculate next state by
using all combinations of
($ND1, $ND2, $ND3)
Sc
Every edge is
transition relation
R: {(S0, Sa), (S0, Sb), (Sa, Sc), …. }
31
Example – BUS arbiter(5/5)
• Compute a set of atomic propositions AP and labeling
function L
– AG (req1 ⇒ AF (gnt1))
• AP = {req1, gnt1} = { p1, p2 }
– AG ~((gnt1 & gnt2) | (gnt2 & gnt3) | (gnt3 & gnt1))
• AP = {~((gnt1 & gnt2) | (gnt2 & gnt3) | (gnt3 & gnt1))} = {p 3}
– ‘AG ( ‘state of bus master’ != bad)
• AP = { ‘state of bus master’ != bad } = {p4}
– L(S0) = {p3, p4}
– L(Sa) = …
• Then we have Kripke structure M and a set of temporal
properties
• Run model checking algorithm to check given properties
– Ex) M ╞ AG (p1 ⇒ AF (p2))
M ╞ AG (p3)
M ╞ AG (p4)
32
Available tools
• Equivalence checker
– FormalPro(Mentor), Formality(Synopsys), Design
VERIFIer(Avant!)
• Model checker
– VIS(Berkeley), CMV(Cadence), STeP (Stanford), Formal
Model Checker(Avant!)
• Theorem prover
– PVS(SRI)
33
Useful sites
• Glossary of first order logic
– http://www.earlham.edu/~peters/courses/logsys/glossar
y.htm
• SMV
– http://www-cad.eecs.berkeley.edu/~kenmcmil/
• Logic pattern (LTL, CTL, …)
– http://www.cis.ksu.edu/santos/spec-patterns/
• Formal method
– http://eis.jpl.nasa.gov/quality/Formal_Methods/
• Sugar - Language for describing temporal
properties
– http://www.haifa.il.ibm.com/projects/verification/sugar/