Introduction to Spin and PromelaSagar ChakiCMURoadmapn Historical perspectiven Overview of Spinn Overview of Promelan Simulation with Spinn Overview of LTLn Verification with SpinPart IIIOverview of LTLBasic conceptsn Set of propositions: Pn P = {a,b,c}n Infinite trace τ over Pn t0,t1,t2, …n tisubset of P for i  0n τidenotes infinite trace ti,ti+1, …n {b},{a,c},{},{a,b,c},{a}, …n Set of all infinite traces over P: Γ(P)LTL syntaxn φ := p proposition| true| false| (φ)| φ binop φ| unop φLTL syntaxn unop := [] always (G)| <> eventually (F)| X next time| ! logical negationn binop := U strong until| && logical AND| || logical OR| -> implication| <-> equivalenceLTL semanticsn An infinite trace τ (over P) either satisfies or does not satisfy an LTL formula φ (over P)n Satisfaction denoted by τ ² φLTL semanticsn Given an infinite trace τ = t0,t1,t2, … and a LTL formula φ we can decide if τ ² φ depending on the structure of φn τ ² p iff p belongs to t0n Always τ ² truen Never τ ² falsen τ ² (φ) iff τ ² φLTL semanticsn τ ² [] φ iff τi² φ forall i  0n τ ² <> φ iff exists i  0 s.t. τi² φn τ ² X φ iff τ1² φn τ ² !φ iff NOT(τ ² φ)n τ ² φ1U φ2iff exists i  0 s.t. τj² φ1for 0  j < i and τi² φ2LTL semanticsn τ ² φ1&& φ2iff τ ² φ1AND τ ² φ2n τ ² φ1|| φ2iff τ ² φ1OR τ ² φ2n τ ² φ1-> φ2iff τ ² φ1IMPLIES τ ² φ2n τ ² φ1<-> φ2iff τ ² φ1IFF τ ² φ2LTL semanticsn An LTL formula can also be looked at as the set of infinite traces that satisfy itn Note the striking similarity with the case of regular expressions and finite strings over an alphabet Σn If S is the set of traces that satisfy φ then Γ(P)\S is the set of traces that satisfy !φExamplesn {a},{b},{a},{b}, …n [](a -> Xb) [](a <-> Xb)n [](b -> Xa) [](b <-> Xa)n [](a -> (b U a))n [](a -> (a U b))Things to remembern Every LTL formula represents the set of infinite traces which satisfy itBuchi automatan Recall the similarity of LTL with regular expressionsn Regular languages are accepted by finite automatan Are there automata for LTLn Turns out there aren They are called Buchi automataBuchi automatan Fix an alphabet Σn Buchi automaton is a 4-tuple : <Q,I,δ,F>n Q : set of statesn I : initial staten δ : transition relation: subset of QX Σ XQn F : set of accepting statesn In our case Σ is 2PExampleS0 S1aI = S0 , F = {S0}bBuchi automatan A run is an infinite sequence of state s0,s1,s2, … such thatn s0= In Exists aiº Σ s.t. (si,ai,si+1) º δ for i  0n A run is an accepting run iff it visits some accepting state infinitely oftenBuchi automatan Given a run σ = s0,s1,s2, …a trace τ = τ0,τ1,τ2, …is said to correspond to σ iff(si,τi,si+1) º δ for i  0n The language of a Buchi automaton is the set of traces corresponding to its accepting runsn LTL also corresponds to a set of tracesExamplen Traces : {{a},{b},{a},{b},…}S0 S1aI = S0 , F = {S0}bCute resultsn BA are closed under complementationn For every Buchi automaton A there exists another Buchi automaton B such that the language of A is the complement of the language of Bn Here complement means set difference from Γ(P)Cute resultsn BA are closed under intersection and unionn Checking if the language of a Buchi automaton is empty is decidablen Can check if the langauges of two Buchi automata have a non-empty intersectionCute resultsn Buchi automata are not always determinisablen There exists a non-deterministic Buchiautomaton A such that there is no deterministic Buchi automaton with the same language as An Non-deterministic means some states have multiple outgoing transitions with same labelCute resultsn The set of languages accepted by Buchi automata is called the set of ω-regular languagesn This is a strict superset of LTLn Every LTL corresponds to some BAn There exists a BA whose language does not correspond to any LTL formulaThings to remembern Every LTL formula represents the set of infinite traces which satisfy itn Every LTL formula has a corresponding Buchi automatonKripke structuren Is a 4-tuple : <S,I,δ,L>n S : set of statesn I : initial staten δ : transition relation: subset of S X Sn L : labeling function : S -> 2PComputations and Tracesn A computation is an infinite sequence of states s0,s1,s2, …n s0= In (si,si+1) º δ for i  0n Given a computation s0,s1,s2, … the corresponding trace isL(s0), L(s1), L(s2), …Kripke and Buchin Kripke looks different from Buchin Labels are on states not transitionsn No accepting statesn Nevertheless …n For every Kripke structure K there exists a Buchi automaton which accepts exactly the set of traces corresponding to computations of KKripke to Buchia bcS0 S1S2I = S0Kripke to BuchiS0 S1S2abcKripke to BuchiS0 S1S2abcS3aI = S3, F = {S0,S1,S2,S3}Things to remembern Every LTL formula represents the set of infinite traces which satisfy itn Every LTL formula has a corresponding Buchi automatonn Every Kripke structure has a corresponding Buchi automatonWhat do we really want?n Kripke (M) ² LTL (φ)n Traces of M contained in traces of φn Language of Buchi of M contained in language of Buchi of φn Language of Buchi of M has empty intersection with language of Buchi of !φn This is decidableLTL model checkingn Two ways to do itn Convert Kripke to Buchin Convert claim (LTL) to Buchin Check language inclusionORn Convert ~Claim (LTL) to Buchin Check empty intersectionWhat Spin doesn Checks non-empty intersectionn Requires very little space in best casen Works directly with Promelan No conversion to Kripke or Buchin Must provide Spin with negation of property you want to proveTime for example 5Referencesn http://cm.bell-labs.com/cm/cs/what/spin/n http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.htmln