SPINPropertiesLTL Model CheckingLTL FormulaeLTL SemanticsSlide 6Slide 7Buchi AutomataSlide 9Slide 10Slide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20References1Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398SPINAn explicit state model checker2Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Properties•Safety properties–Something bad never happens–Properties of states•Liveness properties–Something good eventually happens–Properties of pathsReachability is sufficientWe need something more complex to check liveness properties3Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Liveness properties are expressed in LTL–Subset of CTL* of the form:•A fwhere f is a path formula which does not contain any quantifiers•The quantifier A is usually omitted.•G is substituted by (always)•F is substituted by (eventually)•X is (sometimes) substituted by (next)4Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Formulae•Always eventually p: pAGFp in CTL*AG(pFq) in CTL*•Fairness: ( p ) AG(p AFq) in CTLAG AF p in CTLA((GF p) ) in CTL*Can’t express it in CTL•Always after p there is eventually q: ( p ( q ) )5Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Semantics•The semantics is the one defined by CTL*•Given an infinite execution trace = s0s1… 1221212121210|).(0|)(.0||).(0||).(0[]|||)|()|(|)|()|(|)(|jiiiijiUiispp6Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•An LTL formula defines a set of traces•Check trace containment–Traces of the program must be a subset of the traces defined by the LTL formula–If a trace of the program is not in such set•It violates the property•It is a counterexample–LTL formulas are universally quantified7Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Trace containment can be turned into emptiness checking–Negate the formula corresponds to complement the defined set:–Subset corresponds to empty intersection:)()(setset0 BABA8Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automata•An LTL formula defines a set of infinite traces•Define an automaton which accepts those traces•Buchi automata are automata which accept sets of infinite traces9Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automata•A Buchi automaton is 4-tuple <S,I,,F>:–S is a set of states–I S is a set of initial states: S 2S is a transition relation–F S is a set of accepting states•We can define a labeling of the states:: S 2L is a labeling functionwhere L is the set of literals.10Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automatas0s1s2S = { s0, s1, s2 }I = { s0 } = { (s0, {s0, s1}), (s1, {s2}), (s2, {s2}) }F = { s2 } = { (s0, {a}), (s1, {b}), (s2, {}) }a b true11Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automata•An infinite trace = s0s1… is accepted by a Buchi automaton iff:–s0 I i ≥ 0: si+1 (si) i ≥ 0: j > i: sj F12Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Let’s assume each state is labeled with a complete set of literals–Each proposition or its negation is present–Labeling function •A Buchi automaton accepts a trace = S0S1…so I: (S0) (so) i ≥ 0: si+1 (si). (Si+1) (si+1) i ≥ 0: j > i: sj F13Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automatas0s1s2batrue = a a a a a b b b a c c c c … = a a a c a b b b a b a b b …14Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automata•Some properties:–Not all non-deterministic Buchi automata have an equivalent deterministic Buchi automata–Not all Buchi automata correspond to an LTL formula–Every LTL formula corresponds to a Buchi automaton–Set of Buchi automata closed until complement, union, intersection, and composition15Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automatabatrues0s1s2a U bWhat LTL formula does this Buchi automatoncorresponds to (if any)?16Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Generate a Buchi automaton for the negation of the LTL formula to check•Compose the Buchi automaton with the automaton corresponding to the system•Check emptiness17Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Composition:–At each step alternate transitions from the system and the Buchi automaton•Emptiness:–To have an accepted trace:•There must be a cycle•The cycle must contain an accepting state18Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checking•Cycle detection–Nested DFS•Start a second DFS•Match the start state in the second DFS–Cycle!•Second DFS needs to be started at each state?–Accepting states only will suffice•Each second DFS is independent–If started in post-order states need to be visited at most once in the second DFS searches19Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checkingprocedure DFS(s) visited = visited {s} for each successor s’ of s if s’ visited then DFS(s’) if s’ is accepting then DFS2(s’, s’) end if end if end forend procedure20Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checkingprocedure DFS2(s, seed) visited2 = visited2 {s} for each successor s’ of s if s’ = seed then return “Cycle Detect”; end if if s’ visited2 then DFS2(s’, seed) end if end forend procedure21Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398References•http://spinroot.com/ •Design and Validation of Computer Protocols by Gerard Holzmann•The Spin Model Checker by Gerard Holzmann•An automata-theoretic approach to automatic program verification, by Moshe Y. Vardi, and Pierre Wolper •An analysis of bitstate hashing, by G.J. Holzmann •An
View Full Document