WIXLIB

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Statements(2)Statements areseparated by asemi-colon: “;”. The skip statement is always executable.– “does nothing”, only changes process’ process counter A run statement is only executable if a new process can becreated (remember: the number of processes is bounded). A printf statement is always executable (but is notevaluated during verification, of course).int x;proctype Aap(){int y 1;skip;run Noot();x 2;x 2 && y 1;skip;}Thursday 11-Apr-2002Executable if Noot canbe created Can only become executableif a some other processmakes x greater than 2.Theo C. Ruys - SPIN Beginners' TutorialStatements23(3) assert( expr );– The assert-statement is always executable.– If expr evaluates to zero, SPIN will exit with an error, asthe expr “has been violated”.– The assert-statement is often used within Promela models,to check whether certain properties are valid in a state.proctype monitor() {assert(n 3);}proctype receiver() {.toReceiver ? msg;assert(msg ! ERROR);.}Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20022412

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Interleaving Semantics Promela processes execute concurrently. Non-deterministic scheduling of the processes. Processes are interleaved (statements of differentprocesses do not occur at the same time).– exception: rendez-vous communication. All statements are atomic; each statement is executedwithout interleaving with other processes. Each process may have several different possible actionsenabled at each point of execution.– only one choice is made, non-deterministically. randomlyThursday 11-Apr-2002 deadlocks safety properties liveness propertiesTheo C. Ruys - SPIN Beginners' Tutorial(X)SPIN ArchitectureSPINϕ25M melamodel MXspinediting windowsimulation optionsverification optionsMSC simulation windowThursday 11-Apr-2002spin.exeVerifierGeneratorC programcounterexamplefalsecheckerpan.exe Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 2002pan.*2613

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Xspin in a nutshell Xspin allows the user to– edit Promela models ( syntax check)– simulate Promela models random interactive guided– verify Promela models exhaustive bitstate hashing modewith dialog boxes to setvarious options and directivesto tune the verification process– additional features Xspin suggest abstractions to a Promela model (slicing)Xspin can draw automata for each processLTL property managerHelp system (with verification/simulation guidelines)Thursday 11-Apr-2002DEMOTheo C. Ruys - SPIN Beginners' TutorialMutual Exclusionbit flag;byte mutex;27WRONG!(1)/* signal entering/leaving the section *//* # procs in the critical section.*/proctype P(bit i) {flag ! 1;models:flag 1;while (flag 1) /* wait */;mutex ;printf("MSC: P(%d) has entered section.\n", i);mutex--;flag 0;Problem: assertion violation!}Both processes can pass theproctype monitor() {flag ! 1 “at the same time”,assert(mutex ! 2);i.e. before flag is set to 1.}init {atomic { run P(0); run P(1); run monitor(); }}starts two instances of process PThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20022814

Theo C. Ruys - SPIN Beginners' TutorialDEMOversion: Friday, 13 September 2002Mutual Exclusionbit x, y;byte mutex;WRONG!(2)/* signal entering/leaving the section/* # of procs in the critical section.*/*/active proctype B() {y 1;x 0;mutex ;mutex--;y 0;}active proctype A() {x 1;Process A waits fory 0;process B to end.mutex ;mutex--;x 0;}active proctype monitor() {assert(mutex ! 2);}Problem: invalid-end-state!Both processes can pass executex 1 and y 1 “at the same time”,and will then be waiting for each other.Thursday 11-Apr-2002DEMOTheo C. Ruys - SPIN Beginners' TutorialMutual Exclusionbit x, y;byte mutex;byte turn;29Dekker [1962](3)/* signal entering/leaving the section/* # of procs in the critical section./* who's turn is it?active proctype A() {x 1;turn B TURN;y 0 (turn A TURN);mutex ;mutex--;Can be generalisedx 0;to a single process.}active proctype monitor() {assert(mutex ! 2);}Thursday 11-Apr-2002*/*/*/active proctype B() {y 1;turn A TURN;x 0 (turn B TURN);mutex ;mutex--;y 0;}First “software-only” solution to themutex problem (for two processes).Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20023015

Theo C. Ruys - SPIN Beginners' TutorialDEMOversion: Friday, 13 September 2002Mutual Exclusionbyte turn[2];byte mutex;Bakery(4)/* who’s turn is it?*//* # procs in critical section */proctype P(bit i) {Problem (in Promela/SPIN):doturn[i] will overrun after 255.:: turn[i] 1;turn[i] turn[1-i] 1;(turn[1-i] 0) (turn[i] turn[1-i]);mutex ;mutex--;turn[i] 0;More mutual exclusion algorithmsodin (good-old) [Ben-Ari 1990].}proctype monitor() { assert(mutex ! 2); }init { atomic {run P(0); run P(1); run monitor()}}Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorialif-statement(1)31inspired by:Dijkstra’s guardedcommand languageif:: choice1 - stat1.1; stat1.2; stat1.3; :: choice2 - stat2.1; stat2.2; stat2.3; :: :: choicen - statn.1; statn.2; statn.3; fi; If there is at least one choicei (guard) executable, the ifstatement is executable and SPIN non-deterministicallychooses one of the executable choices. If no choicei is executable, the if-statement is blocked. The operator “- ” is equivalent to “;”. By convention, it is usedwithin if-statements to separate the guards from thestatements that follow the guards.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20023216

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002if-statementif::::::::fi(n % 2 ! 0) - n 1(n 0)- n n-2(n % 3 0) - n 3else- skipskipskipskipskip- - - - The else guard becomesexecutable if none of theother guards is executable.non-deterministic branchinggive n a random valueif::::::::fi(2)n 0n 1n 2n 3skips are redundant, because assignmentsare themselves always executable.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorialdo-statement33(1)do:: choice1 - stat1.1; stat1.2; stat1.3; :: choice2 - stat2.1; stat2.2; stat2.3; :: :: choicen - statn.1; statn.2; statn.3; od; With respect to the choices, a do-statement behaves in thesame way as an if-statement. However, instead of ending the statement at the end of thechoosen list of statements, a do-statement repeats the choiceselection. The (always executable) break statement exits a do-loopstatement and transfers control to the end of the loop.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20023417

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002do-statement(2)if- and do-statementsare ordinary Promelastatements; so they canbe nested. Example – modelling a traffic lightmtype { RED, YELLOW, GREEN } ;mtype (message type) models enumerations in Promelaactive proctype TrafficLight() {byte state GREEN;do:: (state GREEN) - state YELLOW;:: (state YELLOW) - state RED;:: (state RED)- state GREEN;od;}Note: this do-loop does not containany non-deterministic choice.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' MSGMSGs2r?MSGACKr2s!ACKr2s?ACK! is sending? is receivingThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20023618

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Communication(2) Communication between processes is via channels:– message passing– rendez-vous synchronisation (handshake)also called:queue or buffer Both are defined as channels:chan name [ dim ] of { t1 , t2 , tn };name ofthe channeltype of the elements that will betransmitted over the channelnumber of elements in the channeldim 0 is special case: rendez-vouschan c [1] of {bit};chan toR [2] of {mtype, bit};chan line[2] [1] of {mtype, Record};Thursday 11-Apr-2002array ofchannelsTheo C. Ruys - SPIN Beginners' TutorialCommunication37(3) channel FIFO-buffer (for dim 0)!Sending - putting a message into a channelch ! expr1 , expr2 , exprn ; The values of expri should correspond with the types of thechannel declaration. A send-statement is executable if the channel is not full.? Receiving - getting a message out of a channelch ? var1 , var2 , varn ; var const can bemixedmessage passing If the channel is not empty, the message is fetched from the channeland the individual parts of the message are stored into the vari s.ch ? const1 , const2 , constn ; message testing If the channel is not empty and the message at the front of thechannel evaluates to the individual consti , the statement isexecutable and the message is removed from the channel.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20023819

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Communication(4) Rendez-vous communication dim 0The number of elements in the channel is now zero.– If send ch! is enabled and if there is a correspondingreceive ch? that can be executed simultaneously and theconstants match, then both statements are enabled.– Both statements will “handshake” and togethertake the transition. Example:chan ch [0] of {bit, byte};– P wants to doch ! 1, 3 7– Q wants to doch ? 1, x– Then after the communication, x will have the value 10.Thursday 11-Apr-2002DEMOTheo C. Ruys - SPIN Beginners' TutorialAlternating Bit Protocol39(1) Alternating Bit Protocol– To every message, the sender adds a bit.– The receiver acknowledges each message by sendingthe received bit back.– To receiver only excepts messages with a bit that itexcepted to receive.– If the sender is sure that the receiver has correctlyreceived the previous message, it sends a newmessage and it alternates the accompanying bit.Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20024020

Theo C. Ruys - SPIN Beginners' TutorialDEMOversion: Friday, 13 September 2002Alternating Bit Protocolchannellength of 2chan toS [2] of {mtype, bit};chan toR [2] of {mtype, bit};proctype Receiver(chan in, out){bit recvbit;do:: in ? MSG(recvbit) - out ! ACK(recvbit);od}mtype {MSG, ACK};proctype Sender(chan in, out){bit sendbit, recvbit;do:: out ! MSG, sendbit - in ? ACK, recvbit;if:: recvbit sendbit - sendbit 1-sendbit:: elsefiod}Thursday 11-Apr-2002(2)init{run Sender(toS, toR);run Receiver(toR, toS);}Alternative notation:ch ! MSG(par1, )ch ? MSG(par1, )Theo C. Ruys - SPIN Beginners' Tutorial41[Ruys & Brinksma 1998]Cookie: “hippies” problemGermany.5.10.20 60 min?.Hollandholescoffeeshop25 2 persThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20024221

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002[Ruys & Brinksma 1998]Cookie: soldiers problemunsafe5 60 min?safe10 20 25 2 persThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorial43Advanced SPIN Towards effective modelling in Promela– Some left-over Promela statements– Properties that can be verified with SPIN– Introduction to SPIN validation algorithms– SPIN’s reduction algorithms– Extreme modelling: the “art of modelling”– Beyond Xspin: managing the verification trajectory– Concluding remarks– SummaryThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20024422

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002Basic SPINPromela Model A Promela model consist of:mtype, typedefs,constants– type declarationschan ch [dim] of {type, }asynchronous: dim 0rendez-vous: dim 0– channel declarations– global variable declarations– process declarations– [init process]can be accessedby all processesbehaviour of the processes:local variables statementsinitialises variables andstarts processesThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialPromela statementsalways executableskip45Basic SPINare either executableor blockedassert( expr ) always executableexpressionexecutable if not zeroassignmentalways executableifexecutable if at least one guard is executabledoexecutable if at least one guard is executablebreakalways executable (exits do-statement)send (ch!)executable if channel ch is not fullreceive (ch?)executable if channel ch is not emptyThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20024623

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002atomicatomic { stat1; stat2; . statn }– can be used to group statements into an atomic sequence;all statements are executed in a single step(no interleaving with statements of other processes)no pure atomicity– is executable if stat1 is executable– if a stati (with i 1) is blocked, the “atomicity token” is(temporarily) lost and other processes may do a step (Hardware) solution to the mutual exclusion problem:proctype P(bit i) {atomic {flag ! 1; flag 1; }mutex ;mutex--;flag 0;}Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorial47d stepd step { stat1; stat2; . statn }– more efficient version of atomic: no intermediate states aregenerated and stored– may only contain deterministic steps– it is a run-time error if stati (i 1) blocks.– d step is especiallyuseful to performintermediate computationsin a single transition::Rout?i(v) - d step {k ;e[k].ind i;e[k].val v;i 0; v 0 ;} atomic and d step can be used to lower the number ofstates of the modelThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20024824

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002No atomicityproctype P1() { t1a; t1b; t1c }proctype P2() { t2a; t2b; t2c }init { run P1(); run P2() }P1P200t1at1a (0,1)t2bt1c (2,0) t2at1b (1,1)t2b t1a (0,2)(3,0)t2ct2a t1c (2,1)t2b t1b (1,2)t2c t1a (0,3)(3,1)t2b t1c (2,2)t2c t1b (1,3)(3,2)t2c t1c (2,3)1t1bt2b22t1ct2c3t2at1b (1,0) t2at2a1(0,0)t1a3(3,3)Not completely correct as eachprocess has an implicit end-transition Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorialatomicproctype P1() { atomic {t1a; t1b; t1c} }proctype P2() { t2a; t2b; t2c }init { run P1(); run P2() }It is as if P1 has only one transition (2,2)(3,2)If one of P1’s transitionsblocks, these transitionsmay get executed(0,3)(1,3)(2,3)(3,3)Thursday 11-Apr-200249Although atomic clauses cannotbe interleaved, the intermediatestates are still constructed.Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20025025

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002d stepproctype P1() { d step {t1a; t1b; t1c} }proctype P2() { t2a; t2b; t2c }init { run P1(); run P2() }It is as if P1 has only one transition (2,2)(3,2)(0,3)(1,3)(2,3)No intermediate states willbe constructed.(3,3)Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorial51Checking for pure atomicity Suppose we want to check that none of the atomic clausesin our model are ever blocked (i.e. pure atomicity).1. Add a global bit variable:2. Change all atomic clauses to:atomic {stat1;bit aflag;aflag 1;stat23. Check that aflag is always 0.[]!aflage.g.active process monitor {assert(!aflag);}Thursday 11-Apr-2002statnaflag 0;}Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20025226

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002timeout(1) Promela does not have real-time features.– In Promela we can only specify functional behaviour.– Most protocols, however, use timers or a timeoutmechanism to resend messages or acknowledgements. timeout– SPIN’s timeout becomes executable if there is noother process in the system which is executable– so, timeout models a global timeout– timeout provides an escape from deadlock states– beware of statements that are always executable Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorialtimeout53(2) Example to recover from message loss:active proctype Receiver(){bit recvbit;do:: toR ? MSG, recvbit - toS ! ACK, recvbit;:: timeout- toS ! ACK, recvbit;od} Premature timeouts can be modelled by replacing thetimeout by skip (which is always executable).One might want to limit the number of prematuretimeouts (see [Ruys & Langerak 1997]).Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20025427

Theo C. Ruys - SPIN Beginners' TutorialDEMOversion: Friday, 13 September 2002Alternating Bit Protocol abp-1.pr– perfect lines abp-2.pr(3)How large should MAX besuch that we are sure thatthe ABP works correctly?onlythree!– stealing daemon (models lossy channels)– how do we know that the protocol works correctly? abp-3.pr– model different messages by a sequence number– assert that the protocol works correctly– how can we be sure that different messages are beingtransmitted?Thursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' Tutorial55gotogoto label– transfers execution to label– each Promela statement might be labelled– quite useful in modelling communication protocolswait ack:Timeout modelled by a channel.if:: B?ACK - ab 1-ab ; goto success:: ChunkTimeout?SHAKE - if:: (rc MAX) - rc ; F!(i 1),(i n),ab,d[i];goto wait ack:: (rc MAX) - goto errorfifi ;Part of model of BRPThursday 11-Apr-2002Theo C. Ruys - SPIN Beginners' TutorialSPIN 2002 Workshop, Grenoble, 11-13 April 20025628

Theo C. Ruys - SPIN Beginners' Tutorialversion: Friday, 13 September 2002unless{ stats } unless { guard; stats }– Statements in stats are executed until the firststatement (guard) in the escape sequence becomesexecutable.– resembles exception handling in languages like Java– Example:proctype MicroProcessor() {{./* execute normal ins

Theo C. Ruys - SPIN Beginners' Tutorial version: Friday, 13 September 2002 SPIN 2002 Workshop, Grenoble, 11-13 April 2002 7 Thursday 11-Apr-2002 Theo C. Ruys - SPIN Beginners' Tutorial 13 SPIN - Introduction (2) Major versions: 4.0 late 2002 Ax: automata extraction from C code 3.0 Apr 1997 minimised automaton representation