Original scientific paper Informacije ^efMIDEM A Innrnal of M Journal of Microelectronics, Electronic Components and Materials Vol. 43, No. 4 (2013), 235 - 250 Model Checking using Spin and SpinRCP Zmago Brezočnik, Boštjan Vlaovič, Aleksander Vreže Faculty of Electrical Engineering and Computer Science, University of Maribor, Slovenia Abstract: Spin is one of the leading verification tools for the model checking of distributed systems. It is used over a broad spectrum of applications where systems can be represented as asynchronously running processes. This paper provides an overview of the concepts of model checking, the Spin model checker together with its input language Promela, and of the available graphical user interfaces to Spin. In order to offer Spin users an integrated development environment for Spin, we have developed a SpinRCP. We introduce its structure and demonstrate some of its features by considering a standard algorithm for leader election in a unidirectional ring. Keywords: formal verification, model checking, modelling, simulation, Promela, Spin, SpinRCP Preve^rjanje modelov z uporabo orodij Spin in SpinRCP Izvleček: Spin je eno izmed vodilnih verifikacijskih orodij za preverjanje modelov porazdeljenih sistemov. Uporablja se za širok spekter aplikacij, pri katerih lahko sisteme predstavimo kot asinhrono izvajajoče se procese. V članku podajamo kratek pregled osnovnih pojmov o preverjanju modelov, preverjalniku modelov Spin, njegovem vhodnem jeziku Promela in razpoložljivih grafičnih uporabniških vmesnikih za Spin. Da bi uporabnikom orodja Spin ponudili integrirano razvojno okolje za Spin, smo razvili SpinRCP. Predstavljamo njegovo strukturo in prikažemo nekatere izmed njegovih značilnosti na primeru standardnega algoritma za izbiro vodje v enosmernem obroču. Ključne besede: formalna verifikacija, preverjanje modelov, modeliranje, simulacija, Promela, Spin, SpinRCP ' Corresponding Author's e-mail: brezocnik@uni-mb.si 1 Introduction The constantly increasing sizes and complexities of contemporary ICT (Information and Communication Technology) systems as well as demands for reduction in costs and a shortening of time-to-market for a new product, confront designers with harder and harder tasks for ensuring the correct functioning of developed systems. Nowadays, ICT systems are becoming ubiquitous in our daily lives and we have to rely on their correctness. If any of them malfunction, it will be at least annoying for its user but in the case of safety-critical systems, such as for example systems in transport, medicine, industry, ecology, telecommunications, space exploration, and the military, each undiscovered error in the hardware or software may cause a lot of damage, threatening the health or even the lives of people. Let us recall some dramatic examples. Between 1985 and 1987 four cancer patients died and two were seriously injured following incorrect behaviour (100-times radiation overdosing) of the Therac-25 anti-tumour ir- radiating machine. The cause was a design error in the control software. On 4th June 1996, the Ariane 5 rocket changed trajectory and exploded 40 seconds after being launched on its first flight. The cause of failure was a variable overflow during the conversion of a 64-bit real number to a 16-bit integer. In 1997, a computer onboard the Mars Pathfinder had to be reset often due to an error in the algorithm for access of several processes to a common computer bus. A design error in the Intel Pentium floating point division algorithm in 1994 caused the loss of about 450 million dollars when replacing faulty processors. Therefore, the reliability of systems is a key issue in the system design process that takes up the greatest part of the design time and effort. A very promising approach towards ensuring the correctness of ICT systems is that of model checking. Model checking is a formal verification method that can automatically verify the desired behavioural properties of a given system through exhaustively exploring all states of a system's suitable model. One of the most successful model checkers is Spin [1, 2]. Although it was originally designed as a tool for protocol verification, it is capable of model checking and simulating almost any system consisting of asynchronously running processes. Spin is a command line tool that accepts user commands from a command line and also outputs the results there. In order to ease Spin model checking, some graphical user interfaces have appeared for Spin. Two of them were developed at the Faculty of Electrical Engineering and Computer Science at the University of Maribor. In this paper we introduce the latest one called SpinRCP. Section 2 introduces the basic concepts of model checking including its strengths and weaknesses. Section 3 provides a short overview of Spin and its input language called Promela. Section 4 gives an overview of the currently available graphical user interfaces for Spin. Section 5 introduces our new integrated development environment (IDE) for Spin called SpinRCP. The use of SpinRCP is demonstrated on the model of an algorithm for leader election in a unidirectional ring in Section 6. Section 7 draws together the concluding remarks. 2 Model checking Model checking is an automated technique that, given the finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model. A detailed explanation of the model checking technique can be found in [3]. A schematic view of model checking is shown in Fig. 1. We can distinguish between three different phases when applying model checking to a system: the modelling, running, and analysis phases. Figure 1: Schematic view of model checking. In the modelling phase, a model of the system under consideration has to be obtained. Models describe the possible behaviours of systems in a precise and unambiguous manner. They are usually expressed as finite-state automata that consist of a finite set of states and a final set of transitions. Models can be created either manually or automatically using a model extraction tool. In both cases the model has to be described in a description language used by the model checker. Simple errors within the model can be found by simulation prior to the model checking. Such inexhaustive simulation can disclose errors in the model but it cannot guarantee that the model is error-free. In order to find any remaining subtle errors, we have to resort to rigorous verification using model checking. The informal requirements for the system's behaviour have to be formalised into precise and unambiguous properties using an adequate property specification language. A kind of temporal logic is most often used. The model checking process actually checks whether the system description M is a model of a temporal logic formula P. A temporal formula can express the behaviour of a system over time. It allows the specifying of relevant system properties regarding the following kinds: functional correctness (does the system do what it should?), safety ("something bad never happens"), live-ness ("something good will eventually happen"), fairness (does an event occur infinitely often under certain conditions?), and real-time properties (does the system act in due time?). In the running phase the user has to set various options, parameters, and directives for the model checker that should be used for verification. Then, the model checker automatically checks the validity of the property under examination in all states of the system model. In the analysis phase the user has to evaluate the outcome of model checking performed within the previous phase. There are three possible outcomes: the specified property is either valid or violated in the given model, or the model turns out to be too large to fit in the available computer memory or the model checking run is unfinished within a reasonable amount of time. If the property is valid, the next property can be checked with a new run perhaps with different options, parameters, and/or directives. If the property is violated, a counterexample is generated that can be analysed by simulation. The counterexample guides the simulation run across a path where the property is violated. A thorough counterexample analysis can reveal the cause of the violation. It may be a modelling error, a system design error, or a property error. In the case of the modelling error, the model does not reflect the design of the system. The model has to be corrected and all the properties have to be checked again. In the case of the system design error, the system does not behave as required and has to be corrected. The last possible cause is that the property does not reflect the informal requirement for the system behaviour. This implies a revision of the property and a new verification for this property. The designed system is verified with respect to the given properties if and only if all of them have been proven valid. Whenever the model is too large to be handled within the available amount of computer memory or within a reasonable time, the model has to be reduced using different abstractions. Model checking has many strengths including the following ones: it is a general technique that is applicable to a wide range of systems (e.g., protocols, hardware, software), it allows partial verification (only the more relevant properties are checked), it is nothing harder to find less likely errors than the more likely ones, it provides a counterexample in case a property is invalidated, it is an automatic technique and software tools exist, or it is more and more accepted in the industry. On the other hand, it also has some weaknesses: it is mainly appropriate for control-intensive applications and much less suitable for data-intensive applications, it is applicable only to final-state systems, it verifies a system model, and not the system itself, its results are only as good as the system model, it checks only given properties and provides no guarantee about the completeness of the results, it is faced with state-space explosion, or it cannot handle parameterised systems. Despite these weaknesses it is a fact that model checking is an effective technique for exposing potential design errors and thus increases the quality of a system design. 3 Spin and Promela This section provides a short introduction to the input language of Spin called Promela and the main features of Spin. 3.1 Short Introduction to Promela Promela (Process or Protocol Meta Language) is a language for describing finite state automata. It is not intended to be an implementation language but a system description language that is aimed at facilitating the searches for good abstractions of systems' designs. The language is oriented towards the modelling of process coordination and synchronisation, and not to computation. The reason is simple. Promela is not a programming language but a verification modelling language. Promela language reference can be found in [1]. A Promela model consists of processes, variables, and channels. It corresponds to a finite state transition system, hence all objects in Promela are bounded. The processes are global objects, whilst the variables and channels may be declared either as global or local to a process. A new inline or block scope for variables has been introduced since Spin Version 6. The processes are instantiations of proctype declarations and define parts of the system's behaviour. A proctype consists of a name, a list of formal parameters, local variable declarations, and a body. The body consists of a sequence of statements. A process executes concurrently with all other processes. It communicates with other processes using either global (shared) variables or channels. There may be several processes of the same type. Each process has its own local state that consists of a process counter (current location within the proctype) and the values of the local variables. Processes can be created within any process at any point of execution using the run statement. They can also be created by adding the keyword active in front of the proctype declaration. A so-called init process becomes active in the initial state of the system. It serves to initialise other processes and global variables. Promela has nine basic (integer) variable types: bit or bool (1 bit), byte (8 bits), chan (8 bit), mtype (8 bit), pid (8 bit), short (16 bits), int (32 bits), unsigned (1one. To rename more messages within a single command, a space has to be entered for separating individual renamings. When we want to make an abstraction of the model, we can use a powerful feature of joining a group of processes into a virtual process. For example, the 1,2>onetwo command has to be entered in order to join processes with IDs 1 and 2 into a virtual process called onetwo. More virtual processes can be created within a single command using a space separator. The abstraction by joining processes results in a smaller number of processes in the MSC as well as in a smaller number of messages displayed, as all messages within each group of joined processes are internal for the virtual process and therefore not shown. Parameter hiding is especially useful when reviewing simulation trails of real systems, where messages often contain many parameters that lead to less transparent diagrams. The same set of simulation view options is also available in the Spin Trail to MSC View, which is intended for converting a Spin simulation output trail to the standard MSC text format according to [13] in the same manner that the Export to MSC command does. In addition, Spin Trail to MSC View displays a list of created processes and messages transmitted between them during the simulation run. During the simulation run the variable values and queue contents values are updated in two separate tables at the bottom of the Simulation View. The current simulation step number is shown at the top of the tables. p0: <> (nr_leaders > 0) p1: <>[] (nr_leaders == 1) p2: [] (nr_leaders == 0 U nr_leaders == 1) p3: ![] (nr_leaders == 0) Such in-model specification of LTL properties has been supported since Spin Version 6. They state "positive" properties. Spin performs the negation automatically. After a successful syntax check, eventual redundancy check and/or listing of a model symbol table, it is useful to become more acquainted with the model. For this purpose we can first generate and display a graphical representation of a state transition system (an automaton) for each proctype and never claim in the model. By clicking the Automata View button in the Tool bar, the Automata View preference page (Fig. 4) opens and gives us the choice of selecting the type of files that will contain the automata. Let us suppose that we select the pdf file type (as in Fig. 4). Then the following sequence of commands is executed: 6 Leader election example Let us demonstrate some features of SpinRCP by considering a standard algorithm for leader election in a unidirectional ring. An efficient algorithm for solving this problem was published in [19]. The Promela model of this algorithm is taken from Spin Version 6 distribution. The leader election algorithm, when given a circular arrangement of N uniquely numbered processes in a unidirectional ring, determines the maximum number in a distributive manner. Communication occurs only between neighbours around the ring. All processes have the same program. They differ only by having distinct numbers (known only to the owners) in their local memory. We suppose that N = 5. The Promela model contains two proctype definitions: init and nnode. The init process first assigns a unique number for each of the five processes using non-deterministic choices. Then it creates five instances of a nnode process and assigns them their numbers. Next, the five nnode processes start to send and receive messages around the ring and process them according to the algorithm. A process terminates when it recognizes whether it is a leader (has the greatest number in a ring) or not. A global variable nr_leaders is defined and initialised to zero in line 26. In lines 28 through to 31, four required properties for the algorithm are specified with the following LTL formulas: spin -o3 -a leader.pml gcc-4 -o pan pan.c pan -D | dot>leader-automata dot -O -Tpdf leader-automata The first command generates the verifier source code for the model leader.pml without statement merging, the second one compiles it, the third one writes state tables in dot-format to leader-automata file, and the last one creates a pdf file with the automaton for each proctype and never claim. Now a new selection dialogue is open and we can select, which automaton we want so see. Each selected automaton is opened in a system application that is assigned for a given file type. Let us suppose that we want to see the automata for nnode, p0, p1, and p2. To save space, all of them are placed together in Fig. 9. In order to deepen understanding of the model and perhaps to find some early (simple) errors before verification, it is wise to perform random and/or interactive simulation. In random simulation, Spin decides by itself, as to which one of the executable statements will be chosen at the points of non-deterministic selections. In interactive simulation, these decisions have to be made by a user. Fig. 8 shows the content of the console, the MSC Editor window, and the Simulation View on completion of the random simulation of the leader. pml model. At the bottom of the Variable values table in the Simulation View it is evident that the nr_leaders variable is given the final value 1. We may want to prove several interesting properties about this algorithm but one of the most important Figure 9: Automata for nnode, p0, p1, and p2. seems to be the property that under no conditions should it be possible that more than one process declare to be the ring leader. Firstly, let us check p0, i.e., that eventually the number of leaders is greater than 0. By clicking the Verification tool button, the Verification preference page (Fig. 6) is displayed. Since p0 specifies a liveness property, we must select the Liveness and Acceptance cycles radio buttons. Next, we select Apply never claim and as a manner of never claim specification select In-model LTL formula/claim name. Finally, we enter the name of the in-model LTL formula, p0, in the text field to the right of the label. As a result of verification, Spin returns that no error is found (i.e., the model fulfils the property p0) (see the Console in Fig. 2). But it is as yet unclear whether the algorithm will eventually always give one single leader. In order to verify this, we check if the model fulfils p1, i.e., if eventually the number of leaders will always be 1. Therefore, this time we enter p1 as the LTL formula name and run the verification again. Spin finds no errors, which means that the model fulfils p1. Now the only doubt about the correctness of the algorithm that still exists is whether the number of leaders goes from 0 to 1 directly with no intermediate numbers greater than 1. In order to find out the answer to this question, we check whether the system fulfils p2 as well, i.e., the number of leaders is always 0 until the number of leaders is 1. The new verification run succeeds and thus p2 is verified. p3 specifies that the number of leaders is not always zero. This means that eventually the number of leaders is not zero. Since this number cannot be negative, p3 means exactly the same as p0, and is thus already verified. 7 Conclusions Using the Spin model checker on a huge model, automatically extracted from the SDL code of a real telecommunication industry product, encouraged us to develop an integrated development environment for Spin model checking called SpinRCP. SpinRCP is based on the Rich Client Platform technology. It is written in Java as an Eclipse plug-in and then exported together with many other plug-ins as an Eclipse product. Therefore, it runs as a stand-alone RCP application on any platform without the need for an installed Eclipse but nevertheless has many of the useful Eclipse functionalities. The whole application consists of 92 plug-ins. The Java source code for our plug-in called org.um.feri.spin.rcp is contained in 19 Java packages with a total of 84 files defining Java classes. The total amount of our source code is around 16,800 lines of Java code. The help contents for SpinRCP is implemented in a separate plug-in that contains more than 60 html files with descriptions of individual help topics and many xml configuration files. Currently, SpinRCP runs on 32- and 64-bit Windows operating systems. Platforms with other operating systems will be supported later. Once the website for SpinRCP is ready, it will be publicly announced. Amongst the more important features of SpinRCP are the following ones: a user-friendly Promela editor with syntax colouring, code folding, keyword autocomple-tion, and syntax error marking, running Spin verification, random, guided, and interactive simulation, graphical MSC viewing, abstracting MSCs by joining some processes into an abstract process, conversion of Spin simulation output trail to a standard text file, which is readable by professional MSC viewers, displaying graphical automata representation of proctype definitions and never claims in a model. There are still a lot of ideas for improvements and new features. Let us mention just some of them: better Spin simulation output filtering, stepping back in time during single step simulation, indication of the statement that is currently executed during a simulation run in the Promela source file, display of a process creation in the MSC Viewer, generation of state tables for proctype definitions and never claims, cleanup of temporary files, verification management, swarm support [15] for distributing a model checking task to more CPU cores or to a cloud of workstations, etc. APPENDIX A 1 /* Dolev, Klawe & Rodeh for leader election in unidirectional ring 2 * 'An O(n log n) unidirectional distributed algorithm for extrema 3 * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 4 5 * Randomized initialization added -- Feb 17, 1997 6 */ 7 8 /* sample properties: 9 * <>elected 10 * <>[]oneLeader 11 * [] (noLeader U oneLeader) 12 * ![] noLeader 13 * 14 * ltl format specifies positive properties 15 * that should be satisfied -- spin will 16 * look for counter-examples to these properties 17 * verify as: 18 * spin -a leader.pml 19 * cc -o pan pan.c 20 * ./pan -N p0 21 * ./pan -N p1 22 * ./pan -N p2 23 * ./pan -N p3 24 */ 25 26 byte nr_leaders = 0; 27 28 ltl p0 { <> (nr_leaders > 0) } 29 ltl p1 { <>[] (nr_leaders == 1) } 30 ltl p2 { [] (nr_leaders == 0 U nr_leaders == 1) } 31 ltl p3 { ![] (nr_leaders == 0) } 32 33 #define N 5 /* number of processes in the ring */ 34 #define L 10 /* 2xN */ 35 byte I; 36 37 mtype = { one, two, winner }; 38 chan q[N] = [L] of { mtype, byte}; 39 40 proctype nnode (chan inp, out; byte mynumber) 41 { bit Active = 1, know_winner = 0; 42 byte nr, maximum = mynumber, neighbourR; 43 44 xr inp; 45 xs out; 46 47 printf(„MSC: %d\n", mynumber); 48 out!one(mynumber); 49 end: do 50 :: inp?one(nr) -> 51 if 52 :: Active -> 53 if 54 :: nr != maximum -> 55 out!two(nr); 56 neighbourR = nr 57 :: else -> 58 know_winner = 1; 59 out!winner,nr; 60 fi 61 :: else -> 62 out!one(nr) 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 fi :: inp?two(nr) -> if :: Active -> if :: neighbourR > nr && neighbourR > maximum -> maximum = neighbourR; out!one(neighbourR) :: else -> Active = 0 fi :: else -> out!two(nr) fi :: inp?winner,nr -> if :: nr != mynumber -> printf(„MSC: LOST\n"); :: else -> printf(„MSC: LEADER\n"); nr_leaders++; assert(nr_leaders == 1) fi; if :: know_winner :: else -> out!winner,nr fi; break od } init { byte proc; byte Ini[6];/* N<=6 randomize the process numbers */ atomic { I = 1; /* pick a number to be assigned 1..N */ do :: I <= N -> if /* non-deterministic choice */ :: Ini[0] == 0 && N >= 1 -> Ini[0] = I :: Ini[1] == 0 && N >= 2 -> Ini[1] = :: Ini[2] == 0 && N >= 3 -> Ini[2] = :: Ini[3] == 0 && N >= 4 -> Ini[3] = :: Ini[4] == 0 && N >= 5 -> Ini[4] = I :: Ini[5] == 0 && N >= 6 -> Ini[5] = I /* works for up to N=6 */ fi; I++ :: I > N -> /* assigned all numbers 1..N */ break od; 116 proc = 1; 117 do 118 :: proc <= N -> 119 run nnode (q[proc-1], q[proc%N], Ini[proc-1]); 120 proc++ 121 :: proc > N -> 122 break 123 od 124 } 1 25 } Acknowledgments This work was partially supported by the Slovenian Research Agency within the research programme Advanced Methods of Interaction in Telecommunication. References 1. G.J. Holzmann, "The Spin Model Checker: Primer and Reference Manual", Addison-Wesley, 2004. 2. G.J. Holzmann, "The Model Checker SPIN', IEEE Transaction on Software Engineering, vol. 23, no. 5, pp. 279-295, 1997. 3. C. Baier, J.-P. Katoen, "Principles of Model Checking", The MIT Press, 2008. 4. T.C. Ruys, "SPIN Beginners' Tutorial", SPIN 2002 Workshop, Grenoble, France, April 11, 2002, electronic file available at http://spinroot.com/spin/ Man/. 5. M. Ben-Ari, "Principles of the Spin Model Checker"', Springer, 2008. 6. V.J. Koskinen, J. Plosila, Applications for the Spin Model Checker - A Survey, Technical Report 782, Turku Centre for Computer Science, Finland, September 2006. 7. M. Ben-Ari, jSpin -"Java GUI for SPIN: User's Guide", Version 5.0, electronic file available at http://code. google.com/p/jspin/downloads/list, 2010. 8. T. Kovše, "Integration of Spin Tool into Development Environment Eclipse", Diploma Work (in Slovene), Faculty of Electrical Engineering, Slovenia, 2008. 9. T. Kovše, B. Vlaovič, A. Vreže, Z. Brezočnik, "Eclipse plug-in for spin and st2msc tools - tool presentation", Lecture Notes in Computer Science, vol. 5578, pp. 143-147, 2009. 10. B. Vlaovič, A. Vreže, Z. Brezočnik, T. Kapus, "Automated generation of Promela model from SDL specification", Computer Standards and Interfaces, vol. 29, no. 4, pp. 449-461, 2007. 11. A. Vreže, B. Vlaovič, Z. Brezočnik, "Sdl2pml - tool for automated generation of Promela model from SDL specification", Computer Standards and Interfaces, vol. 31, no. 4, pp. 779-786, 2009. 12. T. Kovše, B. Vlaovič, A. Vreže, Z. Brezočnik, "Spin Trail to a Message Sequence Chart Conversion Tool", ConTEL 2009, I. Podnar 2arko, B. Vrdoljak (Eds.), Proceedings of the 10th International Conference on Telecommunications, Zagreb, Croatia, June 8-10, 2009. 13. "Message Sequence Chart (MSC): Recommendation ITU-T Z.120', International Telecommunication Union, 2011, electronic file available at http:// www.itu.int/rec/T-REC-Z.120-201102-I/en. 14. M.J. Hornos, J.C. Augusto,"Installation Process and Main Functionalities of the Spin Model Checker", electronic file available at http://digibug.ugr.es/ handle/10481/19601, 2012. 15. G.J. Holzmann, R. Joshi, A. Groce, "Swarm Verification Techniques", IEEE transactions on Software Engineering, vol. 37, no. 6, pp. 845-857, 2011. 16. B. de Vos, L.C.L Kats, C. Pronk, "EpiSpin: An Eclipse Plug-In for Promela/Spin Using Spoofax", In: A. Groce, M. Musuvathi (Eds.): SPIN 2011, LNCS 6823, Springer-Verlag, pp. 177-182, 2011. 17. T. Kovše, "Environment for formal verification of safety-critical systems", Master Thesis (in Slovene), Faculty of Electrical Engineering and Computer Science, University of Maribor, Slovenia, 2011. 18. Graphviz - Graph Visualization Software, electronic file available at http://graphviz.org. 19. D. Dolev, M. Klave, M. Rodeh, "An O(n log n) Unidirectional Algorithm for Extrema Finding in a Circle", Journal of Algorithms, vol. 3, pp. 245-260, 1982. Arrived: 01. 10. 2013 Accepted: 08. 11. 2013