Front. Comput. Sci., 2014, 8(1): 1 16 DOI /s Model checking with fairness assumptions using PAT Yuanjie SI 1, Jun SUN 2,YangLIU

Transcription

1 Front. Comput. Sc., 2014, 8(1): 1 16 DOI /s Model checkng wth farness assumptons usng PAT Yuanje SI 1, Jun SUN 2,YangLIU 3, Jn Song DONG 4, Jun PANG 5, Shao Je ZHANG 2, Xaohu YANG 1 1 College of Computer Scence, Zhejang Unversty, Hangzhou , Chna 2 Informaton System Technology and Desgn, Sngapore Unversty of Technology and Desgn, Sngapore , Sngapore 3 School of Computer Engneerng, Nanyang Technologcal Unversty, Sngapore , Sngapore 4 School of Computng, Natonal Unversty of Sngapore, Sngapore , Sngapore 5 Faculty of Scence, Technology and Communcaton, Unversty of Luxembourg, Luxembourg L-1359, Luxembourg c Hgher Educaton Press and Sprnger-Verlag Berln Hedelberg 2013 Abstract Recent development on dstrbuted systems has shown that a varety of farness constrants (some of whch are only recently defned) play vtal roles n desgnng selfstablzng populaton protocols. Exstng model checkers are defcent n verfyng the systems as only lmted knds of farness are supported wth lmted verfcaton effcency. In ths work, we support model checkng of dstrbuted systems n the toolkt PAT (process analyss toolkt), wth a varety of farness constrants (e.g., process-level weak/strong farness, event-level weak/strong farness, strong global farness). It performs on-the-flyverfcaton aganst lnear temporal propertes. We show through emprcal evaluaton (on recent populaton protocols as well as benchmark systems) that PAT has advantage n model checkng wth farness. Prevously unknown bugs have been revealed aganst systems whch are desgned to functon only wth strong global farness. Keywords model checkng, farness, PAT, verfcaton tool, formal methods 1 Introducton In the area of dstrbuted and concurrent system verfcaton, lveness means somethng good must eventually happen. Receved March 18, 2013; accepted October 10, 2013 E-mal: sunjun@sutd.edu.sg For nstance, a typcal requrement for leader electon protocols s that one and only one leader must be elected eventually n a network. A counterexample to a lveness property (aganst a fnte state system) s a loop (or a deadlock state, whch can be vewed as a trval loop) durng whch the good thng never occurs. For nstance, the network nodes may repeatedly exchange a sequence of messages and never elect a leader. Farness, whch s concerned wth a far resoluton of nondetermnsm, s often necessary and mportant to prove lveness propertes. Farness s an abstracton of the far scheduler n a mult-threaded programmng envronment or the relatve speed of the processors n dstrbuted systems. Wthout farness, verfcaton of lveness propertes often produces unrealstc loops durng whch one process or event s nfntely gnored by the scheduler or one processor s nfntely faster than others. It s mportant to rule out those counterexamples and utlze computatonal resources to dentfy the real bugs. However, systematcally rulng out counterexamples due to lack of farness s hghly non-trval. It requres flexble specfcaton of farness as well as effcent verfcaton wth farness. In ths work, we focus on formal system analyss wth farness assumptons. The objectve s to delver a toolkt whch model checks lnear temporal logc (LTL) propertes aganst dstrbuted systems functonng wth a varety of farness constrants. Farness and model checkng wth farness have attracted

2 2 Front. Comput. Sc., 2014, 8(1): 1 16 much theoretcal nterest for decades [1 5]. Ther practcal mplcatons n system/software desgn and verfcaton have been dscussed extensvely. Recent development on dstrbuted systems show that there are a famly of farness notons, ncludng a newly formulated farness noton named strong global farness [6], whch are crucal for desgnng self-stablzng dstrbuted algorthms [6 9]. The populaton protocol model has emerged as an elegant computaton paradgm for descrbng moble ad hoc networks [7]. Such networks consst of multple moble nodes whch nteract wth each other to carry out a computaton. Applcaton domans of the protocols nclude wreless sensor networks and bologcal computers. The nteracton events among the nodes are subject to farness constrants. One essental property of populaton protocols s that all nodes must eventually converge to the correct output values (or confguratons). A number of populaton protocols have been proposed and studed [6 9]. Farness plays an mportant role n the protocols. For nstance, n [6] t was shown that wth the help of an eventual leader detector (see detals n Secton 2), selfstablzng algorthms can be developed to handle two natural classes of network graphs: complete graphs and rngs. The algorthm for the complete graph works wth event-level strong farness, whereas the algorthm for rngs, only works wth strong global farness. It has been proved that wth only event-level strong farness or weaker, unform self-stablzng leader electon n rngs s mpossble [6]. Because the algorthms are desgned to functon wth farness, model checkng of (mplementatons of) the algorthms thus must be carred out wth the respectve farness constrants. Exstngmodel checkersare neffectve wth respect to farness. One way to apply exstng model checkers for verfcaton wth farness constrants s to re-formulate the property so that farness constrants become premses of the property. A lveness property φ s thus verfed by showng the truth value of the followng formula: f arness assumptons = φ Ths practce s, though flexble, defcent for the reason below. Model checkng s PSPACE-complete n the sze of the formula. In partcular, automata-based model checkng reles on constructng a Büch automaton from the LTL formula. The sze of the Büch automaton s exponental to the sze of the formulas. Thus, t s nfeasble to handle large formulas, whereas a typcal system may have multple or many farness constrants. There has been dedcated research on handlng large LTL formulae [10, 11]. In [12], Pang et al. appled the SPIN model checker to establsh the correctness of a famly of populaton protocols. Only protocols relyng on a noton of weak farness operatng on very small networks were verfed because of the problems dscussed above. Protocols relyng on a noton of stronger farness (e.g., strong farness or strong global farness) are beyond the capablty of SPIN even for the smallest network (e.g., wth three nodes). It s mportant to develop an alternatve approach and toolkt whch can handle larger networks because real counterexamples may only be present n larger networks, as shown n Secton 5. An alternatve method s to desgn specalzed verfcaton algorthms whch take farness nto account whle performng model checkng. The focus of exstng model checkers has been on process-level weak farness, whch, nformally speakng, states that every process shall make nfnte progress f always possble (see detaled explanaton n Secton 2). For nstance, SPIN has mplemented a model checkng algorthm whch handles ths knd of farness. The dea s to copy the global reachablty graph K + 2 tmes (for K processes) so as to gve each process a far chance to progress. Process-level strong farness s not supported because of ts complexty. It has been shown that process-level farness may not be suffcent, e.g., for populaton protocols. In ths work, we enhance a toolkt PAT (process analyss toolkt) to support on-the-fly model checkng wth a varety of farness constrants ncludng process-level weak/strong farness, event-level weak/strong farness, strong global farness, etc. Our model checkng algorthm unfes prevous work on model checkng based on fndng strongly connected components (SCC) and extends t to handle newly proposed notons lke strong global farness and event-labeled farness effcently. After enhancement, PAT supports a rch modelng language and an easy way of applyng farness. A PAT user can choose one of the farness constrants and apply t to the whole system. Usng PAT, we dentfed prevously unknown bugs n the mplementaton of populaton protocols [6, 13]. For experments, we compare PAT wth SPIN over recent dstrbuted algorthms as well as benchmark systems. We show that our approach handles farness more flexbly and effcently. The man contrbuton of ths work s the enhancement of PAT to support modelng, smulaton and model checkng of dstrbuted algorthms wth farness constrants. PAT s appled to a number of case studes ncludng recently proposed populaton protocols and have successfully found prevously unknown bugs. Another contrbuton s that we extend prevously developed model checkng algorthm wth weak/strong farness to model check wth a varety of farness, ncludng

3 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 3 strong global farness and event-labeled farness. The remander of the artcle s organzed as follows. Secton 2 shows a concrete motvatng example and our computatonal model, together wth a famly of farness constrants. Secton 3 develops necessary theores for model checkng. Secton 4 presents the algorthmforverfcaton wth farness. Secton 5 presents the PAT model checkng system, and experment results. Secton 6 dscusses the related work. Secton 7 concludes the paper. 2 Background In ths secton, we start wth ntroducng a concrete motvatng example and then present our computatonal model as well as formal defntons of farness. 2.1 Motvatng examples Leader electon s a fundamental problem n dstrbuted systems. The problem s easly solved wth the help of a central coordnator. Nonetheless, there may not be a central coordnator n domans lke wreless sensor networks. Selfstablzng algorthms do not requre ntalzaton n order to operate correctly and can recover from transent faults that oblterate all state nformaton n the system. In [6, 7, 13], a number of algorthms have been proposed for the selfstablzng leader electon problem. In partcular, Fscher and Jang propose a self-stablzng algorthm for rng networks [6], whch guarantees that one and only one leader wll be eventually elected gven any ntal confguraton. The algorthm reles on two assumptons. One s that the system satsfes a rather strong farness constrant called strong global farness [6]. The other one s that there exsts a leader detector. The detector s a dagnostc devce whch tests network nodes for certan nformaton, whch s requred to eventually (not necessarly mmedately) detect the presence/absence of a leader. Fgure 1 presents the PAT model of the algorthm presented n [6]. PAT supports a modelng language whch mxes hghlevel specfcaton language features (e.g., determnstc or nondetermnstc choce, alphabetzed parallel, nterleavng, nterrupt, etc.) wth low-level programmng language features (arrays, whle, f-then-else, etc.), so that the users are offered wth great expressveness as well as flexblty. We skp the detals of the language as t s not the focus of ths work. Interested readers are referred to [14] for ts desgn prncples. Lnes 1 6 of Fg. 1 declares constants and varables of the model. In partcular, constant N (of value 3) to models the network sze,.e., the number of network nodes; correct s an ndcator whch s of value 1 f and only f the leader detector has started detectng correctly. guess s a Boolean flag representng the current dagnostc result of the detector,.e., true for the presence of a leader and false for the absence. Array ld (short for leader), bu (short for bullet), and sh (short for Fg. 1 Leader electon protocol for rngs

4 4 Front. Comput. Sc., 2014, 8(1): 1 16 sheld) model the status of each node. For nstance, the bt of ld[n] tells whether the th node s a leader or not. We skp the ntuton behnd these varables and refer the readers to [6]. Lnes 7 and 8 declares two propostons. A proposton s a synonymy of a Boolean formula, whch may be used n the model or the assertons. In partcular, proposton oneleader s defned to be true f and only f there s one and only one leader (.e., ld[0] + ld[1] + ld[2] s 1). Proposton exst denotes the leader detector beleves there s a leader n the network. That s, f t has not startng detectng correctly (.e., correct s 0), then t guesses there s a leader (.e., guess s 1); otherwse f t detects correctly, then there s a leader n the network (.e., ld[0] + ld[1] + ld[2] > 0). Lnes 9 24 defne three processes n the form of equatons, whch capture the essence of the algorthm. In partcular, Lnes 9 20 defne process Node() whch models the behavors of a network node. Every tme there s an nteracton event n the network, the ntator and responder must update themselves accordng to a set of fve pre-defned rules, e.g., to become a leader f there s no leader (accordng to the leader detector), to stop beng a leader f both the ntator and the responder are leaders, etc. The rules are specfed usng a case statement of the followng form, case{ b 0 : P 0 b 1 : P 1 b k : P k } where b s a condton and P s a process expresson. The condtons are evaluated n sequence untl the frst one whch evaluates to true, then the correspondng process s executed. For nstance, f the leader detector beleves there s no leader n the network, then the condton at Lne 10 s true, and therefore the process expresson at Lne 11 s executed. The process expresson takes the form of e{program} P where e s an event name, program s a sequental program attached wth the event and P s a process. Intutvely, the event s taken and at the same tme the program s executed atomcally together. Next, process P s executed. In general, an event may be attached wth a sequental program (wth loops, branches, etc.), whch executes atomcally. Equvalently, oracle can be vewed as a label of the program (for easy referencng). For nstance, f the process expresson at Lne 11 s taken, event rule1..( + 1)%N s generated. At the same tme, bu[], d[]andsh[] are all set to be 1. Afterwards, process Node() s nvoked so that the network node repeats from the begnnng. We skp the detals of the rules and refer the readers to [6]. Lnes21 23defne the leader Detector, where [] s the uncondtonal choce operator borrowed from the classc CSP [15]. The detector has three choces. It may be enlghtened (Lne 21) through the event oracle and then detects correctly ever-after. Or, t may take a guess, randomly statng that there s a leader (Lne 23) or there s not (Lne 22). We remark that there s no guarantee that the detector wll eventually detect correctly (e.g., the event oracle may never happen) unless farness s appled. Lne 24 models the leader electon algorthm as process LeaderElecton. The algorthm frstly nvokes process Int, whch ntalzes the system n every possble confguraton, e.g., each element n the arrays may be ether assgned 0 or 1. We omt the detals of Int as t can be constructed straghtforwardly usng the uncondtonal choce operator []. After the ntalzaton, the system behaves as the nterleavng (modeled by operator ) of the leader detector and all the network nodes. The property of nterest to all leader electon algorthms s oneleader (defned as an asserton at Lne 25), where and are modal operators whch read as eventually and always respectvely. In PAT, we support the state/event LTL [16]. We remark that the asserton s false wth no farness, process-level weak/strong farness or event-level weak/strong farness. Counterexamples can be generated effcently for each of the cases usng PAT. The asserton s true wth strong global farness, as proved by PAT for bounded networks. However, verfyng the orgnal algorthm s only as useful as confrmng the theorem proved. In order to show that an mplementaton of the algorthm satsfes the property, t must be verfed wth strong global farness. To the best of our knowledge, PAT s the only tool whch s capable of fndng bugs n such a settng. 2.2 Models and defntons We present the approaches n the settng of labeled transton systems (LTS). Models n PAT are nterpreted as LTSs mplctly by defnng a complete set of operatonal semantcs. Let e be an event, whch could be ether an abstract event (e.g., a synchronzaton barrer f shared by multple processes) or a data operaton (e.g., a sequental program). Let Σ be the set of all events. Defnton 1 A Labeled Transton System L s a 3-tuple (S, nt, ) wheres s a set of system confguratons/states,

5 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 5 nt S s the ntal system confguraton and S Σ S s a labeled transton relaton. We wrte s e s to denote that (s, e, s ) s a transton n. enabledevt(s) s the set of enabled events at s,.e., e s n enabledevt(s) f and only f there exsts s such that s e s. If the system s consttuted by multple processes runnng n parallel, we wrte enabledpro(s)to be the setof enabledprocesses, whch may make a move gven the system state s. Gven a transton s e s, we wrte engagedpro(s, e, s )to be the set of partcpatng processes, whch have made some progress durng the transton. Notce that f e s synchronzed by multple processes, the set contans all the partcpatng processes. We wrte engagedevt(s, e, s ) to denote {e}. Because our targets are nontermnatng dstrbuted systems, and farness affects nfnte not fnte system behavors, we focus on nfnte system executons n the followng. Fnte behavors are extended to nfnte ones by appendng nfntely many dlng events at the rear. Gven an LTS L = (S, nt, ), an executon s an nfnte sequence of alternatng states and events E = s 0, e 0, s 1, e 1,... where e s 0 = nt and for all s s+1. Wthout farness constrants, a system may behave freely as long as t starts wth an ntal state and conforms to the transton relaton. A farness constrant restrcts the set of system behavors to only those far. Gven a propertyφ,verfcaton wth farness s to verfy whether all far executons of the system satsfy φ.inthefollowng, we revew a varety of dfferent farness constrants and llustrate ther dfferences usng examples. Defnton 2 Let E = s 0, e 0, s 1, e 1,... be an executon. E satsfes event-level weak farness, f and only f for every event e, fe eventually becomes enabled forever n E, then e = e for nfntely many,.e., e s enabled e s engaged. Event-level weak farness (EWF) [2] states that f an event becomes enabled forever after some steps, then t must be engaged nfntely often. An equvalent formulaton s that every computaton should contan nfntely many postons at whch e s dsabled or has just been engaged. The latter s known as justce condton [17]. Intutvely, t means that an enabled event shall not be gnored nfntely. Or equvalently some state must be vsted nfntely often (e.g., acceptng states n Büch automata). Defnton 3 Let E = s 0, e 0, s 1, e 1,... be an executon. E satsfes process-level weak farness, f and only f for every process p,fpeventually becomes enabled forever n E,then p engagedproc(s, e, s +1 )fornfntely many,.e., p s enabled p s engaged. Process-level weak farness (PWF) states that f a process becomes enabled forever after some steps, then t must be engaged nfntely often. From another pont of vew, process-level weak farness guarantees that each process s only fntely faster than the others. Weak farness (or justce condton) has been well studed and verfcaton wth weak farness has been supported to some extent, e.g., process-level weak farness s supported by the SPIN model checker [18]. Gven the LTS n Fg. 2(a), the property a s engaged s true wth event-level weak farness. Acton a s always enabledand,hence,by defnton t must be nfntely often engaged. The property s, however, false wth no farness or process-level weak farness. The reason that t s false wth process-level weak farness s that the process W may make progress nfntely (by repeatedly engagng n b) wthout ever engagng n event a. Alternatvely, f the system s modeled usng two processes as shown n Fg. 2(b), a s engaged becomes true wth process-level weak farness (or event-level weak farness) because both processes must make nfnte progress and therefore both a and b must be engaged nfntely. Ths example suggests that, dfferent from process-level weak farness, event-level weak farness s not related to the system structure. In general, processlevel farness may be vewed a specal case of event-level farness. By a smple argument, t can be shown that processlevel weak farness can be acheved by labelng all events n a process wth the same name and applyng event-level weak farness. For smplcty, n the rest of the paper, we wrte a (or a) to denote a s engaged (or a s engaged) unless otherwse stated. Fg. 2 Event-level vs. process-level weak farness Defnton 4 Let E = s 0, e 0, s 1, e 1,... be an executon. E satsfes event-level strong farness f and only f, for every event e, fe s nfntely often enabled, then e = e for nfntely many,.e., e s enabled e s engaged. Event-level strong farness (ESF) has been dentfed by dfferent researchers. It s named strong farness n [19] (by contrast to weak farness defned above). In [6], t s named strong local farness (n comparson to strong global far-

6 6 Front. Comput. Sc., 2014, 8(1): 1 16 ness defned below). It s also known as compasson condton [20]. Event-level strong farness states that f an event s nfntely often enabled, t must be nfntely often engaged. Ths type of farness s partcularly useful n the analyss of systems that use semaphores, synchronous communcaton, and other specal coordnaton prmtves. Gven the LTS n Fg. 3(a), the property b s false wth event-level weak farness but true wth event-level strong farness. The reason s that b s not always enabled (.e., t s dsabled at the left state) and thus the system s allowed to always take the c branch wth event-level weak farness. It s nfntely often enabled, and thus, the system must engagen b nfntely wth event-level strong farness. Fg. 3 Event-level vs. process-level strong farness Defnton 5 Let E = s 0, e 0, s 1, e 1,... be an executon. E satsfes process-level strong farness f and only f, for every process p, fp s nfntely often enabled, then p engagedproc(s, e, s +1 )fornfntely many,.e., p s enabled p s engaged. The process-level correspondence s process-level strong farness (PSF). Intutvely, process-level strong farness means that f a process s repeatedly enabled, t must eventually make some progress. Gven the LTS n Fg. 3(b), the property c s false wth process-level weak farness but true wth process-level strong farness. The reason s that event c s guarded by condton x = 1 and therefore s only repeatedly enabled. Verfcaton wth (event-level/process-level) strong farness (or compasson condton) has been dscussed prevously, e.g., n the settng of Streett automata [21,22], far dscrete systems [23] or programmng codes [24]. Nonetheless, there s few establshed tool support for formal verfcaton wth strong farness [1] to the best of our knowledge. The man reason s the computatonal complexty. For nstance, t s clamed too expensve to support n SPIN (page 182 of [18]). We, however, show that reasonably effcent model checkng wth strong farness can be acheved (refer to experment results n Secton 5). Defnton 6 Let E = s 0, e 0, s 1, e 1,... be an executon. E satsfes strong global farness f and only f, for every s, e, s e such that s s,fs = s for nfnte many, s = s and e = e and s +1 = s for nfntely many. Strong global farness (SGF) was suggested n [6]. It states that f a step (from s to s by engagng n event e) can be taken nfntely often, then t must actually be taken nfntely often 1).Dfferent from the prevous notons of farness, strong global farness concerns about both events and states, nstead of events only. It can be shown by a smple argument that strong global farness s stronger than eventlevel strong farness. Because t concerns about both events and states, t s event-level and process-level. Strong global farness requres that an nfntely enabled event must be taken nfntely often n all contexts, whereas event-level strong farness only requres the enabled event to be taken n one context. It can be shown that strong global farness concdes event-level strong farness when every transton s labeled wth a dfferent event. Ths observaton mples that we can unquely label all transtons wth dfferent events and then apply model checkng algorthm for strong farness to deal wth global farness. We show however, model checkng wth global farness can be solved usng a more effcent approach. Fgure 4 llustrates the dfference wth two examples. Under event-level strong farness, state 2 n Fg. 4(a) may never be vsted becauseall eventsare engagednfntely often f the left loop s taken nfntely. As a result, property state 2 s false. Under strong global farness, all states n Fg. 4(a) must be vsted nfntely often and therefore state 2 s true. Fgure 4(b) llustrates ther dfference when there s non-determnsm. Both transtons labeled a must be taken nfntely wth strong global farness, whch s not necessary wth event-level strong farness or weak farness. Thus, property b s true only wth strong global farness. Many populaton protocols rely on strong global farness, e.g., protocols presented n [6, 7]. As far as the authors know, there are no prevous works on model checkng wth strong global farness. Fg. 4 3 Loop/SCC searchng Strong global farness Gven an LTS L and an LTL formula φ, model checkng 1) The defnton n [6] s for unlabeled transton systems. We slghtly changed t so as to sut the settng of LTS.

7 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 7 s about searchng for an executon of L whch fals φ. In automata-based model checkng, the negaton of φ s translated to an equvalent Büch automaton B, whch s then composed wth the LTS representng the system model. Model checkng wth farness s to search for an nfnte executon whch s accepted by the Büch automaton and at the same tme satsfes the farness constrants. In the followng, we wrte L φ to mean that the LTS satsfes the property wth no farness,.e., every executon of L satsfes φ. We wrte L EWF φ (L PWF φ) to mean that L satsfes φ wth eventlevel (process-level) weak farness; L ESF φ (L PSF φ)to mean that L satsfes φ wth event-level (process-level) strong farness, and L SGF φ to mean that L satsfes φ wth strong global farness. We assume that L contans only fnte states. By a smple argument, t can be shown that L contans an nfnte executon f and only f there exsts a loop. A lasso n the product of L and B, denoted as R j, s a sequence of alternatng states/events (s 0, b 0 ), e 0,...,(s, b ), e,...,(s j, b j ), e j, (s j+1, b j+1 ), such that s s a state of L, b s a state of B, s = s j+1 and b = b j+1. We skp the detals on constructng the product and refer the readers to [18]. R j s acceptng f and only f the sequence b 0, e 0, b 1, e 1,...,b k, e k,... s acceptng to B,.e., the sequence vsts at least one acceptng state of B nfntely often. R j s far wth certan noton of farness f and only f the sequence s 0, e 0, s 1, e 1,...,s k, e k,... s. Furthermore, we defne the followng sets: alwaysevt(r j ) = {e k : {,..., j} e enabled(s k)}, alwayspro(r j ) = {p k : {,..., j} p enabledpro(s k)}, onceevt(r j ) = {e k : {,..., j} e enabled(s k)}, oncepro(r j ) = {p k : {,..., j} p enabledpro(s k)}, engagedevt(r j ) = {e k : {,..., j} e = e k}, engagedpro(r j ) = {p k : {,..., j} p engagedpro(s k, e k, s k+1 )}. Intutvely, set alwaysevt(r j )(alwayspro(r j )) s the set of events (processes) whch are always enabled durng the loop. Set onceevt(r j )(oncepro(r j )) s the set of events (processes) whch are enabled at least once durng the loop. Set engagedevt(r j )(engagedpro(r j )) s the set of events (processes) whch are engaged durng the loop. Lemma 1 Let L = (S, nt, ) beanlts;b be a Büch automaton equvalent to the negaton of an LTL formula φ. L EWF φ f and only f there does not exst R j s.t. alwaysevt(r j ) engagedevt(r j )andr j s acceptng. L PWF φ f and only f there does not exst R j s.t. alwayspro(r j ) engagedpro(r j )andr j s acceptng. L ESF φ f and only f, there does not exst R j s.t. onceevt(r j ) engagedevt(r j )andr j s acceptng. L PSF φ f and only f there does not exst R j s.t. oncepro(r j ) engagedpro(r j )andr j s acceptng. The lemma can be proved straghtforwardly by contradcton. By the lemma, a system fals the property wth certan farness f and only f there exsts a loop whch satsfes the farness and at the same tme fals the property. Modelng checkng wth farness s hence reduced to loop searchng. Gven a transton system, a subgraph s strongly connected f there s a path from each state n the subgraph to every other state n the subgraph. A SCC s a maxmal strongly connected subgraph. Gven the product of L and B,letS be a set of states whch, together wth the transtons among them, forms a strongly connected subgraph. In an abuse of notatons, we refer to S as the strongly connected subgraph n the followng. To further abuse notatons, we wrte alwaysevt(s ) (alwayspro(s ), onceevt(s ), oncepro(s ), engagedevt(s )or engagedpro(s )) to denote the set obtaned by applyng the functon to a loop whch traverses through all states of the subgraph. We say S s acceptng f and only f there exsts one state (s, b)ns such that b s an acceptng state of B. Lemma 2 Let L be an LTS; B be a Büch automaton equvalent to the negaton of an LTL formula φ. L ESF φ f and only f there does not exst a reachable strongly connected subgraph S n the product of L and B such that S s acceptng and onceevt(s ) engagedevt(s ). L PSF φ f and only f there does not exst a reachable strongly connected subgraph S n the product of L and B such that S s acceptng and oncepro(s ) engagedpro(s ). The above lemma can be proved by a smple argument. It shows that model checkng wth strong farness can be reduced to strongly connected subgraph (not SCC) searchng. Lemma 3 Let L be an LTS; B be a Büch automaton equvalent to the negaton of an LTL formula φ. L EWF φ f and only f there does not exst a reachable SCC S n the product of L and B such that S s

8 8 Front. Comput. Sc., 2014, 8(1): 1 16 acceptng and alwaysevt(s ) engagedevt(s ). L PWF φ f and only f there does not exst a reachable SCC S n the product of L and B such that S s acceptng and alwayspro(s ) engagedpro(s ). The proof of the lemma follows prevous results (see for example Chapter 6 of [25]). In the followng, we argue the event-level weak farness part of the lemma and remark that the other part can be proved smlarly. It can be shown that a system fals φ wth event-level weak farness f and only f there exsts one reachable strongly connected subgraph C such that C s acceptng and alwaysevt(c) engagedevt(c). Hence, t s suffcent to show that there exsts such a C f and only f there exsts a reachable SCC S such that S s acceptng and alwaysevt(s ) engagedevt(s ). If there exsts such an SCC S, then we smply let C be S. If there exsts such subgraph C, thesccs whch contans C s acceptng and satsfes alwaysevt(s ) engagedevt(s ) snce alwaysevt(s ) alwaysevt(c) andengagedevt(c) engagedevt(s ). Ths concludes the proof. The lemma shows that model checkng wth weak farness can be reduced to SCC searchng. The followng lemma reduces model checkng wth strong global farness to searchng for a termnal SCC n L. An SCC s termnal f and only f any transton startng from a state n the SCC must end wth a state n the SCC. Notce that a termnal SCC n the product of L and B may not be consttuted by a termnal SCC n L. Lemma 4 Let L be an LTS; B be a Büch automaton equvalent to the negaton of an LTL formula φ. L SGF φ f and only f there does not exst a reachable SCC S n the product of L and B such that S s acceptng and for all (s, b) S, f there exsts e and s e such that s s, then there exsts (s, b ) S such that (s, b) e (s, b ). Proof f there exsts R j L fals φ wth strong global farness f and only n the product of L and B such that R j s acceptng. L fals satsfes strong global farness and R j φ wth strong global farness f and only f there exsts a reachable strongly connected subgraph C such that a loop whch travels through all states/transtons n C (and no other states/transtons) nfntely often satsfes strong global farness and C s acceptng. Hence, t s suffcent to show that there exsts such a subgraph C f and only f there exsts an SCC S such that S whch satsfes the constrant. f: Ths s proved trvally. only f: Assume that there exsts such a subgraph C. Let x(c) = {s b (s, b) C} be the states of L whch consttute C and t(c) = {(s, e, s ) s x(c) s x(c) (s, b), (s, b ): e C (s, b) (s, b )} be the transtons of L whch consttute the strongly connected subgraph. By contradcton, t can be shown that x(c) (together wth the transtons n t(c)) forms one termnal SCC n L. LetS be the SCC contanng C. It can be shown that x(s ) (together wth the transtons n t(s )) forms the same termnal SCC. Therefore, S must satsfy the constrant. 4 Modelng checkng wth farness There are two groups of methods for loop searchng. One s basedonnesteddepth-frst-search (DFS) and the other one s based on dentfyng SCCs. Nested DFS has been mplemented n SPIN. The basc dea s to perform a frst DFS to reach a target state (.e., an acceptng state n the settng of Büch automata) and then perform a second DFS from that state to check whether t s reachable from tself. It has been shown the nested DFS works effcently for model checkng wth no farness [18]. Nonetheless, t s not sutable for verfcaton wth farness because whether an executon s far depends on the whole path nstead of one state. In recent years, model checkng based on SCC has been re-nvestgated and t has been shown that t yelds comparable performance [26]. In ths work, we extend the exstng SCC-based model checkng algorthms to cope wth dfferent notons of farness. The algorthm s nspred by early work on emptness check of Streett automata [22]. 4.1 A unfed algorthm Fgure 5 presents the algorthm. It s based on Tarjan s algorthm for dentfyng SCCs (whch s lnear tme n the number of graph edges [27]). It searches for far strongly connected subgraph on-the-fly. The basc dea s to dentfy one SCC at a tme and then check whether t s far or not. If t s, Fg. 5 Algorthm for model checkng wth farness

9 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 9 the search s over. Otherwse, the SCC s parttoned nto multple smaller strongly connected subgraphs, whch are then checked recursvely one by one. Fgure 6 presents a runnng example,.e., the product of an LTS and a Büch automaton. Notce that state 2 s an acceptng state. Fg. 6 Model checkng example Assume for now that S s the set of states and T s the set of transtons. The method takes three nputs,.e., S, T and a farness type F (of value ether EWF, PWF, ESF, PSF or SGF). At Lne 1, a set vsted, whch stores the set of vsted states, s ntalzed to be empty. The man loop s from Lnes At Lne 3 Tarjan s algorthm (mproved and mplemented as method fndscc(s, T)) s used to dentfy one SCC wthn S and T. Identfyng S and T for compostonal systems or software programs requres reachablty analyss. In order to perform on-the-fly verfcaton, fndscc s desgnednsuchawaythatfnos and T are gven, t wll explore states and transtons on-the-fly untl one SCC s dentfed. We skp the detals of fndscc as t largely resembles the algorthm presented n [21]. Gven the LTS presented n Fg. 6, fndscc dentfes two SCCs,.e., scc1 whchs composed of state 1 only and scc2 whch s composed of state 0, 2, and 3. The order n whch SCCs are found s rrelevant to the correctness of the algorthm. At Lne 4, we mark scc_states as vsted so that the SCC s not examned agan. At Lne 5, we check whether the SCC s acceptng. Only acceptng SCCs may contan a bad loop whch consttutes a counterexample. For nstance, scc1 s not acceptng and therefore gnored. Functon prune (at Lne 6) s used to prune bad states from the SCC. Bad states are the reasons why the SCC s not far. For nstance, state 0 (where the event a s enabled) s a bad state n scc2 wth event-based strong farness because event a s never engaged n scc2 (.e., a s not n engagedevt(ssc2)). State 3 s a bad state wth strong global farness because the step from state 3 to state 1vacs not part of the SCC. The ntuton behnd the prunng s that there may be a far strongly connected subgraph n the remanng states after elmnatng the bad states. By smply modfyng the prune method, the algorthm can be used to handle dfferent farness constrants. Refer to detals n Secton 2. If the SCC does satsfy the farness assumpton, no state s pruned and thus the sze of the SCC remans the same (Lne 7 of Fg. 5). In such a case, a far loop whch traverses all states/transtons n the SCC s generated as a counterexample and we conclude that the property s not true at Lne 8. We skp the detals on generatng the path n ths paper and remark that t could be a non-trval task (see [23]). If some states have been pruned, a recursve call s made to check whether there s a far strongly connected subgraph wthn the remanng states. The recursve call termnates n two ways. One s that a far subgraph s found (at Lne 9) and the other s all states are pruned (at Lne 14). If the recursve call returns true, there s no subgraph satsfyng the farness condton and we contnue wth another SCC untl all states are checked. 4.2 Copng wth dfferent notons of farness In ths secton, we show how to customze the prune functonsoastohandledfferent farness constrants. Let S be a strongly connected subgraph and T be the transton among the states. The followng defnes the prunng methods for event-based weak farness. prune(s, T, EWF) = S, f alwaysevt(s ) engagedevt(s ); prune(s, T, EWF) =, otherwse. If there exsts an event e whch s always enabled (.e., e alwaysevt(s )) but never engaged (.e., e not n engagedevt(s )), by defnton S does not satsfy event-level weak farness. If an SCC does not satsfy event-level weak farness, none of ts subgraphs do, because e s always enabled n any of ts subgraphs but never engaged. As a result, ether all states are pruned or none of them s. Smlarly, the followng defnes the prunng functon for process-level weak farness. prune(s, T, PWF) = S, f alwayspro(s ) engagedpro(s ); prune(s, T, PWF) =, otherwse. In the case of event-level (process-level) strong farness, a state s pruned f and only f there s an event (process) enabled at ths state but never engaged n the subgraph. By prunng the state, the event (process) may become never enabled and therefore not requred to be engaged. The followng defnes the prunng functon for event-level and process-level

10 10 Front. Comput. Sc., 2014, 8(1): 1 16 strong farness. prune(s, T, ESF) = {s : S enabledevt(s) engagedevt(s )}; prune(s, T, PSF) = {s : S enabledpro(s) engagedpro(s )}. By Lemma 4, an SCC may consttute a counterexample to a property wth strong global farness f and only f the SCC satsfes strong global farness and s acceptng. Therefore, we prune all states f t fals strong global farness. prune(s, T, SGF) = S, f (s, b) S e, s s e s s S ; prune(s, T, SGF) =, otherwse. We remark that the tme complexty of the prune functons are all lnear n the number of edges of the SCC. Gven the example n Fg. 6, wth event-level strong farness, state 0 s pruned from scc2 because enabledevt(state 0) = {a, c} engagedevt(scc2). After that the only remanng strongly connected subgraph contans states 2 and 3, now state 3 where c s enabled s consdered as a bad state because c s not engaged n the subgraph. State 2 s then pruned for beng a trval strongly connected subgraph whch fals event-level strong farness. 4.3 Complexty and soundness The tme complexty for verfcaton wth no farness, eventlevel or process-level weak farness or strong global farness are smlar,.e., all lnear n the number of transtons n the product automaton. All states n one SCC are dscarded at once n all cases and, therefore, no recursve call s necessary. Furthermore, the prune functon s lnear n the number of transtons of an SCC. SPIN s model checkng algorthm wth process-level weak farness ncreases the run-tme expense of a verfcaton run by a factor that s lnear n the number of runnng processes. In comparson, our algorthm s less expensve for weak farness. Ths becomes evdent by the experment results presented n Secton 5. Verfcaton wth event-level or process-level strong farness s n general expensve. In the worst case (.e., the whole system s strongly connected and only one state s pruned every tme), the fnd- SCC method may be nvoked at most #S tmes, where #S s the number of system states. Thus, the tme complexty s bounded by #S #T where #T s the number of transtons. In practce, however, f the property s false, a counterexample s usually dentfedquckly, becauseouralgorthmconstructs and checks SCCs on-the-fly. Even f the property s true, our experence suggests that the worse case scenaro s rare n practce. Instead of performng detaled complexty analyss (see the dscusson presented n [22]), we llustrate the performance of our algorthm usng real systems n Secton 5. Next, we argue the total correctness of the algorthm. The algorthm s termnatng because by assumpton, the number of states s fnte, and the number of vsted states and pruned states are monotoncally ncreasng. Theorem 1 Let L be an LTS. Let φ be a property. Let F be a farness type (.e., EWF, PWF, ESF, PSF or SGF). L F φ f and only f the algorthm returns true. Proof Case EWF: By Lemma 1, L EWF φ f and only f there does not exst an SCC S such that alwaysevt(s ) engagedevt(s )ands s acceptng. Gven any SCC S,the algorthm returns false f and only f t does so at Lne 8 because the recursve call at Lne 9 always returns true (by the defnton of prune(s, T, EWF)). Therefore, t returns false f and only f S s acceptng (so that the condton at Lne 5 s true) and alwaysevt(s ) engagedevt(s ) (so that the condton at Lne 7 s true). If there does not exst such an SCC, the algorthm returns true. If the algorthm returns true, there must not be such an SCC. Therefore, L EWF φ f and only f the algorthm returns true. Case PWF: Smlar to the above. Case ESF: By Lemma 3, L ESF φ f and only f there does not exst a strongly connected subgraph C such that onceevt(c) engagedevt(c)andc s acceptng. If C tself s an SCC, t must be found (by the correctness of Tarjan s algorthm and functon prune(s, T, ESF)) and the algorthm returns false f C s acceptng. If t s contaned n one (and only one) SCC, by the correctness of prune(s, T, ESF), ts states are never pruned. As a result, t s dentfed when all other states n the SCC are pruned or a far strongly connected subgraph contanng all ts states s dentfed. In ether case, the algorthm returns false f and only f such a far strongly connected subgraph s found. Equvalently, t returns true f and only f there are no such subgraphs. Therefore, L ESF φ f and only f the algorthm returns true. Case PSF: Smlar to the above. Case SGF: By Lemma 4, L SGF φ f and only f there does not exst an SCC S such that S satsfes strong global farness and S s acceptng. The algorthm returns false f and only f t s at Lne 8 because the recursve call at Lne 9 always

11 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 11 returns true (by the defnton of prune(s, T, SGF)). By defnton of prune(s, T, SGF), the control reaches Lne 8 f and only f the SCC s termnal and s acceptng. Thus, L SGF φ f and only f t returns true. 5 Implementaton and experments The man contrbuton of the work s the model checkng wth farness capablty n the PAT model checker. PAT s desgned for systematc valdaton of dstrbuted/concurrent systems usng state-of-art model checkng technques. Its man functonaltes nclude smulaton, explct on-the-fly model checkng, and verfcaton wth farness. It has three man components. The edtor features all standard text edtng functonaltes. The smulator allows users to nteractvely drve the system executon. The model checker combnes complementary model checkng technques for system verfcaton. In the followng, we show ts performance on both benchmark systems as well as recently developed populaton protocols, whch requre farness for correctness. All the models (wth confgurable parameters) are embedded n the PAT package and avalable onlne at our web ste Table 1 summarzes the verfcaton statstcs on recently developed populaton protocols. The experments are made on a 3.0 GHz Pentum IV CPU and 2 GB memory executng SPIN 4.3. Notce that means ether out of memory or more than four hours; column Sze represents the number of network nodes; result Yes means there s no counterexample; result No means there s a counterexample; the verfcaton tmes for PAT and SPIN are measured n seconds. We compare PAT wth the SPIN model checker manly because SPIN targets at smlar systems and t adopts smlar model checkng approaches (.e., automata-based on-the-fly LTL model checkng). Note that there are mprovements on model checkng technques whch have not been ncorporated n SPIN, e.g., on handlng large LTL formulae [10, 11] or on nested DFS [26]. The protocols nclude leader electon for complete networks (LE_C) [6], for rooted trees (LE_T) [9], for odd szed rngs (LE_OR) [13], for network rngs (LE_R) [6] and token crculaton for network rngs (TC_R) [7]. The descrptons of these protocols are bult n the PAT model checker [28]. The property s that eventually always there s one and only one leader n the network,.e., oneleader. Correctness of all these algorthms reles on dfferent notons of farness. For smplcty, farness s appled to the whole system. We remark that event-level farness or strong global farness s requred for these examples. Table 1 Experment results on populaton protocols Model Sze EWF ESF SGF Result PAT SPIN Result PAT Result PAT LE_C 5 Yes Yes 4.7 Yes 4.1 LE_C 6 Yes Yes 26.7 Yes 23.5 LE_C 7 Yes Yes Yes LE_C 8 Yes Yes Yes LE_T 5 Yes Yes 0.2 Yes 0.2 LE_T 7 Yes Yes 1.4 Yes 1.4 LE_T 9 Yes Yes 10.2 Yes 9.6 LE_T 11 Yes Yes 68.7 Yes 65.1 LE_T 13 Yes Yes Yes LE_OR 3 No No 0.2 Yes 11.8 LE_OR 5 No No 1.8 LE_OR 7 No No 21.3 LE_R 3 No 0.1 < 0.1 No 0.2 Yes 1.5 LE_R 4 No 0.3 < 0.1 No 0.7 Yes 19.5 LE_R 5 No 0.8 < 0.1 No 2.7 Yes LE_R 6 No No 4.6 LE_R 7 No No 9.6 LE_R 8 No No 28.3 TC_R 3 Yes < 0.1 < 0.1 Yes < 0.1 Yes < 0.1 TC_R 5 No < 0.1 < 0.1 No < 0.1 Yes 0.6 TC_R 7 No No 0.2 Yes 13.7 TC_R 9 No No 0.4 Yes As dscussed n Secton 2, process-level weak farness s dfferent from event-level weak farness. In order to compare PAT wth SPIN for verfcaton wth event-level weak farness, we twst the models so that each event n populaton protocols s modeled as a process. By a smple argument, t can be shown that for such models, event-level weak farness s equvalent to process-level weak farness. Nonetheless, model checkng wth process-level weak farness n SPIN ncreases the verfcaton tme by a factor that s lnear n the number of processes. By modelng each event as a process, we ncrease the number of processes and therefore unavodably ncrease the SPIN verfcaton tme by a factor that s constant (n the number of events per process for network rngs) or lnear (n the number of network nodes for complete network). SPIN has no support for event-level/process-level strong farness or strong global farness. Thus, the only way to model check wth strong farness or strong global farness n SPIN s to encode the farness constrants as part of the property. However, even for the smallest network (wth three nodes), SPIN needs sgnfcant amount of tme to construct (very large) Büch automata from the property. Therefore, we conclude that t s nfeasble to use SPIN for such a purpose and omt the experment results from the table. We remark that n theory, strong farness can be transformed to weak

12 12 Front. Comput. Sc., 2014, 8(1): 1 16 farness by payng the prce of one Boolean varable [23]. Nonetheless, the property needs to be augmented wth addtonal clauses after the translaton, whch s agan nfeasble. In [4], we carred out some experments on usng the approach n [23] and the results show that t s very neffcent. All of the algorthms fal to satsfy the property wthout farness. The algorthm for complete networks (LE_C) or trees (LE_T) requres at least event-level weak farness, whereas the rest of the algorthms requre strong global farness. It s thus mportant to be able to verfy systems wth strong farness or strong global farness. Notce that the token crculaton algorthm for network rngs (TC_R) functons correctly for a network of sze 3 wth event-level weak farness. Nonetheless, event-level weak farness s not suffcent for a network wth more nodes, as shown n the table. The reason s that a partcular sequence of message exchange whch satsfes event-level weak farness only needs the partcpaton of at least four network nodes. Ths suggests that our mprovement n terms of the performance and ablty to handle dfferent forms of farness has ts practcal value. We hghlght that prevously unknown bugs n mplementaton of the leader electon algorthms for odd-szed rng [13] have been revealed usng PAT. A few conclusons can be drawn from the results n the table. Frstly, n the presence of counterexamples, PAT usually fnds one quckly (e.g., on LE_R and TC_R wth eventlevel weak farness or strong farness). It takes longer to fnd a counterexample for LE_OR manly because there are too many possble ntal confguratons of the system (exactly 2 5N where N s network sze) and a counterexample s only present for partcular ntal confguratons. Secondly, verfcaton wth event-level strong farness s more expensve than verfcaton wth no far, event-level weak farness or strong global farness. Ths conforms to theoretcal tme complexty analyss. The worse case scenaro s absent from these examples (e.g., there are easly mllons of transtons/states n many of the experments). Lastly, PAT s worse than SPIN on LE_R and TC_R wth event-level weak farness. Ths s however not ndcatve as when there s a counterexample, the verfcaton tme depends on the searchng order. PAT outperforms the current practce of verfcaton wth farness. PAT offers comparably better performance on verfcaton wth weak farness (e.g., on LE_C and LE_T) and makes t feasble to verfy wth strong farness or strong global farness. Ths allows us to dscover bugs n systems functonng wth strong farness. Experments on LE_C and LE_T (for whch the property s only false wth no farness) show mnor computatonal overhead for handlng a stronger farness. Table 2 shows verfcaton statstcs of benchmark systems to show other aspects of our algorthm. Notce that the property bounded bypass means a process whch s nterested n gettng nto the crtcal secton wll be n the crtcal secton; the verfcaton tmes for PAT and SPIN are measured n seconds. Because of the deadlock state, the dnng phlosophers model (dp(n) forn phlosophers and forks) does not guarantee that a phlosopher always eventually eats ( eat0) whether wth no farness or strong global farness. Ths experment shows PAT takes lttle extra tme for handlng the farness assumpton. We remark that PAT may spend more tme than SPIN on dentfyng a counterexample n some cases. Ths s both due to the partcular order of exploraton and the dfference between model checkng based on nested DFS and model checkng based on dentfyng SCCs. PAT s algorthm reles on SCCs. If a large porton of the system s strongly connected, t takes more tme to construct the SCC before testng whether t s far or not. In ths example, the whole system contans one large SCC and a few trval ones ncludng the deadlock state. If PAT happens to start wth the large one, the verfcaton may take consderably more tme. Table 2 Experment results on benchmark systems Model Property Result Farness PAT SPIN dp(10) eat0 No No 0.8 < 0.1 dp(13) eat0 No No 9.8 < 0.1 dp(15) eat0 No No 56.1 < 0.1 dp(10) eat0 No SGF 0.8 dp(13) eat0 No SGF 9.8 dp(15) eat0 No SGF 56.0 ms(10) work0 Yes ESF 9.3 ms(12) work0 Yes ESF peterson(3) bounded bypass Yes PWF peterson(4) bounded bypass Yes PWF 1.7 > 671 peterson(5) bounded bypass Yes PWF 58.9 Mlner s cyclc scheduler algorthm (ms(n) forn processes) s a showcase for the effectveness of PAT, n whch we apply event-level strong farness to the whole system. Peterson s mutual exclusve algorthm (peterson(n)) requres at least process-level weak farness to guarantee bounded bypass [29],.e., f a process requests to enter the crtcal secton, t eventually wll. The property s verfed wth processlevel weak farness n PAT and process-level weak farness n SPIN. PAT outperforms SPIN n ths settng as well. 6 Related work Ths work s the full verson of the tool paper about the PAT model checker publshed at CAV09 [30]. In ths artcle, we

13 Yuanje SI et al. Model checkng wth farness assumptons usng PAT 13 present a comprehensve lst of farness notatons and how they are supported effcently n the PAT model checker. The research on categorzng farness/lveness, motvated by system analyzng of dstrbuted or concurrent systems, has a long hstory [2,17,31,32]. A rch set of farness notons have been dentfed durng the last decades, e.g., weak or strong farness n [2], justce or compasson condtons n [17], hyperfarness n [19, 33], strong global or local farness recently n [6], etc. Ths work summarzes a number of farness notons whch are closely related to dstrbuted system verfcaton and provdes a framework to model check wth dfferent farness constrants. Other works on categorzng farness/lveness have been evdenced n [20, 34 36]. Ths work s related to research on system verfcaton wth farness [1,2,6]. In automata theory, farness/lveness s often captured usng the noton of acceptng states. For nstance, an executon of a Büch automaton (whch s an automaton wth justce condtons) must vst at least one acceptng state nfntely often. An executon of a Streett automaton (whch s an automata wth compasson condtons) must nfnte states n a set F f nfntely many states n E s vsted, where E and F are subsets of states. Our model checkng algorthm s related to prevous works on emptness checkng for Büch automata [18, 21] and Streett automata [21 23, 37]. Two dfferent groups of methods have been proposed for checkng emptness of Büch automata,.e., one based n nested DFS [38] and the other based on dentfyng SCCs [21]. As dscussed n Secton 4, nested DFS s not feasble for verfcaton wth strong farness. Smlar to [21], our work s based on Tarjan s algorthm for dentfyng SCCs. We generalze the dea to handle dfferent farness constrants. In [22], an algorthm for checkng emptness of Streett automata s proposed. In ths work, we apply the dea to the automata-based model checkng framework and generalze t to handle dfferent farness constrants. In ths way, our algorthm ntegrates the two algorthms presented n [21, 22] and extends them n a number of aspects to sut our purpose. Furthermore, model checkng algorthms wth strong farness have been proposed n [21] and [37]. In both works, a smlar prunng process s nvolved. Besdes, some research has been done on combnng farness and state reducton technques, e.g., combnng symmetry reducton wth global farness assumptons [39], applyng partal order reducton durng model checkng wth farness assumpton [4], etc. Ths work s also related to prevous work on CTL model checkng wth farness, whch also reles on dentfyng a far strongly connected component. For nstance, the basc fxedpont computaton algorthm for the dentfcaton of far executons was presented n [40] and ndependently developed n [41] for far CTL. Nonetheless, our algorthm s desgned for automata-based on-the-fly model checkng, wth a varety of farness constrants ncludng the recently emerged strong global farness. Dfferent from the prevous works [42,43] on symbolc model checkng wth farness, our approach s desgned for LTL model checkng. Ths work s also related to the recent work on desgnng a strong far scheduler for concurrent programs testng presented [24]. The far scheduler presented [24] generates only partal far executons, whch worksfortestng butnotformalverfcaton. In addton, ths work s remotely related to the work on handlng large LTL formulae [11] as well as our prevous work on verfyng concurrent systems [44 46]. 7 Concluson and future work In summary, we developed a method and a self-contaned toolkt for (dstrbuted) system analyss wth a varety of farness constrants. We showed that our method and the toolkt are effectve enough to prove or dsprove not only benchmark systems but also newly proposed dstrbuted algorthms. We are actvely developng PAT. One future work of partcular nterest s to nvestgate refnement wth farness constrants. Refnement checkng s an alternatve way of system verfcaton. Instead of showng that a system mplementaton satsfes some crtcal property, refnement checkng may be used to show that the mplementaton satsfes ts own specfcaton (often n the same language). The man motvaton s that refnement wth a far scheduler or n a dstrbuted system s dfferent from refnement under schedulng wth no farness. For nstance, trace refnementwth event-levelweak farness prevents removng a transton whch s always enabled and trace refnement wth strong global farness prevents removng a nondetermnstc choce. The consequence of a far scheduler over program refnement s worth nvestgatng. In order to handle non-trval systems, effcent algorthms for refnement checkng wth farness must be developed. Another lne of future work s to nvestgate how to verfy nfnte-state systems wth farness. For nstance, how to ntegrate our method wth abstracton technques whch are used to buld fnte state models. In partcular, we wll nvestgate abstract schema whch are proposed for parameterzed systems so that our method can be extended to verfy populaton protocols wth many or even nfnte network nodes. Acknowledgements Ths work was partally supported by the research

14 14 Front. Comput. Sc., 2014, 8(1): 1 16 grant NAP project Formal Verfcaton on Cloud (M ), Automatc Checkng and Verfcaton of Securty Protocol Implementatons (M ), and the Natonal Natural Scence Foundaton of Chna (Grant Nos , ). References 1. Gannakopoulou D, Magee J, Kramer J. Checkng progress wth acton prorty: s t far? In: Proceedngs of the 7th ACM SIGSOFT Symposum on the Foundatons of Software Engneerng. 1999, Lamport L. Provng the correctness of multprocess programs. IEEE Transactons on Software Engneerng, 1977, 3(2): Kurshan R P. Computer-aded Verfcaton of Coordnatng Processes: The Automata-Theoretc Approach. Prnceton Unversty Press, Sun J, Lu Y, Dong J S, Wang H H. Specfyng and verfyng eventbased farness enhanced systems. In: Proceedngs of the 10th Internatonal Conference on Formal Engneerng Methods. 2008, Sun J, Lu Y, Roychoudhury A, Lu S, Dong J. Far model checkng wth process counter abstracton. FM 2009: Formal Methods, 2009, Fscher M J, Jang H. Self-stablzng leader electon n networks of fnte-state anonymous agents. In: Proceedngs of the 10th Internatonal Conference on Prncples of Dstrbuted Systems. 2006, Anglun D, Aspnes J, Fscher M J, Jang H. Self-stablzng populaton protocols. In: Proceedngs of the 9th Internatonal Conference on Prncples of Dstrbuted Systems. 2005, Anglun D, Fscher M J, Jang H. Stablzng consensus n moble networks. In: Proceedngs of the 2006 Internatonal Conference on Dstrbuted Computng n Sensor Systems. 2006, Canepa D, Potop-Butucaru M. Stablzng Token Schemes for Populaton Protocols. Computng Research Repostory, 2008, abs/ Rozer K Y, Vard M Y. LTL Satsfablty Checkng. In: Proceedngs of the 14th Internatonal SPIN Workshop. 2007, Hammer M, Knapp A, Merz S. Truly on-the-fly LTL model checkng. In: Proceedngs of the 11th Internatonal Conference on Tools and Algorthms for the Constructon and Analyss of Systems. 2005, Pang J, Luo Z Q, Deng Y X. On automatc verfcaton of selfstablzng populaton protocols. In: Proceedngs of the 2nd IEEE Internatonal Symposum on Theoretcal Aspects of Software Engneerng. 2008, Jang H. Dstrbuted Systems of Smple Interactng Agents. PhD thess, Yale Unversty, Sun J, Lu Y, Dong J S, Chen C Q. Integratng specfcaton and programs for system modelng and verfcaton. In: Proceedngs of the thrd IEEE Internatonal Symposum on Theoretcal Aspects of Software Engneerng. 2009, Hoare C A R. Communcatng Sequental Processes. Internatonal Seres on Computer Scence. Prentce-Hall, Chak S, Clarke E M, Ouaknne J, Sharygna N, Snha N. State/eventbased software model checkng. In: Proceedngs of the 4th Internatonal Conference on Integrated Formal Methods. 2004, Lehmann D J, Pnuel A, Stav J. Impartalty, justce and farness: the ethcs of concurrent termnaton. In: Proceedngs of the 8th Colloquum on Automata, Languages and Programmng. 1981, Holzmann G J. The SPIN Model Checker: Prmer and Reference Manual. Addson Wesley, Lamport L. Farness and hyperfarness. Dstrbuted Computng, 2000, 13(4): Pnuel A, Sa ar Y. All you need s compasson. In: Proceedngs of the 9th Internatonal Conference on Verfcaton, Model Checkng and Abstract Interpretaton. 2008, Geldenhuys J, Valmar A. More effcent on-the-fly LTLverfcaton wth Tarjan s algorthm. Theortcal Computer Scence, 2005, 345(1): Henznger M R, Telle J A. Faster algorthms for the nonemptness of streett automata and for communcaton protocol prunng. In: Proceedngs of the 5th Scandnavan Workshop on Algorthm Theory. 1996, Kesten Y, Pnuel A, Ravv L, Shahar E. Model checkng wth strong farness. Formal Methods and System Desgn, 2006, 28(1): Musuvath M, Qadeer S. Far stateless model checkng. In: Proceedngs of the ACM SIGPLAN 2008 Conference on Programmng Language Desgn and Implementaton. 2008, Baer C, Katoen J. Prncples of Model Checkng. The MIT Press, Schwoon S, Esparza J. A note on on-the-fly verfcaton algorthms. In: Proceedngs of the 11th Internatonal Conference on Tools and Algorthms for the Constructon and Analyss of Systems. 2005, Tarjan R. Depth-frst search and lnear graph algorthms. SIAM Journal on Computng, 1972, 2: Lu Y, Pang J, Sun J, Zhao J. Verfcaton of populaton rng protocols n pat. In: Proceedngs of the 3rd IEEE Internatonal Symposum on Theoretcal Aspects of Software Engneerng. 2009, Alagarsamy K. Some myths about famous mutual excluson algorthms. SIGACT News, 2003, 34(3): Sun J, Lu Y, Dong J S, Pang J. PAT: towards flexble verfcaton under farness. Lecture Notes n Computer Scence, 2009, 5643: Apt K R, Francez N, Katz S. Apprasng farness n languages for dstrbuted programmng. Dstrbuted Computng, 1988, 2(4): Francez N. Farness. Texts and Monographs n Computer Scence. Sprnger-Verlag, Atte P C, Francez N, Grumberg O. Farness and hyperfarness n multparty nteractons. Dstrbuted Computng, 1993, 6(4): Quelle J P, Sfaks J. Farness and related propertes n transton systems a temporal logc to deal wth farness. Acta Informatcae, 1983, 19: Kwatkowska M Z. Event farness and non-nterleavng concurrency. Formal Aspects of Computng, 1989, 1(3): Völzer H, Varacca D, Kndler E. Defnng farness. In: Proceedngs of the 16th Internatonal Conference on Concurrency Theory. 2005, Latvala T, Heljanko K. Copng wth strong farness. Fundamenta Informatcae, 2000, 43(1 4): Courcoubets C, Vard M Y, Wolper P, Yannakaks M. Memoryeffcent algorthms for the verfcaton of temporal propertes. Formal Methods n System Desgn, 1992, 1(2/3): Zhang S, Sun J, Pang J, Lu Y, Dong J. On combnng state space reductons wth global farness assumptons. FM 2011: Formal Methods, 2011,

15 Yuanje SI et al. Model checkng wth farness assumptons usng PAT Lchtensten O, Pnuel A. Checkng that fnte state concurrent programs satsfy ther lnear specfcaton. In: Proceedngs of the 12th ACM SIGACT-SIGPLAN Symposum on Prncples of Programmng Languages. 1985, Emerson E A, Le C L. Modaltes for model checkng: branchng tme logc strkes back. Scence of Computer Programmng, 1987, 8(3): Hardn R H, Kurshan R P, Shukla S K, Vard M Y. A new heurstc for bad cycle detecton usng BDDs. Formal Methods n System Desgn, 2001, 18(2): Klarlund N. An n log n Algorthm for Onlne BDD Refnement. In: Proceedngs of the 9th Internatonal Conference on Computer Aded Verfcaton. 1997, Dong J S, Lu Y, Sun J, Zhang X. Verfcaton of computaton orchestraton va tmed automata. In: Proceedngs of the 8th Internatonal Conference on Formal Engneerng Methods. 2006, Dong J S, Hao P, Sun J, Zhang X. A reasonng method for tmed CSP based on constrant solvng. In: Proceedngs of the 8th Internatonal Conference on Formal Engneerng Methods. 2006, Sun J, Lu Y, Dong J S. Model checkng csp revsted: ntroducng a process analyss toolkt. In: Proceedngs of the 3rd Internatonal Symposum on Leveragng Applcatons of Formal Methods, Verfcaton and Valdaton. 2008, Yuanje S s a PhD canddate n the College of Computer Scence at Zhejang Unversty, Chna. He receved BS n Software Engneerng from Zhejang Unversty n Chna. Hs current research nterests nclude software engneerng and formal verfcaton, n partcular, model checkng and software relablty evaluaton technques. Jun Sun receved BS and PhD degrees n Computng Scence from Natonal Unversty of Sngapore (NUS) n 2002 and In 2007, he receved the prestgous LEE KUAN YEW postdoctoral fellowshp n School of Computng of NUS. Snce 2010, he joned Sngapore Unversty of Technology and Desgn (SUTD) as an assstant professor. He was a vstng scholar at MIT from Jun s research focuses on software engneerng and formal methods, n partcular, system verfcaton and model checkng. He s the co-founder of the PAT model checker. Yang Lu graduated n 2005 wth a BS of Computng n the Natonal Unversty of Sngapore (NUS). In 2010, he obtaned hs PhD and contnued wth hs post doctoral work n NUS. Snce 2012, he joned Nanyang Technologcal Unversty as an assstant professor. Hs research focuses on software engneerng, formal methods and securty. Partcularly, he specalzes n software verfcaton usng model checkng technques. Ths work led to the development of a stateof-the art model checker, Process Analyss Toolkt. Jn Song Dong receved BS and PhD degrees n Computng from Unversty of Queensland, Australa n 1992 and From , he was Research Scentst at CSIRO n Australa. Snce 1998 he has been n the School of Computng at the Natonal Unversty of Sngapore (NUS) where he s currently Assocate Professor and a member of PhD supervsors at NUS Graduate School. He s on the edtoral board of Formal Aspects of Computng and Innovatons n Systems and Software Engneerng. Hs research nterests nclude formal methods, software engneerng, pervasve computng, and semantc technologes. Jun Pang receved hs PhD degree from Free Unversty of Amsterdam, Netherlands. Currently, he s a senor researcher wth the Faculty of Scence, Technology and Communcaton n the Unversty of Luxembourg. Hs man research areas nclude formal methods, model checkng, securty and prvacy. Shao Je Zhang receved her PhD degree n computer scence from Natonal Unversty of Sngapore n Currently, she s a postdoctoral researcher n Sngapore Unversty of Technology and Desgn, Sngapore. Her current research nterests nclude software engneerng and formal verfcaton, n partcular model checkng and state reducton technques.

16 16 Front. Comput. Sc., 2014, 8(1): 1 16 Xaohu Yang receved hs PhD degree of Computer Scence at Department of Computer Scence and Technology n Zhejang Unversty, Chna n He s currently a professor n College of Computer Scence, Zhejang Unversty, Chna. Hs man research areas nclude very large-scale nformaton system, software engneerng, and fnancal nformatcs.