Approaches to Verification
1
Approaches to Verification
Can be classified as follows:
• Proof-based versus model-based.
• Degree of automation.
• Full- versus property-verification.
• Intended domain of application.
• Pre- versus post-development.
2
Model Checking
3
Safety and Liveness
• Safety properties
– Invariants, deadlocks, reachability, etc.
– Can be checked on finite traces
– “something bad never happens”
• Liveness Properties
– Fairness, response, etc.
– Infinite traces
– “something good will eventually happen”
4
Model Checking Process
[ Adapted from www.lix.polytechnique.fr/comete/seminar/1-ModelChecking.ppt]
Model
(System Requirements) Answer:
Model
Yes, if model satisfies
Checker specification
Specification M╞ φ
Counterexample, otherwise
(System Property)
For increasing our confidence in the correctness of the model:
Verification: The model satisfies important system properties
Debugging: Study counter-examples, pinpoint the source of the error, correct
the model, and try again
5
Mutual Exclusion Example
Model
(System Requirements)
The Model (Willem Visser, http://ase.arc.nasa.gov/visser/ASE2002TutSoftwareMC-fonts.ppt)
• Two process mutual exclusion with shared semaphore
• Each process has three states
• Non-critical (N)
• Trying (T)
• Critical (C)
• Semaphore can be available (S0) or taken (S1)
• Initially both processes are in the Non-critical state and
the semaphore is available --- N1 N2 S0
N1 T1 N2 T2
T1 S0 C1 S1 || T2 S0 C2 S1
C1 N1 S0 C2 N2 S0
6
Mutual Exclusion Example
Model
(System Requirements)
•Initially both processes are in the Non-critical state and the semaphore is available --- N1 N2 S0
N1 T1 N2 T2
T1 S0 C1 S1 || T2 S0 C2 S1
C1 N1 S0 C2 N2 S0
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
7
C1T2S1 T1C2S1
Mutual Exclusion Example
Specification
(System Property)
Specification – Desirable Property
No matter where you are there is
always a way to get to the initial state
K ╞ AG EF (N1 N2 S0)
Kripke structure CTL (Computation Tree Logic)
M╞ φ
8
Mutual Exclusion Example
Model N1N2S0
(System Requirements)
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
C1T2S1 T1C2S1
Model Answer: Yes
Checker
Specification M╞ φ
(System Property)
K ╞ AG EF (N1 N2 S0) 9
Mutual Exclusion Example
Answer: Yes
A Proof: For All possible behaviors
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
C1T2S1 T1C2S1
10
Mutual Exclusion Example
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
C1T2S1 T1C2S1
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
11
C1T2S1 T1C2S1
Mutual Exclusion Example
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
C1T2S1 T1C2S1
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
12
C1T2S1 T1C2S1
Mutual Exclusion Example
Specification – Desirable Property
No matter where you are there is
no way to get to the initial state
K ╞ AG EF (N1 N2 S0)
⌐
13
Mutual Exclusion Example
Answer: No N1N2S0
Counterexample
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
C1T2S1 T1C2S1
N1N2S0
T1N2S0 N1T2S0
C1N2S1 T1T2S0 N1C2S1
14
C1T2S1 T1C2S1
Defining Models
Model
(System Requirements)
Kripke Structure
K = < S ,P, R > (M = < S ,P, R, L (, {s0})>) (s0S - initial state)
- S: the set of possible global states
- P: a non-empty set of atomic propositions {p1, . . ., pk} which express atomic
properties of the global states, e.g., being an initial state, being an accepting state,
or that a particular variable has a special value.
- R⊆ S × S: a transition relation s.t. R(s,s') if s to s' is a possible atomic transition
- L: S → 2P: a labeling function which defines which propositions hold in which states.
State explosion problem: The size of S is often exponential in |requirements/design
Model checking problem: A model checker checks whether a system, interpreted
as an automaton, is a (Kripke) model of a property
expressed as a temporal logic formula.
K |= φ
15
Defining Models
For a complex real-life control systems
Extended Finite State Machine (EFSM)
- FSM with a way to
-modularize the requirements to view them at different levels of detail
-combine requirements (or design) of components
- state variables and facilities in guards on transitions.
16
Defining Specifications
Specification
(System Property)
• Temporal Logic
– Express properties of event orderings in time
– e.g. “Always” when a packet is sent it will “Eventually” be received
Linear Time Branching Time
– Every moment has a unique – Every moment has several
successor successors
– Infinite sequences (words) – Infinite tree
– Linear Time Temporal Logic (LTL) – Computation Tree Logic (CTL)
17
Branching Temporal Logic (BTL)
Computation Tree Logic (CTL) Syntax http://www.cs.ucl.ac.uk/staff/J.Bowen/GS03/w3_l1_ctl_notes.pdf
A CTL wff ϕ is (p is an atomic property/proposition):
ϕ ::= ⊤ | ⊥ | p | ￢ φ | φ ∧ ψ | φ ∨ ψ | φ → ψ | AX φ | EX φ |
AF φ | EF φ | AG φ | EG φ | A[φU ψ] | E[φU ψ]
R (‘‘Release’’)
EX φ true in current state if formula φ is true in at least one of the next states
E φUψ true in current state if formula φ is true until ψ becomes true in some path beginning
in current state that satisfies the formula φ
EF φ true in current state if there exists some state in some path beginning in current state
that satisfies the formula φ
EG φ true in current state if every state in some path beginning in current state that
satisfies the formula φ
AX φ true in current state if formula φ is true in every one of the next states
A φUψ true in current state if formula φ is true until ψ becomes true in every path beginning
in current state that satisfies the formula φ
AF φ true in current state if there exists some state in every path beginning in current state
that satisfies the formula φ
AG φ true in current state if every state in every path beginning in current state satisfies the
formula φ 18
Branching Temporal Logic (BTL)
Computation Tree Logic (CTL) Semantics
Let M = (S,R, L) be a transition system (or a Kripke structure, also called a
model for CTL).
Let ϕ be a CTL formula and s ∈ S.
Then M, s |= ϕ is defined inductively on the structure of ϕ, as follows:
M,s |= ⊤
M,s |≠ ⊥
M,s |= p iff p ∈ L(s)
M,s |= ￢ϕ iff M,s |≠ ϕ
M,s |= ϕ ∧ ψ iff M,s |= ϕ and M,s |= ψ
M,s |= ϕ ∨ ψ iff M,s |= ϕ or M,s |= ψ
19
Branching Temporal Logic (BTL)
Computation Tree Logic (CTL) Semantics
M,s |= AXϕ iff ∀s’ s.t. sRs’, M,s’ |= ϕ
M,s |= EXϕ iff ∃s’ s.t. sRs’ and M,s’ |= ϕ
M,s |= AGϕ iff for all paths (s, s2, s3, s4, . . .) s.t. siRsi+1
and for all i, it is the case that M,si |= ϕ
M,s |= EGϕ iff there is a path (s, s2, s3, s4, . . .) s.t. siRsi+1
and for all i it is the case that M,si |= ϕ
M,s |= AFϕ iff for all paths (s, s2, s3, s4, . . .) s.t. siRsi+1,
there is a state si s.t. M,si |= ϕ
M,s |= EFϕ iff there is a path (s, s2, s3, s4, . . .) s.t. siRsi+1,
and there is a state si s.t. M,si |= ϕ
M,s |= A[ϕUψ] iff for all paths (s, s2, s3, s4, . . .) s.t. siRsi+1
there is a state sj s.t. M,sj |= ψ and M,si |= ψ for all i < j.
M,s |= E[ϕUψ] iff there exists a path (s, s2, s3, s4, . . .) s.t. siRsi+1
and there is a state sj s.t. M,sj |= ψ and M,si |= ϕ for all i < j.
M |= p if M, s0 |= p
20
Branching Temporal Logic (BTL)
Equivalences between CTL formulas
AXϕ ≡ ￢EX￢ϕ
AGϕ ≡ ￢EF￢ϕ
AFϕ ≡ ￢EG￢ϕ
EFϕ ≡ E[⊤Uϕ]
Therefore, only three operators are required to express all the remaining:
EX,EG,EU (this is called an adequate set of operators).
21
Branching Temporal Logic (BTL)
Specification patterns
Two example of requirements patterns:
• Liveness: “Something good will eventually happen”.
E.g.: “Whenever any process requests to enter its critical section,
it will eventually be permitted to do so”.
In CTL: AG(request → AF(critical))
• Safety: “Nothing bad will happen”.
E.g: “Only one process is in its critical section at any time”.
In CTL (with 2 processes only): AG(￢(critical1 ∧ critical2))
More examples:
1. “From any state it is possible to get a reset state”:
AGEF(reset)
2. “Event p precedes s and t on all computation paths” (try to encode the negation of
this):
The negation: there exists in the future a state in which p follows
s ∧ t: EF((s ∧ t) → EF(p)).
Its negation: ￢EF((s ∧ t) → EF(p)) ≡ AG(￢((s ∧ t) → EF(p)))
3. “On all computation paths, after p, q is never true”: AG(p → (￢EF(q)))
22
Defining Specifications
Intuition for CTL formulae which are satisfied at state s0
23
Issues
Temporal logic: (heavy) can be hard to work with
Translations of requirements models to the input language of model checking
engines often not straightforward.
If no bugs are detected, does this mean that we have achieved verification, or just
got too crude a model or property?
Number of states typically grows exponentially in the number of processes:
cannot be efficiently checked, due to state space explosion
Counter-examples: do not mean anything to the stakeholders; need to be translated
back into the original modeling language.
Deals only with state-oriented behavioral requirements models
24
Appendix: Microwave Oven Example
Model http://pi.informatik.uni-siegen.de/niere/lehre/SS04/SeminarFinal/6_sun/Folien.pdf
M = (S, S0, R, L)
• S = (S1, S2, S3, S4)
• S1 is the initial state
• R = ({S1, S2} {S2, S1}, {S1, S4}, {S4, S2}, {S2, S3}, {S3, S2}, {S3, S3}
• L (S1) = {¬close, ¬ start, ¬ cooking}
L (S2) = {close, ¬ start, ¬ cooking}
L (S3) = {close, start, cooking}
L (S4) = {¬close, start, ¬ cooking}
Specification
1. AG (start AF cooking)
2. AG ((close ∧ start) AF cooking)
25
Appendix: Microwave Oven Example
M = (S, S0, R, L)
http://pi.informatik.uni-siegen.de/niere/lehre/SS04/SeminarFinal/6_sun/Folien.pdf
• S = (S1, S2, S3, S4)
• S1 is the initial state
• R = ({S1, S2} {S2, S1}, {S1, S4}, {S4, S2}, {S2, S3}, {S3, S2}, {S3, S3}
• L (S1) = {¬close, ¬ start, ¬ cooking}
L (S2) = {close, ¬ start, ¬ cooking}
L (S3) = {close, start, cooking}
L (S4) = {¬close, start, ¬ cooking}
1. AG (start AF cooking)
1) Change formal to ¬EF (start ∧ EG ¬ cooking))
2) From simple partial formulas to the more complicated formulas, until all of the
formulas are true.
• S (start) = {S3, S4}
• S (¬cooking) = {S1, S2, S4}
• S (EG ¬ cooking) = {S1, S2, S4} (all conditions lie on a path)
• S (start ∧ EG ¬ cooking) = {S4}
• S (EF (start Ù EG ¬ cooking)) = {S1, S2, S3, S4} (can be followed with S4)
• S (¬ (EF (start ∧ EG ¬ cooking))) = {}
2. AG ((close ∧ start) AF cooking)
1) change formal to ¬ EF(close ∧ start ∧ EG ¬ cooking)
2) Now the algorithm can be applied to the formula
Model
• S (close)= {S2, S3} Checker
• S (start)= {S3, S4} M╞ φ
• S (¬ cooking) = {S1, S2, S4}
• S (EG ¬ cooking) = {S1, S2, S4}
• S (close ∧ start ∧ EG ¬ cooking) = {}
• S (EF (close ∧ start ∧ EG ¬ cooking) = {} 26
• S (¬ (EF (close ∧ start v EG ¬ cooking)) = {S1, S2, S3, S4}
