1Carnegie 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 livenessproperties3Carnegie 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 q (next)4Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Formulae• Always eventually p:  ¡ pAGFp in CTL*AG(poFq) in CTL*• Fairness:(  ¡ p ) o MAG(p oAFq) in CTLAG AF p in CTLA((GF p) o M) in CTL*Can’t express it in CTL• Always after p there is eventually q:  ( p o ( ¡ q ) )5Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Semantics• The semantics is the one defined by CTL*• Given an infinite execution trace V = s0s1…  1221212121210|).(0|)(.0||).(0||).(0[]|||)|()|(|)|()|(|)(|IVIVIIVIVIVIVIVIVIVIVIVIIVIVIVIIVV d t t ! t z      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:)()( II  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,G,F>:– S is a set of states– I  S is a set of initial states– G: S o 2Sis a transition relation– F  S is a set of accepting states• We can define a labeling of the states:– O: S o 2Lis a labeling functionwhere L is the set of literals.10Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automatas0s1s2S = { s0, s1, s2 }I = { s0 }G = { (s0, {s0, s1}), (s1, {s2}), (s2, {s2}) }F = { s2}O = { (s0, {a}), (s1, {b}), (s2, {}) }a b true11Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automata• An infinite trace V = s0s1… is accepted by a Buchi automaton iff:– s0  I–  i  0: si+1 G(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 V = S0S1…– so I: /(S0)  O(so)–  i  0:  si+1 G(si). /(Si+1)  O(si+1)–  i  0:  j > i: sj F13Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Buchi Automatas0s1s2batrueV = a a a a a b b b a c c c c …V = 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 Buchiautomaton– 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 sif s’  visited thenDFS(s’)if s’ is accepting thenDFS2(s’, s’)end ifend ifend forend procedure20Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398LTL Model Checkingprocedure DFS2(s, seed)visited2 = visited2  {s}for each successor s’ of sif s’ = seed thenreturn “Cycle Detect”;end ifif s’  visited2 thenDFS2(s’, seed)end ifend 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 Improvement in Formal Verification, by G.J. Holzmannand D. Peled• Simple on-the-fly automatic verification of linear temporal logic, by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper• A Minimized automaton representation of reachable states, by A. Puri and G.J.