Home

A Method of Bounded Model Checking for a Temporal Epistemic

Contents

1. where R is defined as per the Kripke semantics given previously with the one addition that it maps the input state to a unique successor state for a certain behaviour through the model It should be noted that R s s and R 1 s R R s 21 2 Computational Tree Logic Computational Tree Logic CTL was introduced by Clarke and Emerson in 1980 15 CTL is a branching time logic and is able to express the existence of and properties upon runs of a system 1Adapted from 32 see also 44 10 CTL Syntax Definition 3 The syntax of CTL is defined as follows Vp AP pis a formula If vis a formula then g is a formula Ify and wy are formulae then y V w is a formula If is a formula EX is a formula If visa formula EGy is a formula Ify andy are formulae then E pUy is a formula Syntax of CTL in BNF p p ny eV p EXy EG E pU From the above definition we can see that CTL has four temporal operators EXy EGy E pUy From these we can further define extra temporal operators AXy AEX EFy ae trueUy AGY amp EF def A PUY E YUng A 77 AEG AFy trueUy Semantics of CTL Definition 4 A path 16 in a Kripke structure M is an infinite series of states 7 s 51 such that Vi gt 0 si Si 1 ER It should be noted that in comparison to LTL R where used here may return the set of all successor states and not a particul
2. Construct iota modal_formula init new modal_formula new atomic_proposition amp str Where we re going to store the results BDD result for modal_formula_p_pair_vector iterator iter bmc_formulae gt begin iter bmc_formulae gt end Dereference the iterator modal_formula_p_pair temp modal_formula_p_pair iter Construct iota gt phi modal_formula f new modal_formula 4 init temp second Check the implication result f gt check_formula Delete the formulae if f delete f Tf phi holds in the initial state if result reach We ve found a counterexample to the original formulae We save it in the vector of falsified formulae bmc_false_formulae gt push_back temp And remove it from the formulae to check and update iter to be the next item in the vector iter bmc_formulae gt erase iter continue Move the iterator on iter Delete the init formula if init delete init 103 Figure A 5 The first half of the BMC method in MCMAS void bdd_bmc void The current reachable states are the initial states reach in_st ql is the new set of next states BDD ql bddmgr gt bddZero Initial next states is the initial states BDD nextl in_st Start at a depth of 0 int k Q Whilst we still have formulae to check while bmc_formulae gt empty Check them with re
3. 68 Although CUDD can adjust the size of the cache during execution having too small a cache will reduce the number of unique BDD functions that can be stored in it meaning that useful results will often be overwritten This also causes an increase in the number of cache misses Each time the cache as well as the unique tables fill up CUDD attempts to garbage collect unreferenced results from the cache As such having too small a cache then results in an increased number of garbage collections When CUDD is required to create a new internal node and the number of nodes exceeds a given threshold CUDD attempts automatic variable reordering When performing BDD based BMC we are required to store a number of intermediate working results all of which are represented as BDDs using CUDD nodes and are stored in the unique table This means that BMC also affects the number of variable reorderings that CUDD performs Table 5 3 The number of asynchronous reorderings and garbage collections performed by CUDD Model Reorderings Garbage Collections T M B Orginal BDD BMC Original BDD BMC 6 II I2 9 I3 55 17 26 For the same models as previously Table 5 3 illustrates the number of variable reorderings and garbage collections that CUDD performed during BMC In some cases BDD based BMC required over four times as many variable reorderings and twice as many garbage collections when compared to MCMAS s defa
4. is valid along a path of length k in the model M The final stage is to create M y M A llm This is then passed to a satisfiability solver 2 3 6 Model Checking Multi Agent Systems Interpreted Systems as Boolean Formulae Given a model of an interpreted system Msg see Section 2 2 2 the number of Boolean variables used to represent local states of an agent is as follows no i logs Lil This means that a global state can be represented with the following number of Boolean variables N gt nv i Vic Agents 20 The evaluation function is simply a mapping of states of variables in AP so this can work on the Boolean variables representing each state The protocols can also be expressed in the same way The transition relation t for each agent can be represented as a set of conditionals which when satisfied enable a transition for an agent between two local states For more details see 52 The model checking algorithm in Section 2 3 6 requires a representation R of the global transition relation between two global states g g 53 Ri g g iff Vi Agents Ja P li g A ti g a 9 Model Checking CTLK The algorithms from the section below have been adapted from 52 53 Algorithm 7 Saterix y Formuta set of STATE 1 if Y E AP then 2 return L y else if p y then return G SaTerix Y1 G is the set of all states in the model else if p EXy then retu
5. eration 2 xX X lt Z Inrr s1 Z Init Z Y lt Inrr Yet EF y 0 Again it can be seen that the fixed point methods work appropriately when dealing with models with truncated paths 5 1 4 SATEU To calculate the E pU W stores p Y stores and X the set of all reachable states Figure 5 6 Checking E pUw Figure 5 7 The labelling function and existential pre image function for Figure 5 1 4 L y iInrr s1 s2 LW s3 prej Inir pres si Init pres s2 si pres s3 82 83 Depth o Depth 1 W e Inir W lt Init W lt Inrrt s1 W lt In17 s1 X e Inir X lt X lt Inrt s X ve Depth 2 W lt IniT 51 52 W lt In17 51 S2 X Inrt 51 52 X Y Y E yU 2 0 Depth 3 W e Inrt 51 52 W lt Inrt 51 52 W lt InrT 51 52 W e INIT 51 so X IniT 51 52 X s3 X s2 s3 X s1 52 S3 Y s3 Y s2 s3 Y In17 51 52 53 Y INIT 51 52 S3 Iteration 4 W e Inrr 51 S2 X Init 1 52 s3 Y In iT S1 52 s3 JE pUg 3 IN1T 51 52 s3 64 5 2 Satz on Truncated Paths Figure 5 8 A model showing the local state equivalence Figure 5 9 The labelling function and existential pre image and knowledge pre image functions for Fig relation ure 5 2 a eee eee Depth o L y s2 pr
6. 75 is a specialised model checker for the automatic verification of certain aspects of a modelled multi agent system It supports CTLK meaning that it is able to check standard temporal formulae and those dealing with epistemic modalities It is based around the symbolic method introduced in 52 using an external BDD library It is based around the Colorado University Decision Diagram CUDD 68 package In a similar style to NuSMV MCMAS is also able to act in an interactive way and allows for the user to interactively select the joint action that should be performed next MCMaAS supports the creation of counterexamples to universal formulae and witnesses to existential formulae MCMAS supports its own dedicated programming language based on the interpreted systems for malism 21 ISPL As per the interpreted systems formalism MCMAS represents the global state as a BDD composed of each local state for each agent ISPL Interpreted Systems Programming Language MCMAS accepts descriptions of multi agent systems in the form of ISPL files These files contain a multi agent system in the form of a list of agents each with their own description and a set of formulae that the user wishes to check The structure of ISPL files is roughly based upon the work presented in 4 Syntax of an ISPL file 54 Agent The name that will be used by MCMAS to represent the agent LState These are the states that are used to define
7. The Dining Cryptographers Bounded Model Checking Resource Usage Figure 5 23 Memor Y me LLL LZ Ti MGW th see States Dep 100 SKK KKK SENSO x Ka WiW e W vw w w ww l III 33993923R 38330233922 38322322S ISSR Ki WW W WYWG 140 120 100 80 60 40 20 0 SIDINOSIY jo Yocl Yocl Formula The Software Development Example Bounded Model Checking Resource Usage Figure 5 24 LLL L 2 QO th se DE oges 0 84 ae are Se lt x x x x x xs xs x e e e O 2 a e o0 Ko a H H H SIDINOSIY jo Yspl Formula 79 5 4 4 Length of Counterexample Found Our attempt to implement BDD based bounded model checking on top of an existing model checker allows us to gain some functionality for free in this case counterexample generation MCMAS is already capable of generating counterexamples and witnesses to ACTLK ECTLK formulae It can do so by printing out the list of states and the joint actions between displaying a trace through the model that invalidates the property To deem counterexample generation from BMC successful we felt we had two goals to satisfy 1 Groce et al 22 make the distinction that bounded model checkers often produce counterexamples that are difficult to unde
8. The local states of the agent in the interpreted systems are as follows 29 Liraini away wait j tunnel Liraing away2 waite tunnels Leontroller red green The local states take the obvious meanings in the context The global state as usual in the interpreted systems is comprised of all of the local states for each agent i e G Lirain X Ltraing X Lcontroller In the scenario presented in 31 29 30 the initial state is taken to be 1 away green away2 The local transition structures with respect to the joint actions for the two trains can be seen in fig 2 11 Which agents are affected when a joint action takes place along with their pre and post states enabling that action can be seen in table 2 12 The joint actions from the table 2 12 can be very roughly translated as follows The properties in the paper are specified with O and presented in a hybrid Rebeca logic C like notation 31 Figure 2 10 An automaton modelling a train from the Train Gate Controller model 1 23 Leaving the tunnel Arrived at the tunnel A Lieur GREEN Figure 2 11 The local transition structures for the two trains and the controller 29 CONTROLLER Rep 32 a represents TRAINI signalling the controller that it wishes to the enter the tunnel similarly for agwith TRAIN2 ag corresponds to the joint action allowing Trarn to enter the tunnel again si
9. trainl_in_tunnel or train2_in_tunnel EF TRAIN1_IN_TUNNEL TRAIN2_IN_TUNNEL This formula could be written in a more intuitive way as AG TRAIN1_IN_TUNNEL TRAIN2_IN_TUNNEL 57 We have used De Morgan s law to present a specification that adheres to the requirement that in ACTLK negation may only appear in front of atoms 57 Formula 3 Yre6c3 When a train is in the tunnel it knows that another train is not ACTLK AG TRAIN1_IN_TUNNEL Kain 7TRAIN2_IN_TUNNEL ECTLK EF TRAIN1_IN_TUNNEL A Kirar TRAIN2_IN_TUNNEL ISPL AG trainl_in_tunnel gt K Train1 train2_in_tunnel Formula 4 Yrec4 Trains always know that they have exclusive use of the tunnel ACTLK AG Kram 7TRAIN _IN_TUNNEL V TRAIN2_IN_TUNNEL ECTLK EF Kram TRAIN1_IN_TUNNEL TRAIN2_IN_TUNNEL ISPL AG K Train1 trainl_in_tunnel or train2_in_tunnel Formula 5 recs Trains are aware that there is a gap between leaving and the next train entering the tunnel ACTLK AG TRAIN1_IN_TUNNEL K ra AX 7TRaing_IN_TUNNEL ECTLK ISPL AGCtrainl_in_tunnel gt K Trainl AX train2_in_tunnel EF TRAIN1_IN_TUNNEL A Kran EX Tratn2_IN_TUNNEL Parameterised The formulae Yy c3 and Precs can be parameterised in a similar way to 29 for a system composed of N trains When a train is in the tunnel it knows that no other train in the whole system is in the tunnel i 1 Yrec3 N
10. 0 if y is of the form EXa or EGa then y a 1 if y is of the form a V 8 a A B or E aU then y a 8 1 Definition 19 Validity of bounded semantics An ECTL formula is valid in a k model Mg E iff Ve T Mk LE p From the bounded semantics above it can be seen that Mg s F vy implies VL L gt k M s E y Simple induction then shows us that Mg s F y implies M s E y Another property from above proof can be found in 48 is that if M s E y then Mpg s E y when k l Creating the propositional formula The function States Path generates the set of states from the k model that can be reached with a path of length k States Path s S da Paths Ji lt k n i s Definition 20 Sub models of M 48 Mpg S T Paths L is a k model of M The structure Mg S T Paths L is a sub model of My such that Paths C Paths S States Paths and L L s a reduction of the labelling function to only contain states in S Definition 21 The function f CTL Formula N 48 fP f 7P 0 fil V w max f uC 18 fep Y f f f EXy f 1 EGY k 1 f y 1 fe EUY k f A 1 Algorithm 6 BMC M Kripke Structure Y ACTL Formuta 48 x p Ww y is an ECTL formula 2 for k 1to M do My lt k model of M Select sub models of M of M with Path lt flp MP
11. III 3 ERIK woo KEES Pee osx 0 84 a2 Bn eee o vA EN Z x x x x x x x x O e e O e 0 t a O o0 Ko a H H H SIDINOSIY jo 12 15 I8 WORKING Breaking Threshold of Train 9 6 72 SX sq w LLLA emor Time States Depth zez 100 M KKK KKK Mw Y me ZZL th aa emor Ti pa ep 100 KG M WORKING WORKING ANIL iA N 5 Bounded Model Checking Resource Usage SR ae Z sete asen SIS SSE BDCbBn B 5 3 S38 presen SKI LL LL NLL Breaking Threshold of Train Bounded Model Checking Resource Usage RSSICON Satateseeanatesonnnesesotatereneneesenens SRR RR RO UMMM KK KKK 140 I20 Figure 5 14 Resource usage in a model with three type 1 trains and a maximum counter of 7 Yrec3 100 80 F 60 gt 40 H 20 F 0 SIDINOSIY jo 140 I20 Figure 5 15 Resource usage in a model with three type 2 trains and a maximum counter of 7 Yrec3 100 80 F 60 gt 40 H 20 F 0 SIDINOSIY jo 5 3 Breaking Threshold of Train 73 The final four graphs for the faulty train gate controller model Figure 5 16 to Figure 5 19 illustrate the difference in either memory re
12. In a nutshell the problem of model checking is simply given a description of a finite state system and property expressed as a logical formula does the system satisfy that property If an error is located the process will return a counterexample showing the steps in which the error state was reached Model checking is an automated technique that given a finite state model of a system and a logical property systematically checks whether this property holds for a given initial state in that model 32 Model checking is an effective technique to expose potential design errors 3 The remainder of this section focuses on CTL model checking 2 3 1 Explicit Model Checking The principle behind CTL model checking is given a model M S Z R L to label each state s S with all of the formulae that are valid in s Then to check if a formula is valid in s M s F iff s is labelled with y To decide if the model M satisfies the formula y is as simple as checking if all the initial states are in the set of states that satisfy p That is ME piff I C sEeS M sF p The notation y is used to represent the set of states in the model in which the formula holds yp se S M sF vy II The algorithms below have been adapted from 32 24 50 For further information the reader is advised to consult these texts Algorithm 1 CTL Model Checking 3 x for alli lt p do 2 for all x Sus y
13. Linear These logics allow for the specification of properties of execution sequences of systems e g LTL Branching These logics allow for the specification of the choices available to the system during execu tion e g CTL For the continuation of this document AP is used to represent the set of atomic propositions 2 1 1 Linear Temporal Logic LTL syntax Definition 1 The syntax of LTL formulae is as follows Vp AP pisa formula If y is a formula then g is a formula Ify andy are formulae then V Y is a formula If is a formula Xv is a formula Ify and w are formulae then pUw is a formula From the above we can see that the only temporal logic operators that are used in LTL are X neXt and U Until LTL syntax can also be given in Backus Naur Form BNF where p AP gr ple o V y Xy pUy The temporal operators G always Globally and F eventually Future can be further defined as Fy trueUp Gy det AFA As a note to the reader F and G are sometimes written as and O respectively LTL semantics Definition 2 Semantics of LTL Let p E AP M be a Kripke structure S Z R L s E S p Y are LTL formulae Satisfaction F is defined as follows M sFp iff peEL s M sEnyp iff M s M sEypVvw iff M sE y or M s Ey M sEpAw iff M s F p and M s Ey M s E Xy iff R s Fy M s E pUy iff Jj gt 0 R s E p A VO lt k lt j Ri s Fy
14. They discuss the idea of not only forward bounded model checking from the initial set to the target set Fwp Ver Algo rithm 12 but also the converse working from the pre image of the error set BwDBMC They implement their algorithms into a model checker Forward Backward Verifier FBV using CUDD which they then compare against the SAT based BMC implementation in NuSMV 10 Whilst only considering safety prop erties their results seem to suggest that BDD based BMC scales better with an increasing bound of k Algorithm 12 FwoVer TR S T i k 0O 2 Ry New S 3 while New 4 do a if T New 40 then 5 return CounTEREx R 6 endif 7 kek l1 8 Next Ime TR Next 9 New lt Next Ry_ to Ry Rk 1 New 11 end while 12 return pass These results were backed up by Amal et al 2003 2 when they undertook a more thorough comparison of BMC methods It should be noted here that unlike the work by Cabodi et al and Copty et al Amal et al do not provide any form of algorithm nor any implementation specific information Their work presents three BMC approaches BDD based BMC The paper looks at liveness properties when using a bounded reachability check we assume their approach is similar to Algorithm 12 One of the cases in which their algorithm terminates is when an error state is reached Explicit State BMC They perform explicit state model checking but kill all
15. propositional formula of the transition relation of all the sub models of M M pl M2 A llm Check the satisfiability of M p 3 4 5 6 y M propositional formula of the translation of p over all the sub models of Mi Z 8 9 end for Construction of the propositional formula M p is as follows A symbolic representation is used so that the S C 0 1 where n log S Each state s S can therefore be represented as a vector of propositional variables that hold at that state s s 1 s n sli AP A k path can then be represented as a vector of length k of these states Tk s0 8k LL C N is a finite set of a numbers M92 constrains L L symbolic k paths valid in Mg For j LLP the j symbolic k path is denoted as Wo j Wk j where wi j Vi 0 k are state variables The function lit 48 is defined as follows Oo p lit 1 p p The following are propositional formulae based upon the usual definition of a Kripke structure where w v are state variables 48 IL w if N lit s i wii i 1 T w v if wv ER p w if pe L w p AP H w v iff w v Lejl T wki wij I w encodes the initial state Z of the model s i 1 is encoded by wii and s i 0 is encoded by wwii T w v encodes a transition between two states i e T w v iff wRv p w encodes a proposition of p of ECTL H w v represents logical equivalence b
16. that many times better or worse than the conventional methods As noted in the previous chapter in the majority of cases in which bounded model checking is used in real systems it is the case that there are errors to be found which is the reason for performing model checking in the first place In these cases it should be immediately obvious that using a bounded model checking approach is a preferential selection 6 1 3 Limitations Challenges and Applications When used without reordering and as shown in Section 5 4 5 when performing bounded model checking MCMAS can now check models in which it would have previously failed This shows us that the implementa 89 tion can show the expected benefits and that the requirement of exploring less states results in a lower memory usage The problem arises when reordering is enabled as shown in Section 5 4 1 When comparing our bounded implementation we can see that the extra processing checks required for performing bounded model checking are completely unfavourable We feel that this is an unfair comparison due to the majority of optimisations present in a library such as CUDD having been developed and researched with conventional model checking in mind With this in mind it is highly unsurprising that we under perform 6 2 Further Work 6 2 1 Adding a Visualiser to MCMAS Currently there is no way to visualise the internals of MCMAS during execution this means that there could be
17. 4 dA Satg on Truncated Paths 4 4 4 44834 49h 495 5 2 1 Correctness of the Algorithm Satz Model Checking of ASCTLK with Seed States Performance and Benchmarking 04 5 4 1 An Initial Investigation 44 5 4 2 The Faulty Train Gate Controller 5 4 3 MCMASo 9 8 5 Examples 2445 5 4 4 Length of Counterexample Found 5 4 5 Stress Testing MCMAS 44 Evaluation of One Shot BMC 0 Evaluation of Distributed MCMAS 5 6 1 Depth of Seed States baa ys eee we KG 5 6 2 Number of Slaves 20 00005 5 6 3 Disk Space Overhead i444 449 su oo Qualitative Evaluation 2 6 eee eee eee 5 7 1 Effectiveness of Deliverables 5 7 2 Elegance of Solution 4 s 44 4s 4 4 5 733 Scalability sss eas Oe ee Be ee ee oS 6 Conclusions 6 1 Project Review 2 ee rasa irtok na 6 1 1 Contributions s gt s ss esrsrs erans 6 1 2 COmMparisons s eses eses eee ee ertt 6 1 3 Limitations Challenges and Applications Further Work eea rarae Siw ER E A 8 vi 4I 41 41 42 44 45 45 48 48 48 49 50 54 54 54 55 56 61 61 61 62 63 64 65 65 66 67 67 70 76 80 82 82 83 83 86 86 87 87 87 87 89 89 89 89 89 90 6 2 1 6 2 2 6 2 3 6 2 4 6 2 5 6 2 6 6 2 7 6 2 8 Bibliography Web References A BMC Implementation in MCMAS Adding a Visualiser to MCMAS Counterexample Generation for K Common and Dis
18. 68132260 68132260 70072 198678532 1157876 114868452 114868452 166481 39705828 1157876 43777924 43777924 14379945 Table 5 12 A comparison between BMC and distributed bounded model checking at a seed state generation depth of 4 O Deas Memory Time Seats We can see in Table 5 12 that when we generate deeper seeds this results in reaching a counterexample more quickly because there are now less iterations required until a counterexample can be found This is also mirrored across memory and states Depth 5 Table 5 13 e resource usage of distributed bounded model checking at a seed depth of 5 Pc Miser E E E Model Memory States Memory States Memory Memory States Memory States 70396964 1824660 64144676 64144676 71396 198678532 1659940 867 113094884 113094884 165396 39705828 1824660 43859860 43859860 51017544 Table 5 14 A comparison between BMC and distributed bounded model checking at a seed state generation depth of 5 Decrease Model Memory Time Sere 0 559 0 983 4 134 1 721 0 001 0 001 The number of states explored for distributed bounded model checking when the formulae cannot be falsified stands out in Table 5 13 At a depth of 5 the master instance generates 1227 seeds This means 85 that to be able to infer that the property is never falsified over the entire model bounded model checking is performed until a fixed point is reached f
19. AG Trannon runner Kran N 7TRrainj_IN_TUNNEL j 1 N N 7Trainj_IN_TUNNEL j i 1 When a train is in the tunnel it knows that no other train in the whole system will enter the tunnel in the next evolution i 1 Precs N AG Trani inrunner Kram A Ax Taarnj im runner N j l N AX Tranny im ronner j i 1 We have developed an ISPL generator for this model allowing us to generate models of an arbitrary size containing a configurable number of any of the three types of trains with a configurable breaking depth The generator creates all of the formulae discussed here In these models the controller is modelled as part of the environment Auto generated ISPL code for a controller modelled by the environment in a train gate controller model with 2 trains a maxcounter of 20 and breakingdepth of 10 can be found in Figure 4 17 The generated ISPL for a type 1 faulty train in the same model can be found in Figure 4 18 Similar to a1 from 30 7Or trains are aware that the controller allows for a gap between one train leaving and the next entering 58 Figure 4 17 An example controller environment Agent Environment Vars lights red green trainl_waiting boolean train2_waiting boolean counter Q 2 end Vars Actions enterl enter2 idle Protocol lights green and trainl_waiting true enterl lights green and train2_waiting true enter2
20. BMC depth the algorithm has explored to Tf we reach the seed depth and still have formulae to falsify if k seed_depth amp amp bmc_formulae gt empty DDDMP specifics Dddmp_VarMatchType varmatchmode DDDMP_VAR_MATCHIDS Dddmp_VarInfoType varoutinfo DDDMP_VARIDS int status 0 Identifier for each state int state_iter Q While we still have next states while nextstates bddmgr gt bddZero Pick a random node which is the state in v from the set of next states BDD singlenextstate nextstates PickOneMinterm v Tf the state we ve chosen _isn t_ valid then skip over it if is_valid_state singlenextstate v continue Otherwise Set up the file name sprintf filename s state_ 04d out working_directory state_iter Get the decision diagram representing that node DdNode a singlenextstate getNode Write the node out to a file status Dddmp_cuddBddStore bddmgr gt getManager NULL a NULL NULL DDDMP_MODE_TEXT varoutinfo filename NULL Check if we were unable to write the node out if status 1 cout lt lt DDDMP failed cout lt lt we were unable to write the node to a file cout flush exit 1 Remove the current state from the set of next states set minus nextstates singlenextstate Increment our state identifier state_iter 52 Figure 4 10 Sequence diagram for the distributed bounded model che
21. Mrs G T Il 1 n V where G is the set of reachable global states T C Gis the set of initial states II is the set of possible runs in the system is the binary relation for every agent i g i g iff l g 1 g As before this represents that the global state is indistinguishable for the agent i i e the local state of the agent is invariant between the two global states V is the valuation function for the propositional atoms 2 2 3 A Logic of Knowledge Interpreted systems provide computationally grounded semantics that has been used to model knowledge 56 CTLK is an epistemic logic it allows for the expression of properties that contain a notion of knowledge Syntax of CTLK Definition 11 BNF definition of the CTLK language Y p y p Vy EXy EGy E pUy Kip Semantics of CTLK The epistemic modality K is used to represent knows in logical form agent i knowing y is written as K y As such TS g F Kig ifYg G g i g implies TS g F yp CTLK is enriched with a further two epistemic operators for a set of agents I C Agents in the System Everybody Knows 21 The modal operator Erg is exactly true when all members of the group T know g formally TS gF Er if Vi T TS g F Kip This modality shows that every agent or if T is a strict subset of all the agents every agent in the set T knows y It is sometimes referred to as mutual know
22. N Z ae R 58 g 60 F NE ZN J gt x YNI N L oo Ne NS 4 40 soa WN sea Ne B amp CNS NS Bee YN 4 NS al ve INS NS J 20 Ne UN Sod Ne N Ne We ate iss WINS VSS CNS 25 50 75 WORKING Breaking Threshold of Train The next four figures Figure 5 12 to Figure 5 15 show that bounded model checking is an appropriate verification technique across different size models when using more complex parameterised formulae which also deal with knowledge All four show the attempted falsification of the Yr c3 property the number of agents in the model in Figures 5 12 and 5 13 is 2 whilst being 3 for Figures 5 14 and 5 15 We pass the number of agents in the model as the parameter of the formulae The graphs plotting data from models containing type 2 trains Figure 5 12 and Figure 5 14 both show two interesting anomalies In the first with 2 trains although the initial results depict the expected trend as the depth increases the resource requirements increase towards the deeper breaking depths at which the property can be falsified the resource requirements go down This is still a favourable result in terms of BMC it implies that as the fixed point of reachable states is approached the last few add more states than in the initial iterations In the second with 3 trains it appears that checking a shallower bound requires more resources than a deeper one but this is not the case In the first two the breakin
23. T R L where S isa finite set of states or worlds Tis the set of initial states Z C S Risa transition relation between worlds R C S x S It is a total relation such that Vs S ds S s S ER Lisa function that labels states from S with atomic propositions Temporal logics are used to specify properties about the behaviours of a system defined by Kripke structures A behaviour of such a system can be obtained by repeatedly applying the transition relation R to the set of currently reachable states starting with an initial state s Z Informally a trace or run of a system modelled by a Kripke structure is a sequence of states such that the first state is in the initial states and each successive state is reachable as per the transition relation Given that R is total all of the traces of these systems are infinite This infinite behaviour of systems modelled with Kripke Structures led to Lamport s 34 classification of the requirements of these systems to fall into two categories Safety something bad is unable to occur A system will satisfy the stated property if all of the be haviours of the system do not satisfy this property Liveness something good will eventually happen In this case the system must exhibit a specific behaviour to satisfy the property e g return to the initial state There are two main classifications of types of temporal logics
24. URL http www sciencedirect com science article B75H1 4G6932F 5V 2 5e7d156deb72017230487 10e4e7d1 0 Franco Raimondi and Alessio Lomuscio Verification of Multiagent Systems via Ordered Binary Deci sion Diagrams An Algorithm and Its Implementation In AAMAS 04 Proceedings of the Third Interna tional Joint Conference on Autonomous Agents and Multiagent Systems 2004 pp 630 637 Franco Raimondi and Alessio Lomuscio Towards symbolic model checking for multi agent systems via obdds In Formal Approaches to Agent Based Systems volume 3228 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 24422 6 ISSN 0302 9743 Print 1611 3349 Online 2005 pp 213 221 URL http www springerlink com content h5tnkadaw0bgx0my Franco Raimondi Alessio Lomuscio and Hongyang Qu MCMAS vo 9 6 User Man ual URL http dfn dl sourceforge net sourceforge ist contract mcmas 0 9 6 2 tar gz Richard Rudell Dynamic variable ordering for ordered binary decision diagrams In ICCAD 93 Proceed ings of the 1993 IEEE ACM international conference on Computer aided design IEEE Computer Society Press Los Alamitos CA USA ISBN 0 8186 4490 7 1993 pp 42 47 Marek Sergot Notes from the course 499 Modal and temporal logic Autumn 2008 URL http www doc ic ac uk mjs teaching 499 html M Sirjani A Movaghar A Shali and F S de Boer Model Checking Automated Abstraction and Compositional Verification of Re
25. X n X Ag gt Lpg The set of initial states Z evolution functions t and the protocols Pj define the run of an interpreted system Definition 9 52 A run of an interpreted system 7 go 91 is such that go J and for each pair gj gj 1 E T there exists a set of actions a enabled by the protocol P such that t g a 9j 41 Let A be a set of agents 1 n with respective local states protocols and transition relations The set AP is the countable set of propositional variables p q and V is the valuation function for those variables V AP gt 29 Definition 10 52 An interpreted system is a tuple TS S G 20 1 n V where G is the set of reachable global states T is the set of initial states Z C G Il is the set of all the possible runs of the system The binary relation i A is defined by g i J iff li g lig The relation g g represents that the local state of the agent in the current global state is invariant between the two global states That is l g l g where the function l is the projection function for an agent s local state from the global state If two states are invariant for an agent this means that those states are indistinguishable for that agent and as such the agent is unable to distinguish which global state it is currently in An interpreted systems model 52 From the definition of an interpreted system ZS we can create a model
26. acces sible states at each iteration of state space generation We can see that when using bounded model checking the error trace called a counterexample can be located after reaching the second state In this instance the whole procedure can return false and only has to explore two states rather than checking four states as a conventional model checker would 1 2 Motivation Conventional model checking and bounded model checking are currently complementary to each other Most conventional symbolic model checkers have implementations that are based on a representation called Binary Decision Diagrams BDDs Section 2 3 3 In the simplest of terms these are binary decision trees where isomorphic sub trees are removed to reduce redundancy In comparison bounded model checking is an approach to overcome the state space explosion problem by a translation of the property and the model to the Boolean satisfiability problem SAT Section 2 3 5 Modern SAT solvers take a Boolean formula and attempt to find an assignment to each variable contained in it such that the whole formula evaluates to true Most model checkers are based on BDDs requiring a complete exploration of the state space Section 2 3 1 There is not an obvious conversion from a model checker based on BDDs to being able to perform bounded model checking with SAT 1 3 Contributions The main contribution of this report is a method for bounded model checking
27. based on BDDs Section 4 1 This method unlike other methods for BDD based BMC is complete and exact it does not return either false positives or negatives An evaluation of this method includes an evaluation of using existing fixed point methods for calculating the satisfiability sets when using non total transition relations The specifics and im plementation details of this method and the evaluation can be found in Chapter 4 and Chapter 5 respectively This work contains two different approaches to performing bounded model checking 1 Full BMC Section 4 1 This performs iterative depth bounded model checking inside the model checker in an attempt to find the shortest counterexample to a given specification 2 One shot BMC Section 4 1 2 Rather than performing the satisfiability checks at each incremental depth we describe a method for performing a single satisfiability check at a given depth This depth may be less than the depth required to find the fixed point The uniqueness of our approach is that while there do exist tools which perform bounded model checking on BDDs Section 2 3 9 these are very primitive approaches They can only verify liveness properties which are expressible in terms of atomic propositions These methods detect a violation of the specification by finding a reachable state in which the proposition does not hold In comparison our method allows for a fuller grammar of expressions that can not
28. be seen that our approach is more flexible and expressive given that it is possible to express more properties than a single error state can describe A striking difference between our algorithm and Copty s is that our algorithm keeps a BDD based representation of the entire reachable state space the variable Reach in the above whilst Copty s implementation only keeps the current frontier set of states The Algorithm 13 presented has two exit points lines 5 and 12 The first of which is the case that the algorithm has found a counterexample to Y this is what we refer to as early termination This is due to the fact that as soon as we find the counterexample to the ACTLK formula we are able to return early i e terminate the algorithm and no longer have to continue building a reachable state space The second exit point line 12 is only accessible if we break the main loop body line 9 The terminating condition for the loop is that we have reached a fixed point in the state space i e the set of next states generated is the same as the previous set of next states we are adding nothing new to the Reach set To calculate the next Reach set line 7 we initially generate only the set of next states These are the states that are reachable one step away from the current reachable states set i e with one application of the transition relation We can construct these states from the conjunction of transition relat
29. change the size of the BDD leading to totally different BDDs Definition 14 24 Let z1 n be an ordered list of variables without duplications and let B be a BDD all of whose variables occur somewhere in the list We say that B has the ordering 1 n if all variable labels of B occur in that list and for every occurrence of x followed by x along any path in B we have i lt j An ordered BDD is one that has some ordering for the set of variables it represents For a fixed variable ordering the BDD representing any propositional formula is uniquely defined This means that equivalent formulae are all represented by the same BDD Literature exists to suggest that it is generally a good heuristic to group dependent variables closely together in the graph see 44 for details Tests of BDDs 24 Forafunction f 21 2 andaROBBD Br representing that function the function 1S Valid iff By is the single terminal node B representing true Satisfiable iff By is not the single terminal node Bo representing falsity BDD based algorithms There exist a various number of algorithms that are based around BDDs these are not discussed here the reader is referred to 24 14 Kripke Structures as BDDs The state of a system can be symbolically represented as the assignment of values to the variables of each state The transition relation can equally be represented in the same way as a Boolean func
30. doi http dx doi org 10 1109 ICWS 2008 115 Alessio Lomuscio and Franco Raimondi MCMAS A Model Checker for Multi agent Systems In Tools and Algorithms for the Construction and Analysis of Systems volume 3920 2006 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 33056 1 ISSN 0302 9743 Print 1611 3349 Online 2006 pp 450 454 doi 10 1007 11691372_31 URL http www springerlink com content hr800h4080771487 Alessio Lomuscio and Marek Sergot The bit transmission problem revisited In AAMAS 02 Proceed ings of the first international joint conference on Autonomous agents and multiagent systems ACM New York NY USA ISBN 1 58113 480 0 2002 pp 946 947 doi http doi acm org 10 1145 544862 544961 Alessio Lomuscio and Marek Sergot A formalisation of violation error recovery and enforce ment in the bit transmission problem In Journal of Applied Logic volume 2 2004 1 pp 93 116 ISSN 1570 8683 doi DOI 10 1016 j jal 2004 01 005 The Sixth International Workshop on De ontic Logic in Computer Science URL http www sciencedirect com science article B758H 4C2R2K0 1 2 a86cd71 9a06e11819c2deddf 21e6f5a Alessio R Lomuscio Notes from the course 303 Software Engineering Systems Verification Spring 2008 URL http www doc ic ac uk alessio teaching 08 sv sv html Stephan Merz Model Checking A Tutorial Overview In Modeling and Verification of Parallel Processes editor F Casse
31. end while return Y o S OS ates 22 It can be seen that Algorithm 5 and Algorithm 4 can both be calculated from the least lfp or greatest gfp fixed point of EX 16 EG y gfp Z p AEX Z E pUy If Z y vV pA EXZ We can also define the temporal operator EF in a similar way EF y lfpZ py VEX Z 2 3 2 Counterexamples and Witnesses A benefit of model checking is the ability of the model checker to generate counterexamples and witnesses to properties In a CTL model when a universally quantified formula is found to be false the algorithm will generate a counterexample that is a computation path which demonstrates that the negation of the formula is true 16 Likewise when an existentially qualified formula is found to be true the algorithm will generate a witness that is a computational path which demonstrates why the formula is true 16 2 3 3 Symbolic Model Checking Binary Decision Diagrams Binary Decision Diagrams BDDs 8 3 24 60 or more commonly reduced ordered binary decision diagrams are one of the most widely used symbolic data structures for use in model checking ROBDDs 13 Are canonical and unique to each Boolean function Allow for operations such as negation conjunction and implication to be easily implemented with a complexity that is directly proportional to that of the inputs A BDD is a directed acyclic graph with exactly two terminal nodes drains one marked 1
32. formula quantified with A is true in a state with no successors 86 that transferring such a small file over a gigabit connection would be virtually instantaneous 5 7 Qualitative Evaluation 5 7 1 Effectiveness of Deliverables The solution we have presented here performs as expected when possible it can falsify properties early and when not possible it pays minimal overhead for exploring the whole of the model Although this is a desirable goal the means to an end turning off garbage collection and asynchronous reordering may not be justifiable in other circumstances 5 7 2 Elegance of Solution MCMAS s code whilst not being the cleanest of code bases was amenable to the implementation of all three of the techniques that were implemented Our solution could have been a more modular and cleaner solution if MCMAS utilised the object oriented paradigm more For instance only having a single class representing a formula with a field specifying its type is not an ideal solution Using virtual methods and dynamic dispatch would have allowed for various aspects of the code to be cleaner To be able to support the work presented MCMAS s code has been broken up Originally the code was simply one huge main method containing switch statements to decide which method of verification to attempt with all the code inlined Our solution is now more modular and although it could be extended further has already improved the
33. have any reachable states The flip side to this is if all results from the seeds return this value fig 4 3 3 From this we can see that from all of the seed states the property cannot be falsified This in conjunction with the initial check by the master instance performed up to the generation depth ensures that the invariant is satisfied on the whole model From this we are able to deduce that from all reachable states from the initial state a violation of the invariant cannot be found As such the verifier can return a definite answer of true to the user Figure 4 7 Seeded BMC in which all of the slaves return maybe true Depth k 4 3 4 Distributing MCMAS We have developed a framework that can be used as an extension to MCMAS allowing for easy distribution Our framework is not directly tied to the model checker it acts as a wrapper to the model checker allowing for communication between the master and slave instances Our approach can be utilised across different model checkers providing that they return output in a specific format We use a networked file system that is common to all of the nodes of the system This allows for easy transfer of data the model and the initial states between different hosts MCMAS was extended to take some parameters the first of which is a flag specifying if it should be launched as either a master or a slave If we are launching a master instance we provide it with a directory that
34. looked at LTL invariant properties and these methods unlike the method here are not complete Deliverables The main output of this project has been an extension to the existing model checker for multi agent systems MCMAS An implementation of all three types of bounded model checking has been provided and discussed An auxiliary script to allow for automated one shot BMC until a counterexam ple has been located A novel Java infrastructure allowing for the distribution of any model checker sup porting seed states has been developed and used to show the effectiveness of verifying the logic ASCTLK over a grid Examples The introduction of a new scalable model has been discussed and how it can be used to benchmark bounded model checking with a configurable number of steps until the given formulae can be falsified has been shown 6 1 2 Comparisons In Chapter 5 the implementation devised was evaluated and figures detailing performances were produced It was shown that with variable reordering turned off our BMC implementation out performs traditional model checking when a counterexample can be found and when it cannot the overhead required for performing the iterative checks has been shown to be minimal Performance benefits including results that demonstrated reduction in the order of magnitude were presented It is unfair to simply state a single value and claim that our BDD based BMC implementation performed
35. lt k Si Si 1 ER Definition 16 loop 48 a k path 7 is a loop if 3l 0 lt lt k and x k m l Definition 17 k model 48 Let M S Z R L be a model and k Nt Mg S TZ Pathsk L where Paths is the set of all the paths of length k in M 17 Let M bea Kripke structure and Mg be its respective k model the function loop Path 2N is defined as follows loop 7 1 1 lt k and x k n l E R For the rest of this chapter we will be dealing with two restrictions of CTL One is called ECTL this is a subset of CTL in which negation can only be applied to propositional atoms AP The other is called ACTL p E ACTL iff y E 7 Y ECTL Definition 18 Bounded Semantics of ECTL 48 For a k model My p Y are ECTL formulae Mg s E y denotes vy holds in the state s of a model Mg E is defined as follows Mk sEp iff peEL s Mk sF y iff gk y Mk sFovy if Mpk s E p Mp sEvpAw iff Mk s EF or My s E 4 and Mg 5 E Y Mz SF EX iff Am Paths 1 0 g and 7 1 E My 8F EGp iff dm Paths 7 0 g and Vo lt j lt xMx T J E p and loop 7 0 Mk sHE pU if Jr Paths m 0 g and Jo lt i lt ck Mpg m i E Y and Vo lt jciMk 7 J E p M the size ofa ECTL model is defined by the number of states in S p the length of a ECTL formula is defined as follows ify APU gt p p E AP then y
36. maintainability of code and the provision of further verification techniques into MCMAS The distributed aspects of the model checker in an attempt to avoid re inventing the wheel and to keep MCMAS s code slightly cleaner were implemented as an external Java application Although this can be seen as a not particularly favourable solution due to the lack of tight knit integration and the need for the application to understand MCMAS s output it does have one benefit It can now easily be extended to support other model checkers that support partial state space verification using seed states 5 73 Scalability As shown in Section 5 4 5 when CUDD s optimisations are turned off MCMAS is not able to verify large models The methods presented for distributed bounded model checking could be used to alleviate this problem Rather than using depth as a heuristic for seed state generation we could generate seed states when the memory used or the size of the current reach set exceeds a given threshold Summary In this chapter we have not only shown that the foundations of the approaches we have taken are sound we have also evaluated our implementations of these approaches The performance of our BDD based implementation of bounded model checking has been shown to be favourable when used on models that have formulae that can be falsified prior to reaching the entire state space We have also shown results that allow us to conclude that bounded
37. model checking Given a description of a finite system with a transition relation TR and a set of initial states S their method attempts to check an invariant property P by checking the reachability of the target set T representing the compliment of P from S For each pass of their algorithm a check is made to ascertain if the frontier set the current reach set and the error set are disjoint Given a bound k their algorithm is as follows Algorithm 11 Bounpep TRAvERSAL TR S T k x Frontierg S 2 for i 0 i lt k i do 3 if Frontier T 4 0 then 4 return FAILURE 5 endif 6 Frontier Imc TR Frontier 7 end for 8 return PAss The function Imc is used to calculate the next set of reachable states from a given state using the transition relation Among other topics Amal et al 2003 2 discuss the terminating conditions for BDD based BMC at a depth k gt see 17 for details 27 All paths of length k have been explored A state in the target or error set has been reached All reachable states have been explored a fixed point has been reached The final conclusions reached by Copty by comparing Forecast against a SAT based checker Thunder seem to suggest that a SAT based BMC out performs BDD based BMC but their comparisons are possibly flawed due to the fundamental differences between the two checkers The ideas discussed by Fady Copty et al are further extended by Cabodi et al in 2002 9
38. noted that this overhead is only demonstrated in a model in which the property cannot be falsified meaning that BMC has to perform significantly more calculations in comparison We feel obliged to point out that given how we perform bounded verification and the fact that calculating the satisfiability set of the given formulae is not free this is exactly the result we would expect Figure 5 16 Memory usage for two type 2 trains with a full service depth of 20 when checking various for mulae Bounded Model Checking Memory Usage T T T T T Yrecl 140 H Prec ZZZ 4 Preca SNS 120 gt ES ee ia E 100 4 NOE D 3 IN eee ore Ge J IN ZS 60 H N AN a 5 ZNS YN 2 GN Ne j vaca NS NS ee I ON A 1 UN GNE Ne 20 ZIN Z WN NS 5 RIA A Iw 0 WN Z N NE 4 8 12 16 WORKING Breaking Threshold of Train 74 Figure 5 17 Memory usage for three type 2 trains with a full service depth of 7 when checking various formulae Bounded Model Checking Memory Usage I Pracl 140 gt Prec ZZZ PrecdA SSS Proch ee 120 gt 100 100 80 H 60 of Memory Used 40 H 20 F WWW WI HAIN LMM iy SG wA o SK WORKING 3 Breaking Threshold of Train Figure 5 18 Time required for two type 2 tra
39. only deal with quan tifications of paths through the model but can also verify epistemic properties ones that express a notion of knowledge The final method contributed by this work is an approach of distributed bounded model checking based upon exploration of partial state spaces on different networked hosts Section 4 3 4 Our method generates a set of candidate seed states each of which can be used as the initial state on different hosts To support this distribution we further restrict the universal fragment of CTLK to allow only invariant properties Section 4 3 1 This restriction means that the method of distributed partial state space exploration is both sound and complete Section 5 3 To allow for the effective evaluation of such a method we have presented a novel scalable scenario The Faulty Train Gate Controller Section 4 4 which can allow for an adjustable depth for a counterexample to be found Increasing this bound towards the depth at which the fixed point in the state space is reached allows us to critically evaluate if the method pays an undue overhead The model presented has a number of meaningful parameterised specifications Section 4 4 3 this allows for the generation of formulae proportional to the number of components in the system Chapter 2 Background 2 1 Temporal Logics It is possible to describe a finite state system e g a reactive one as a Kripke structure 33 M S
40. s default regular model checking method a value greater less than 1 indicates a decrease increase Table 5 1 Memory time and states results with a vanilla CUDD verifying the Yrec5 Model Decrease PT MB Memory Time Seve It can be seen that in the examples above BMC did not produce any reduction in the resources used with the exception of a model with 3 trains in which the regular final verification performed took longer than the intermediate checks as performed by BMC but the memory used was still higher It became increasingly apparent that MCMAS required an unusual amount of memory to represent initial states and this value did not fluctuate significantly from start to finish i e there was little variance between the memory required when verification began and the memory held by MCMAS when verification terminated For instance in a model with two Type 2 trains a full counter of 10 and a breaking threshold of 4 MCMAS required 4911108 bytes to represent the single initial state and yet only required 6210388 to hold the entire fixed point of states an additional 10605 states MCMaAS yas initially using the default CUDD constructor Figure 5 10 which gave an initial pre allocated cache size 256 KiB This was changed such that rather than being initialised with CUDD_CACHE_SLOTS CUDD s constructor was passed 0 such that it initialised with no cache This meant that when verification began after
41. specification in k steps From a temporal logic specification and a Kripke structure a propositional formula is generated that is sat isfiable if there exists a computational path with length k within the model that satisfies the specification The generated Boolean formula is given to a solver which calculates an assignment to all of the variables comprising of the formula such that a final evaluation is true The variable assignment is a witness to that path SAT also known as the Boolean satisfiability problem is the problem of trying to find an assignment to all of the variables within a given formula such that the whole formula evaluates to true A crucial part of the bounded model checking algorithm is that although the path considered is finite it may still represent an infinite path within the model if it is said to contain a back loop from one state in the path to an earlier state in the path If the path does not contain a loop then nothing can be inferred about the infinite behaviour of that path An example of this is that p might hold at every state path of length k and therefore be seen to be satisfying Gp but without a back loop it cannot witness that formula because at state 5x41 of a path length k 1 p may no longer hold For a path 7 in a model 7 k represents the state at element k in the path Definition 15 k path 48 Let k Nt and M S Z R L A k path is a finite sequence 7 S0 Sk VWi 0 lt i
42. specifics that occur in the current version of MCMAS 3 3 1 Global Variables The following is a list of global variables that are used throughout MCMAS s code BDD reach the reachable states a BDD representing the current reachable set of states BDDvector v the local states a vector of BDDs each describing an exact local state for each agent see previous part BDDvector pv the next states a vector of BDDs each describing a unique local state for an agent BDDvector vRT the transition relation a per agent mapping between v and pv constructed from the conjunction of the protocol and the evolution function both represented as BDDs map lt string basic_agent gt is_agents the interpreted systems agents an std map of strings of agents names to instances of agents modal_formula_vector is_formulae the interpreted systems formulae an std vector of all the formulae as given in the ISPL for that model 3 3 2 Important Classes Object This is a base class that the majority of classes extend it is very similar to the Object class in Java Importantly the class includes a virtual to_string method modal_formula public Object This is the class that MCMAS uses to represent and store modal formulae When the ISPL code is parsed it generates modal_formula and stores them in the is_formulae vector 1Version 0 9 7 A Boolean vector is an array of BDDs
43. state transitions after a certain depth They look at proving a property holds rather than trying to find a counterexample SAT based BMC As previously discussed They also make the distinction that unlike Copty s implementation both their BDD and explicit state BMC methods can produce a positive answer if all the reachable states have been encountered at the depth checked 2 4 Distributed Model Checking There exist various techniques for attempting to alleviate the infamous state space explosion problem BMC is only one such method which allow for the automated verification of larger systems One such approach is 28 an attempt to distribute and parallelise the computational work load associated with model checking These are approaches that aim to exploit the resources available in a parallel computing environment such as a cluster or a grid computing environment in an attempt to solve larger more realistic industrial sized verification problems 77 When the model checking procedure suffers from the state space explosion and as such no longer fits completely into the computer s main memory this causes swapping Being unable to store the complete state space and having to utilise backing storage causes a significant inefficiency in the procedures used Many attempts to parallelise model checking involve an attempt to divide up the state space into indepen dent sub tasks that can be performed in an arb
44. the logic universal fragment of ACTLK We said that in ASCTLK all formulae are invariant that is the top most connective in the parse tree must be an AG Proposition 2 Seeded bounded model checking is sound with respect to the total model when a counterexam ple for AG is found from an individual seed state Proof Through the construction of the seed states every seed state is reachable from the initial state in the model Finding a counterexample from this seed state means that there exists a path from that state to another in which does not hold i e EF holds in the seed state As such there exists a path in the full model that starts at the initial state and passes through this error state From the semantics of CTLK we also have EF y in the initial state O Proposition 3 Seeded bounded model checking is complete with respect to the total model when a counterex ample for AG cannot be found from any seed state Proof Ifthe truncated model up to the depth at which the seed states were generated could not satisfy EF and neither could any of the partial state spaces starting from each individual seed this means that there does not exist a reachable state in which y does not hold As such from the semantics of CTLK we do not have a path in any part of the model that satisfies EF so AG y is satisfied by the model O 66 5 4 Performance and Benchmarking 5 4 1 An Initial Investigation The machine
45. true and the other 0 false Each of the internal nodes represents a single Boolean variable and has only two outgoing edges one solid representing an assignment of true to that variable and one dashed an assignment of false The node reached from the true path is the value returned by the function succ u v where u v V V is the set of nodes in the graph Similarly for false succo Boolean operationson BDDs Given two BDDs b B representing the functions f g respectively the BDD for f A g can be obtained by taking the BDD By and replacing all of its 1 terminals with By This is similar for f V g except the 0 terminal is replaced 44 24 Semantics of BDDs_ The semantics of a BDD B fis the value the terminal node reached when traversing the graph starting from the root node and taking the corresponding path representing the variable at that node Reduction rules A reduced BDD B is one that has undergone the following transformations repeatedly until a fixed point has been reached 43 3 Elimination For two inner nodes u v for which succ u succo u v all of the incoming edges to u are directed to v and u is eliminated from Bb Isomorphism If two distinct inner nodes u v of B are the roots of two structurally identical sub trees node u is removed and all of its incoming edges are redirected to v Variable ordering The ordering in which variables appear in a BDD drastically
46. where each BDD represents one bit of an expression 67 36 Variables unsigned char op MCMAS does not support any kind of inheritance to distinguish between differ ent types of modal formulae Each type of modal formula has an associated unsigned char value e g an atomic proposition is represented by 0 AG is represented by 10 and K is represented by 30 Object obj MCMAS uses this variable to store the arguments to the formula for example another modal_formula Methods BDD check_formula Checks the modal formula with respect to the current reach set The return value is the BDD representing the set of states in which the formula holds modal_formula push_negations int level Pushes negations down a certain number of levels through the entire formula e g using De Morgan s Laws or re writing formula with a leading negation to use the dual Returns a pointer to a new formula with pushed negations bool is_ACTLK Checks if the given formula is in ACTLK bool is_ECTLK As above except for ECTLK basic_agent Used to represent an agent within MCMAS Each agent has a respective name its name vars the variables that comprise an agent s local state actions the actions that agent can perform protocol which actions can be performed in a given state evolution how an action affects an agent s local state 3 3 3 Satisfiability Checking Within MCMAS As st
47. with Y i do 3 compute Sat w from Sat 4 end for 5 end for 6 return Z C 4 Definition 13 Sub formulae of a CTL formula 32 Let p AP and y Y be CTL formulae then Sus p p Sus gt y Sus y U gt Sun y Vay Sus y U Sus y U p VY Sus EXy Sus y U EXy Sus EGy Sus y U EGy Sus E pUy Sus y U Sus y U E pUy Algorithm 2 Sat p Formuta set of STATE x if p TRUE then 2 return S else if p rarse then return else if p AP then return s py L s else if p 7y then return S Sat y else if p EXy then ro return SATEx 1 tr else if p E y Uya then 12 return Satgu 1 p2 13 else if p EG 1 then 14 return SAaTgG 1 15 endif State pre image functions pre Y s S ds sRs ands Y pre Y s S Ys sRs implies s Y If Y is a set of states pre Y generates the set of states that can transition into Y and pre Y generates the set of states that only transition into Y I2 Algorithm 3 SaTgx y Formuta set of STATE x X Sat y 2 Y prea X 3 return Y Algorithm 4 SaTgu g Formuna Y ForMULA set of STATE 1 W lt Sat y X lt S Y Sat w while X Y do xX Y Y YU WN pre3 Y end while return Y Y oyaw e R Algorithm 5 Satgg y Formuta set of STATE r X lt Sat y 2 Ys Z while Z Y do Z Y Y XN pre Z
48. 0 this is mirrored in these results TThe time taken to perform the single satisfaction check in regular model checking was unusually long which is why one shot appears beneficial in these results 82 Table 5 7 Improvements for One Shot BMC and full Table 5 8 Improvements for One Shot BMC and full verification with reordering 2 Trains Max Counter 20 verification with reordering 3 Trains Max Counter 7 Decrease Memory Time IO Decrease Memory Time 15 WORKING WORKING 5 6 Evaluation of Distributed MCMAS There were two different factors which required consideration when benchmarking 1 Depth of seed state generation The threshold depth at which the seed states generated would affect the number of seed states that had to be verified 2 The number of slaves If the master instance had more slaves available for it to use this should cause a decrease in the time that verification took Evaluation Difficulties Our method of distributed model checking lends itself well to models that have deep counterexamples and that suffer from the state space explosion problem both of which it attempts to alleviate through state space partitioning To be able to show proficient benchmarks we require models with these problems The models that come with MCMAS are either too small or have shallow counterexamples although the faulty train gate controller model can be constructed such that it displays a
49. 4 Descriptions of actions for a type 1 faulty train Label Action Assignments Preconditions ty SERVICE servicecount 0 to BACK servicecount servicecount lt maxcounter t3 SERVICE servicecount 0 t4 SIGNAL servicecount servicecount lt maxcounter ts ENTER servicecount servicecount lt maxcounter Controller action ENTER_TRAIN this T t7 BREAK broken true broken false servicecount gt threshold tg LEAVE servicecount broken false servicecount lt maxcounter 4 4 3 Specifications To display the effectiveness or possible ineffectiveness of our BMC implementation we need to be able to specify properties upon the model that can be falsified in a model with faulty trains i e trains of the type 1 or 2 These are properties that if evaluated on a model with correct trains i e type 3 should not be falsifiable i e they should be satisfiable in the model 56 Figure 4 15 Descriptions of actions for a type 2 faulty train Label Action Assignments Preconditions ee t7 BREAK servicecount gt threshold tg LEAVE servicecount Figure 4 16 Descriptions of actions for a working train Label Action Assignments Preconditons ty SERVICE servicecount 0 to BACK servicecount servicecount lt maxcounter t3 SERVICE servicecount 0 t4 SIGNAL servicecount servicecount lt maxcounter ts ENTER servicecount servicecount lt maxcounter Controller action ENTER_TRAIN this A S
50. A 1 and New Globals Figure A 2 For efficiency rather than calculating an ECTLK formula from a ACTLK each time we keep a pair of both types of formulae which allows us to easily change between the two Conversion of ACTLK to ECTLK Figure A 3 We convert from an ACTLK formula to an ECTLK one by construction of the negation of the ACTLK formula and then pushing the negations through We extended the push_negations function to support re writing a negated K modality to that of a K modality Checking the ECTLK formulae Figure A 4 The original MCMAS implementation iterated over the is_formulae vector In an attempt to reduce the effect our code had on the original implementation we added a function that iterated over the bmc_formulae vector Implementing Algorithm 13 Part 1 Figure A 5 In this Figure we outline our implementation of Lines 1 11 from the original algorithm The main difference between the algorithm and the implemen tation is that rather than a while true our loop is guarded on still having formulae to check Implementing Algorithm 13 Part 2 Figure A 5 Our implementation terminates with Line 12 from the algorithm We print out all of the formulae for which we have found counterexamples any remaining formulae are checked with the original check_formulae function 44 4 2 SAT The heart of bounded model checking lies in being able to satisfy an existential formula without the requi
51. Lomuscio et al in 39 38 presents a model based upon the composition of services based upon acontract Their model contains seven agents a principal software provider PSP a software provider SP a software client C an insurance company I a testing agency T a hardware supplier H and a technical expert E Their idea is as follows The client C wants a piece of software developed and deployed on a hardware supplier H by the technical expert E There are two parties that are to provide the software the principle PSP and non principle SP software providers The PSP performs software integration of its software with SP s when a deliverable is made which it then sends to the testing agency T for testing If the software passes testing it is given to the insurance company I for the provision of software insurance The software is finally handed over to the E who deploys it on the H If any of the above parties deviate from the above e g C requires software changes that either PSP or SP do not agree with or the software fails in testing too many times the contract is violated ACTLK Properties Yspi ACHardwareSupplier_green U HardwareSupplier_end False The hardware supplier is always in compliance until it has finished the contract The Book Store This model is similar to the software development model found above in as much as it deals with contract violations The model contains two a
52. MENG INpI1vipuaL Project REPORT A Method of Bounded Model Checking for a Temporal Epistemic Logic Based on Reduced Ordered Binary Decision Diagrams Andrew JoNES avjos doc ic ac uk Department of Computing Imperial College London Supervisor Dr Alessio R Lomuscto alessio doc ic ac uk Second Marker Prof Marek Sercot mjs doc ic ac uk Project ARCHIVE http www doc ic ac uk avjos memas tgz June 16 2009 Abstract Symbolic model checking is a powerful technique for the verification of reactive systems Traditionally such approaches use reduced ordered binary decision diagrams ROBDDs to represent the model These however suffer adversely from the infamous state space explosion problem Bounded model checking a procedure for bug hunting attempts to alleviate this difficulty by considering only a truncated model up to a specific depth The possible falsification of a universally quantified formula is shown through a translation of the specification and the model to the Boolean satisfiability problem SAT We propose a method of bounded model checking for the existential fragment of the epistemic logic CTLK grounded in the interpreted systems formulation of multi agent systems Our approach uses ROBDDs to rep resent reachable state space rather than a translation of the problem to SAT We show that this is not only flexible but can also be easily extended to support agent verification in a distributed env
53. Models 2 5 1 The Train Gate Controller Model Discussion on Prior Art CUDD Specifics cate aoa 4 MCMaAS Internals 3 3 1 3 3 2 3 343 Models Global Variables Important Classes Satisfiability Checking Within MCMAS oe eS tt ee te ee Ww H H O o ooon H 13 I3 I5 17 20 22 23 27 28 29 30 30 35 35 35 36 36 36 37 38 4 Original Contributions 4 1 4 4 BDD Based BMC 00 04 ee ee ee ees 4 1 1 BDD Based BMC with Early Termination 41 2 VariationsonBDD BMC 4 1 3 An Implementation 4424444264445 4 DATE cee od eelwaw edea e een eed ea ia 4 21 BDD BasedSatg eee eee Distributed Verification of ACTLK 4 3 1 The Key Idea of Grid Based BDD BMC 4 3 2 Outline of Grid Based BDD BMC 4 3 3 Uniqueness of the Approach 4 4 3 4 Distributing MCMAS 2644226645 4 3 5 Consideration of Other Connectives A Scalable Model 2 2 2 ee ee ee ee 44m The Faulty Conteoller 544444 e404 4 4 2 The Faulty Train 400k eo ee ee ee ee 443 Specifications 4 4 04 444444844 2 2 5 Evaluation 5 1 5 3 5 4 5 6 5 7 Fixed Point Methods on Non Total Transition Relations BA SAILE ceaiorie aek ee wk e E AT SATBG 244 4e ak bdo aS Dee ERS BTS JOATBR satapa 4 irrt a ir A we ee a Bhg SATB Aad ad ee ea oe See de ee
54. Other idle end Protocol Evolution counter counter 1 if counter lt 2 and lights red lights green and counter if counter 2 and lights red lights red and trainl_waiting false if trainl_waiting true and lights green and Action enterl and Trainl Action enter lights red and train2_waiting false if train2_waiting true and lights green and Action enter2 and Train2 Action trainl_waiting true if Action idle and Trainl Action train2_waiting true if Action idle and Train2 Action end Evolution end Agent 59 Figure 4 18 An example type 1 faulty train Agent Trainl Vars state wait tunnel away serviced 0 20 broken boolean end Vars Actions signal enter leave back service break Protocol serviced 20 and state away or state wait service state wait and serviced lt 20 signal service enter Trains work correctly if the non deterministic break action is removed Replace the following lines state tunnel and serviced lt 5 and broken false leave state tunnel and serviced gt 5 and serviced lt 20 and broken false leave break state tunnel and broken true break state tunnel and serviced 20 and broken false break With state tunnel leave state away and serviced lt 20 service back end Protocol Evolution serviced if Action service s
55. S tg LEAVE servicecount It should be clear to the reader that a faulty controller when used in a model with faulty trains may allow extra trains to enter the tunnel even though there is still another train currently occupying it e g A train of type I enters and subsequently breaks in the tunnel Two synchronous evolutions occur the controller then moves into the green state and allows another train to also enter We feel compelled to point out to the reader at this point that neither our faulty controller model nor the bounded model checking that has yet to be presented support any kind of notation This means that the starvation property from 57 cannot be used as it would be false both in a model with faulty and a model with correct trains The following formulae are described in a model containing two trains TRAIN and Traino The proposi tional atoms TRAIN _IN_TUNNEL and TRAIN2_IN_TUNNEL hold iff the local state for each agent is Tunnel The formulae p2 to Y5 can be constructed pairwise with each unique pair of agents within the system Formula 1 Yrec1 There always exists a future state in which the train no longer occupies the tunnel ACTLK AG AF TRAIN1_IN_TUNNEL ECTLK EF EG TRAIN1_IN_TUNNEL ISPL AG AF trainl_in_tunnel Formula 2 Yrec2 Mutual Exclusion Two trains never occupy the tunnel at the same time ACTLK AG TRAIN1_IN_TUNNEL V TRAIN _IN_TUNNEL ECTLK ISPL AG
56. T Another problem with a majority of the existing approaches to BMC is that with the exception of the unstated algorithm in 2 they only deal with the falsification of properties This is not a favourable solution given that BDD based methods of satisfaction also enable the user to prove if a property is satisfiable When performing forward verification as in Copty s approach we can be more intelligent The majority of most symbolic model checkers perform forward verification building up a reachable state space until a fixed point is reached An approach such as Copty s which takes this fixed point into consideration is clearly a preferable solution as opposed to assuming that not finding a bug at a given depth is an indication that no bug exists at any depth Approaches taken by NuSMV for invariant satisfaction or the previously discussed BDD based bounded model checking methods only look at very simple properties that is properties that can be expressed through the assignment of propositional atoms NuSMV s approach is to check if the reachable states are a subset of the states in which the atom holds In contrast the BDD based BMC approaches of 17 9 2 look at trying to falsify safety properties through the intersection of the reachable states and the error states which invalidate the safety property It should be immediately obvious that the full lexicon of expressible properties in a logic such as CTLK cannot be expresse
57. The function l is used to extract an agent s local state from the global state This can also be represented with the relation g i g2 where the relation is defined as for CTLK It is worth noting here that ifZS g F y then Vi E Acents ZS g F Kiy given the relation is reflexive For the semantic definition of Ep and Cr the reader is referred to either 62 or 35 Translation to SAT of a ECLTK formula 62 47 As well as having a Boolean encoding for propositions such as the initial state or the proposition variables BMC has a Boolean encoding for the epistemic relation between an agent s local states that is equality between two local states H w v iff U w 1 v Vi E AGENTS The translation of K y to SAT is as follows K hie VV I wo i ip H Wm n wja iELL j 0 2 38 Current Model Checking Technology CUDD CUDD 58 68 isa C based BDD library that allows for easy code reuse CUDD provides The data structures necessary for BDD creation handling and manipulation Efficient implementations of BDD functions and or add Utility functions for managing the BDDs BDD managers that are basically hash tables for BDD storage Within the CUDD BDD representation the lower bits of pointers are used to represent the negative edges from a BDD It also provides a method of generating Graphviz Dot 72 diagrams for the BDDs it is used to represent Operator Overloading As can
58. ace The Dining Cryptographers Although in the dining cryptographers Figure 5 23 Ype2 is false in this model we are unable to find a coun terexample until we reach the same depth at which the fixed point is found so BMC displays no immediate benefits Whilst Ypc2 is true on the model the fixed point in the state space is reached after two iterations so performing two extra checks does not pay much of an overhead The Software Development Example The only ACTLK property that is provided for the software development example is false in the initial state This is an example in which BMC excels as is clearly illustrated by the graph Figure 5 24 Full verification of this model requires 70 iterations to reach the fixed point nearly 14s versus os and uses nearly 60 times as much memory full verification uses 118 MB whereas the initial states are representable in only 2 MB 77 of Resources of Resources 140 120 100 80 60 40 20 o 140 120 100 80 60 40 20 o Figure 5 21 The Correct Bit Transmission Problem Bounded Model Checking Resource Usage Memory Time States Depth 100 LLL LZ MAW RRR Figure 5 22 The Faulty Bit Transmission Problem Bounded Model Checking Resource Usage Memory ime States Depth 100 A MAA NN LLL Ls Os RRR 7 Parel Formula o0
59. aces the train is broken This trace is more convoluted in the second trace because of the multiple break actions performed by the train BMC was unable to generate a counterexample for Precs CUDD caused the program to terminate with a non zero status and printed out the string Unexpected error It should be noted that the counterexamples that were generated were done so by finding a counterexample to the original ACT LK formulae as specified in the ISPL using the K modality and not the K modality Despite this it was felt that counterexample generation was successful both in terms of readability and length ie BMC did not generate a longer counterexample Forcing MCMAS to continue building up a set of reach states beyond its usual termination depth allowed us to find a counterexample shorter than for full verification for this property But as this was not an automated process the result was omitted push_negations int depth was modified such that when performing counterexample generation it did not translate K to its dual Figure 5 25 Counterexample for Yr c1 from regular model checking M bakbak HD siesignabsignal gt a enterI signal service gt gt A enter1 signal service gt Ey enter1 signal enter gt R enter1 signal signal gt a enter1 signal signal gt J enterI signal service gt gt 8 Figure 5 26 Counterexample for from bounded E enter1 signal enter
60. action Ygs4 AG CCsupplier_compliance and purchaser_compliance gt K Supplier AF contract_end False If both parties comply the supplier knows that eventually the contract will end ie it will not be prematurely terminated In the previous property supplier_compliance holds in the same state in which payment_received holds which when using weak until is true 39 40 Chapter 4 Original Contributions This chapter outlines our contribution of an original algorithm for binary decision diagram based bounded model checking We include discussion of how such algorithm could be implemented within an existing model checker We look at the model checker for multi agent systems MCMAS Section 4 1 lays out an overall view of our approach as well as the devised algorithm We also include a discussion of certain variations on a theme displaying an element of flexibility within the method In the final part of this section we look at implementing this method into MCMAS In Section 4 2 we present a method for SaTgerix Which supports the K operator This is a fundamental requirement to our methods in the preceding section when verifying epistemic logic in a bounded context We also include a BDD based implementation of Sarg for MCMAS Section 4 3 covers an extension to the first method further displaying the flexibility of the approach We show how the method can be distributed requiring only limited changes to both th
61. allow any train waiting to pass through the tunnel Another property that they state which also corresponds to how the controller deals with requests is G CONTROLLER SIGNALI F Trarni INTunNEL This states that once a train receives a signal from a train saying that it is waiting to enter the tunnel eventually that train does enter the tunnel A Multi Agent Train Gate Controller The first time that the Train Gate Controller was considered in a multi agent systems context was in the work by van der Hoek et al 23 A flaw with the paper with respect to this current work is that it was concerned with looking at ATL properties on this model properties expressed in either CTL or CTLK were not given The work presented by Kacprzak et al in 31 29 30 looks at building upon the work of van der Hoek 23 but this time they attempt to present an interpreted systems formalism of the Train Gate Controller problem Their approach endeavours to use the Train Gate Controller example when performing unbounded model checking of multi agent systems Their work makes the assumption that the function of the controller is to ensure that two trains are never in the tunnel at one time and that trains follow the lights diligently i e they stop on red In contrast to the work of Alur and van der Hoek the controller only transitions to the red state once a train enters the tunnel ie the controller is by default in the green state
62. and witnesses should they exist for the provided model and formulae MCMAS also provides an Eclipse 69 interface that supports the creation of skeleton MCMAS files as well as syntax highlighting for them It also provides a graphical interface for executing the checking of ISPL files and then the examination of the counterexamples witnesses generated and their corresponding Dot images The internal structure of MCMAS can be seen in fig 2 3 8 26 Figure 2 8 MCMAS internal structure 50 I Specify an interpreted system Text editor Eclipse interface e a Parse the input lt Flex and Bison Parser j Build OBDDs for the MAS C code and CUDD 4 Parse the formulae to check lt _ C code and CUDD 1 5 i Compute the states in which the formulae hold lt C code and CUDD i 4 i 6 i Compare with the reachable states lt C code and CUDD 7 FALSE TRUE return 2 39 BDD Based BMC In 2001 Fady Copty et al 17 investigated the possibility of using BDDs rather than SAT when performing bounded model checking The main aim of their paper was to see if the benefits gained from performing SAT based bounded model checking was due to the underlying technology used for model checking BDDs vs SAT or whether the gains came from the method of model checking bounded vs unbounded model check ing They adapted Intels BDD based unbounded model checker Forecast to perform bounded
63. ar successor for a particular behaviour In CTL E and A are path quantifiers E repre sents the existence of a path whilst A is a quantifier over all paths they can be seen as synonymous to 3 and V We can now inductively define the meaning of satisfaction F where M s F y means y holds in the state s in the model M and M m E means y holds along a path 7 in a model M Definition 5 Semantics of CTL M sEp iff pe L s M sE y iff M sF oy M sFEypVvw iff M sE y or M sF yw M sEpAw iff M sF y and M sF vy M sFEXy iff 4dr 50 51 M 5s F Y M s E EGy iff M sFE pUy iff T S0 S1 ViM s E Y T 50 51 Jk gt 0 M sk FY and VO gt j gt k M sjE g In the above the semantic differences between E and A can be seen by replacing dz with Yr 2 2 Multi Agent Systems Trends in the fields of interconnected and distributed systems have led to the introduction of the multi agent systems paradigm These are systems comprised of software programs that can act as autonomous rational agents 61 These agents are capable of independent actions as well as communication and co operation with other agents The agent acts in such a way that it can reach its design objectives without being given an explicit procedure of completing these goals The idea of a multi agent system is one of many agents interacting in a global environment In these systems agents are able to hold kn
64. arking results for The Book Store example can be seen in Figure 5 20 It can be immediately seen that for ACT LK formulae gs1 ps4 that are applicable to the model BMC offers very little improvement in both memory used and time taken Although we do not pay any overhead for using BMC we do not get any improvements in terms of resources used either BMC does not display a memory improvement because the difference in memory required to hold the initial state space and the entire reachable states is very low Ignoring the cost of checking the formulae MCMAS requires 570324 bytes to hold the initial state and only 588196 bytes to hold the entire reachable states i e the state space reaches a fixed point a difference of 17 KB Due to the lack of extra memory required to store the rest of the model when BMC can falsify the property in all but with Yps2 the benefits are not clearly illustrated For the three properties that are falsifiable Ygs1 Yss3 and Ygs4 we can easily identify that MCMAS only has to explore a fraction of the states it would usually explore when performing BMC MCMAS originally required 10 iterations to reach the fixed point in the state space for the book model and for Yss2 where the property is not falsifiable we can clearly see that BMC pays a very slight memory increase for performing 10 satisfiability checks in comparison to a single check The Correct Bit Transmission Problem Perri when evaluated on a c
65. at has been selected from that BDD Selecting a bad ordering can cause an unfavourable growth in the size of aROBDD The rest of this subsection is An example of how to represent a transition system as BDD and A demonstration of how reordering can effect the size of the BDD Figure 2 3 4 shows a simple transition system with a total transition relation We can easily see that the model has four states and as such each unique state in the model can be represented using two bits An assignment of Boolean variables to each individual state can be seen in Figure 2 2 Figure 2 1 A small transition system Figure 2 2 Variable assignments to states State 1 2 so SI s2 s3 Now that we have a unique bit string for each state in the model it is possible to construct a Boolean formula representing the transitions between each state The Boolean function Figure 2 3 represents the transition relation The function encodes each transition and then takes two Boolean assignments representing states the initial state the unprimed variables and the next state the primed variables If the transition exists in the model the function will evaluate to true and false otherwise Adapted from 64 15 Figure 2 3 A Boolean representation of the transition relation t 21 2 Z1 T2 ay A te A ng A T3 321 A729 A 2 A T3 321 A 22 A 2 A 2 ax A 2 A 2 A 722 lt l
66. ated in Section 2 3 1 a model M satisfies a formula y if the all the initial states Z are included in the set of states at which that formula holds That is MF ov iffZ C y This means that to check the satisfiability of the formula y we can construct and check the satisfiability of the formula L gt p where l represents a propositional atom that is true at the initial states of the model only This implication is implicitly true at all states except the initial ones the antecedent is false so the formula is true regardless of the value of the consequent MCMAS employs this method to check the satisfiability of a formula over an entire model If yl is equal to reachable states reach we can deduce that the formula holds at the initial states of the model More in depth implementation specifics of MCMAS including the construction of SATer x with the ex ception K are not discussed here The reader is referred to 49 74 for further information 37 3 4 Models MCMAS gt comes with a set of example models the following four of which all have properties that are express ible in ACTLK Some of the properties given below have been constructed for this work purely to adhere to the logic ACTLK The Bit Transmission Problem Imagine two processes a sender S and a receiver R who communicate over a possibly faulty communication line S continually sends a bit to R until it receives an ack from R R do
67. be seen in fig 2 6 CUDD s C API makes extensive use of operator over loading Importantly This represents the operation AND upon two BDDs anp can be used to calculate the intersection between two sets represented as BDDs This represents the operation or on two BDDs or can be used to calculate the union of two sets LJ between two sets represented as BDDs This represents the unary operation Not CUDD performs this operation in constant time 28 3We are dealing with a KT 45 logic and as such the relation is reflexive transitive and symmetric It should also be noted that CUDD supports Zero suppressed Binary Decision Diagrams ZDDs and Algebraic Decision Diagrams ADDs but as these do not concern this project they will not be covered here 23 Figure 2 6 An example C program using the CUDD library 50 int main int argc char argv Cudd bddmgr The manager bddmgr Cudd 0 0 BDD x bddmgr bddVar BDD y bddmgr bddVar BDD f x y BDD g y X if f g cout lt lt f is equal to g else cout lt lt f is NOT equal to g BDD Manager CUDD uses unique tables to store BDDs This ensures that each node is unique in this context unique means that there exists no other node labelled with the same variable which also has the same children Cache CUDD contains a cache that is used to store computed results allowing for
68. beca Models In Journal of Universal Computer Science vol ume 11 2005 6 pp 1054 1082 Fabio Somenzi CUDD CU Decision Diagram Package Release 2 4 1 May 2005 URL http www cs ubc ca ajh courses cpsc513 cudd ps Francesca Toni Notes from the course 474 Multi agent Systems Autumn 2008 URL http www doc ic ac uk ft teaching html Ingo Wegener Branching Programs and Binary Decision Diagrams Theory and Applications Society for Industrial and Applied Mathematics Philadelphia PA USA 2000 ISBN 0 89871 458 3 Michael J Wooldridge Reasoning about Rational Agents MIT Press 2000 Bozena Wozna Alessio Lomuscio and Wojciech Penczek Bounded model checking for deontic inter preted systems In Electronic Notes in Theoretical Computer Science volume 126 2005 pp 93 114 doi DOI 10 1016 j entcs 2004 11 015 Proceedings of the 2nd International Workshop on Logic and Com munication in Multi Agent Systems 2004 URL http www sciencedirect com science article B75H1 4FKXPY9 K 2 0a4c45371 53831ab07794690ed1 fae 97 98 Web References 63 64 65 66 67 68 ed 69 70 71 72 73 About CUDD The U Colorado BDD Package http www ece cmu edu ee760 760docs cuddv1 pdf Advanced Model Checking http www i2 informatik rwth aachen de i2 amc09 Akka http staf science uva nl lhendrik SystemDescription html BEEM BEnchmarks for Explicit Model checkers http anna fi muni
69. bounded verification is the number of iterations in which the algorithm generates new next states before a fixed point is reached Figure 5 11 depicts bounded model checking of a model containing two type 1 trains with a maximum service counter of 100 trying to falsify the Yrec2 property It is clearly illustrated in the figure that our im plementation is able to find a counterexample using resources proportional to that of the depth at which the property is found to be false The final group of results woRKING shows the attempted falsification of the same property but on a model with type 3 trains in which the property cannot be falsified In this case it can be seen that bounded verification only pays a very minor overhead in terms of memory used and time taken when compared to regular verifica tion of the same state space Due to the inability of this formula to be falsified on this model bounded model checking has to explore the same number of states and to the same depth as the standard approach 70 Figure 5 11 resource use of BMC against regular model checking with a model containing two type I trains with a maximum depth of 100 and various breaking depths Yrec2 Bounded Model Checking Resource Usage T T T T Memory 140 Time zzzz 4 States Sow Depth xcee00s 120 gt 100 g 100 A 3 Ne 2 80 Nee a v P N RSS
70. ce partitioning to allow for multiple hosts to perform bounded model checking on different areas of the state space The main consideration for this approach is in checking invariant properties expressing that a given condition must hold at every state in the reachable set Invariant properties in CTLK contain AG as the top most connective in the parse tree The simplistic parse tree for the formula AG 4 can be seen in Figure 4 4 This formula will be satisfied from the initial state if at every reachable state y holds Figure 4 4 The parse tree for AG y AG Our method places an extra restriction upon the logic ACTLK stating that AG is at the top we refer to this as ASCTLK The construction of the formula beneath this connective remains unaffected we allow regular ACTLK formula The falsification of a formula can be displayed by finding a single reachable state from the initial state in which the property beneath AG is no longer satisfied We have previously shown that NuSMV supports on the fly checking of invariant properties in a very similar way Section 2 3 8 In a Kripke model the transition relation is transitive we deduce here that the reachability between two states is also transitive if a state 1 is reachable from s and s2 from s then s2 is reachable from s We translate the problem of falsifying AG q in the initial state from finding a single reachable state in which g holds to finding a reachab
71. cking of CTLK MCMASMaster MCMASSlaver MCMASSlave2 Iterate To Seed Depth Check BMC B GenerateSeeds k Initialise Connect 4 ISPL Model ree Initialise Connect he Dee ees ISPLMpdel ig eee Trerate Seeds J Use Seed Iterate Depth Check BMC z result la ree Meee oy Seca ed Use Seed gt Iterate Depth Check BMC pezsi result Aiae mae ren a Aa B nnn 53 4 3 5 Consideration of Other Connectives Although we originally placed a restriction of ACTLK such that AG was the top level connective it is possible to extend our scheme to also support AF The immediate problem of a seed based approach to bounded model checking with respect to an AF for mula is that it is possible to find a counterexample to the original formula from a seed state even though the formula is true from the initial state For example if we take a model in which from the initial state AX holds then from the same initial state AF holds i e p E L s S Riu s Attempting to falsify the original property by checking the satisfaction of EG y as per the initial stage of our distributed method for this initial state will not succeed When BMC cannot satisfy an ECTLK formula the algorithm continues under the assumption
72. cz models BuDDy A BDD package http buddy sourceforge net manual main html CUDD Colorado University Decision Diagram Package http vlsi colorado edu fabio CUDD Eclipse http www eclipse org Flex http flex sourceforge net GNU Bison http www gnu org software bison Graphviz http www graphviz org Lufthansa Technik Aircraft maintenance http www lufthansa technik com applications portal lhtportal lhtportal portal requestednode 4248 amp _ pageLabel Template7_8 amp nfpb true amp webcacheURL TV_I Media Relations Media Archive Archive Press Releases Previous Press Releases Press Releases 1997 Maintenance_e xml MCMAS 0 9 6 2 http dfin dl sourceforge net sourceforge ist contract mcmas Q9 9 6 2 tar gz MCMAS vo 9 8 2 User Manual http www lai doc ic ac uk mcmas manual pdf NuSMV User Guide http nusmv irst itc it NuSMV papers sttt_j html node21 html PDMC Parallel and Distributed Methods in verifiCation http pdmc informatik tu muenchen de Rebeca Reactive Objects Language http khorshid ece ut ac ir rebeca The DDDMP package http fmgroup polito it quer research tool tool htm 99 100 Appendix A BMC Implementation in MCMAS Figure A 1 The extended type system of MCMAS A pair of a formula pair first actlk pair second ectlk typedef std pair lt modal_formula modal_formula gt modal_formula_p_pair A vector of formula pairs
73. d Table 5 6 Stress testing MCMAS Memoty is given in bytes Time in seconds O Ma Rege PSCC IM B Memory Time Ses Moy Time Sas 5 2131866612 8085 88 5834990 64694612 2 43 74017 10 1919076244 34383 60 4755710 319959508 84 51 587164 I5 1971699364 22448 24 3452620 961126804 1657 57 1853920 WORKING 1101036372 2836 36 2688260 1117194660 4007 68 2688260 5 1814837044 3487 12 8560450 829675748 406 35 1549040 IO 1371231508 3707 59 6195380 1380098852 7066 06 6195380 I5 1371165972 3917 96 6195380 1380098852 7086 08 6195380 The italicised results are those in which MCMAS failed to complete the verification of the model It can be seen from these results that there are cases in which BMC can halt and succeed whilst regular model checking halts and fails To attempt to see how robust our implementation was we performed more tests than depicted here We attempted to verify models containing up to 6 agents the maximum service depth was kept at 20 with varying depth breaking of 5 10 15 and a working model but all these models caused both regular and bounded model checking to fail Interestingly these results did not suggest that a memory limit of approximately 1 36 GiB which the latter results in Table 5 6 would suggest was the only limiting factor In a model with 6 trains MCMAS failed at a memory limit of 1 69 GiB and approximately 11970900 states nearly twice as many as shown in the table but after a t
74. d in the most simplistic of terms each variable is considered in turn and placed at every possible position once a best position has been identified this is the new location of the variable in the ordering NuSMV NuSMV 11 is an open source symbolic model checker it is a reimplementation of a model checker developed at CMU called SMV It supports both SAT based BMC for verification as well as BDD based satisfiability methods 12 Due to the fact that these methods are generally used to solve different types of problems it allows for interesting avenues of research In BDD based model checking NuSMV first builds up a finite state machine representing the given model it can then perform a various number of checks including fair CTL LTL via a reduction to CTL and others When operating in SAT mode NuSMV can either use its own built SAT solver SIM or it can write out 24 the SAT problem in the standard DIMACS format which allows for the use of external SAT based solvers e g CHAFF It supports the bounded model checking of LTL properties only During this procedure it interleaves problem generation and solution attempt via a call to a SAT solver and iterates until a solution is found or the specified maximum bound is reached 11 It is able to operate in a simulate mode in which the user can interactively select the behaviour that the system exhibits It also stores all of the traces of the model checking procedure for t
75. d by simply providing the model checker with a single state and then attempting a reachability check 3 2 CUDD Specifics The API provides the functionality for quantification of variables within a BDD The function ExistsAbstract 63 builds the following BDD where x y and z are the BDDs representing the variables that we wish to quantify with respect to Bp 4 x y z By An implementation of the above quantification using CUDD can be seen in fig 3 1 63 Conceptually ExistsAbstract and the similar function Exists use Shannon s expression 16 to construct the quantified BDD f e fleo V x Fle 1 35 This quantification attempts to express if it is possible to make the BDD representing the function f By true by an assignment of either false right hand side or true left hand side to the variable x f z o is a restriction upon the variable x as used in the function f to a value of b 0 1 The BDD for a restriction to 0 can be computed by removing the node n representing the variable x and redirecting all incoming edges to succg 7 A restriction to a 1 can be computed in the same way but the incoming edges are directed to succ n Figure 3 1 Existential quantification of variables within CUDD build the extracted BDD xyz BDD temp x y Zj h there_exists xyz f BDD h f ExistAbstract temp 3 3 MCMAS Internals This section attempts to inform the reader of some implementation
76. ddq2jjtrr9 Cindy Eisner Using Symbolic CTL Model Checking to Verify the Railway Stations of Hoorn Kersenboogerd and Heerhugowaard In Software Tools for Technology Transfer volume 4 1 pp 107 124 URL www haifa ibm com dept svt papers trainssttt ps 19 J Ezekiel and A Lomuscio Combining fault injection and model checking to verify fault tolerance in multi agent systems 2009 20 Johannes Faber Verifying real time aspects of the european train control system In 17th Nordic Workshop 21 22 23 On Programming Theory 2005 pp 67 70 Ronald Fagin Joseph Y Halpern Yoram Moses and Moshe Y Vardi Reasoning About Knowledge MIT Press 1995 Alex Groce and Daniel Kroening Making the most of bmc counterexamples In Electronic Notes in Theoretical Computer Science volume 119 2005 2 pp 67 81 Proceedings of the 2nd International Workshop on Bounded Model Checking BMC 2004 URL http www sciencedirect com science article B75H1 4FNNN9F 6 2 9aac9INbbeVe97 e2453c29c665bc2349 Wiebe van der Hoek and Michael Wooldridge Tractable multiagent planning for epistemic goals In AAMAS 02 Proceedings of the first international joint conference on Autonomous agents and multiagent systems ACM New York NY USA ISBN 1 58113 480 0 2002 pp 1167 1174 doi http doi acm org 10 1145 545056 545095 94 24 25 26 27 28 29 30 31 Michael Huth and Mark Ryan Logic in Comp
77. deep counterexample Due to the cyclic design of the model which allows agents to eventually return to a previous local state the counterexample can be found from every seed state Another problem arises here because the set of next states can transition into the current reach set the next set for this model subsumes the reach set This means that it is possible to have a seed state that is the same as the original initial state as specified in the ISPL model Our distributed approach has been benchmarked using the faulty train gate controller but given the ability to find counterexamples from any state in a faulty model the distributed falsification of properties is shown in a particularly good light This also gives rise to the fact that the property is falsified by the first slave to return a counterexample usually the first slave that connects to the master instance This does not invalidate or make these results any worse it is simply an unintended bias of our method to this particular model Machine Specification The networked hosts of these benchmarks were identical machines to that used to perform the previous bench marks The machines used were vector30 through to vector40 when idle The seed states were saved to the networked file system bitbucket a networked file server for un metered disc space running a 813 GiB XFS file system with a 4 KiB block size in a RAID configuration Each slave was co
78. e BMC performs more of a bug hunting approach and given that most systems do contain bugs BMC can perform favourably One area that quite a lot of focus has been given to is the verification of the correct functionality in railway systems For instance in 20 Faber looks at the verification of various aspects of the new European Train Control System ETCS His work looks at the safety of the railway to prevent crashes A fuller evaluation of applying symbolic CTL model checking to railway interlock software is presented in 18 2 5 1 The Train Gate Controller Model An example of a simplified model based upon a real world train system is that of the Train Gate Controller system Alur et al 1 devised this model for use with the Mocna model checker Their model is based around the idea of two circular train tracks each with a train travelling in a different direction At a particular part of the track the trains must use a tunnel in the original user manual this was a bridge but this has evolved over time and we will be using that formalism but the tunnel can only accommodate a single train At the point at which the tracks merge there exists a controller that controls signals for entry to the tunnel If a train sees a green light it knows it is safe to enter the tunnel Within Mocna each of the trains is modelled as a reactive module that can perform two basic actions arrive and leave Each reactive train module contains a singl
79. e and does not hold at this state As such g is Inrr The pre image calculation pre5 In1T returns the empty set due to the restriction that the starting states of the transition relation must be in the reachable set of states and that in this model there are no states that transition into INIT 61 Therefore EX y does not hold in the initial state so the ECTLK formula is false and we do not have a counterexample to our original formula We shall refer to the set of the state at which a particular formula 4 holds at a particular bound as sounp When we increment k to a depth of 1 giving us y 1 In1T s5 the pre image computation of this set gives us InIT Again the pre image of Inrr is empty whilst the pre image of s5 is In1T So we have found a witness of the existential formula meaning that we have a counterexample to the universal formula As such the BMC algorithm can terminate 5 142 SATEG Figure 5 2 Checking AF 4 Figure 5 3 The labelling function and existential pre image function for Figure 5 1 2 prej Inir pres si1 Inrr s4 pre3 s2 s1 pre3 s3 52 pres s4 53 52 In Figure 5 1 2 the state pre image function can be seen in Figure 5 3 assume that s3 and as such L gt y In17 81 82 54 Using Sargg from Section 2 3 1 the reader is reminded that Y XMpre3 Z we can then calculate the fixed point for the satisfiability of an EG form
80. e enumerated type representing the current state of the train away wait tunnel Each train also has access to a signal external variable signal The train module acts as follows when it arrives at the tunnel it sends the event i e it performs the action arrive to the controller and checks the signal variable state wait Ifthe signal is red the train waits and continually checks the signal When the signal turns green the train enters the tunnel state tunnel and on its exit from the tunnel the train sends the signal leave to the controller such that it knows that the train is no longer in the tunnel To support multiple trains within this environment Alur et al extended the model such that there were two copies of signal variable signalW and signalE representing a train approaching from the east or from the west Similarly the events arrive and leave were prefixed with the approach direction such that the controller could differentiate between the events it witnessed In the proposed model the controller initialised both of the lights to red When a train arrived and signalled to the controller it would check if the other light was red and only then would the signal be changed to green allowing the train access to the tunnel When a train leaves the tunnel and informs the controller of this fact it would then change that light back to red The behaviour of the trains can be seen in Fig 2 10 The edge from the wait state
81. e method and an implemen tation of that method Finally in Section 4 4 we conclude by setting forward a model that could be used to show the possible benefits and limitations of each of these methods 4 1 BDD Based BMC Our main algorithm Algorithm 13 performs an incremental state space generation including a check at each depth We continue this process until either we find a counterexample to the original formula or we reach a fixed point in the state space 4 1 1 BDD Based BMC with Early Termination Algorithm 13 BDD BMC w ACTLK Formuta T Inrt1at State Trans TRANSITION RELATION BOOLEAN x yp Y y ECLTK Formuta 2 Reach Z Reach BDD while True do if y Reach then return Farse Counterexample to ACTLK formula found end if Reach lt Reach V Reach Trans if Reach Unchanged then break Fixed point reached 1o endif H E E ERN R ae 11 end while 12 return i Y Reach Conceptually whilst similar to both Cabodi s approach of Algorithm 12 and Copty s approach of Algo rithm 11 ours differs significantly in one major way Both of the original BDD based BMC methods merely performed a set intersection between either the reach set Algorithm 12 or the frontier set Algorithm 11 of 41 states with a target error state In comparison the algorithm we set forward here performs a full satisfiability check as per Section 3 3 3 on the whole state space It can
82. ed Knowledge The work presented here was mainly an attempt at a proof of concept for showing that BDD based bounded model checking could be at all effective when checking epistemic modalities This we were successful in doing A possible extension would be to allow for the checking of both Common and distributed Knowledge C and C and D and D 6 2 4 Heuristics for Seed State Generation In our distributed model checker we do not handle seed state generation at all intelligently In an attempt to find a counterexample more quickly we could prioritise certain seeds in the order of verification For example in an attempt to falsify AG p V q seed states in which p or q hold could be prioritised This would possibly allow for a state in which the invariant ceases to hold being found sooner i e If p holds in the seed state then BMC attempts to find q 6 2 5 Intersection Based BMC The previous attempts at BDD based BMC all attempted an intersection based approach that is being able to represent the set of bad states and then check if any of these states are inside the current reach Now we have a way of saving the states to disk we could use this to create and hold a single error state allowing for an intersection based approach to model checking We could also use MCMAS s RedStates to represent the set of error states and if an intersection of the reachable states and these red states is found then an error ha
83. ej Inir pres si Init Le oe ne E pre3 s2 si pre3 s3 82 83 a pre s1 81 52 pre s2 81 52 Gr pater ee a ee gee ee a Depth 2 pre 53 s3 In Figure 5 2 l s1 1 s2 That is l s1 and 1 s2 are local states that are indistinguishable for Agent X the epistemic relation is represented by the dashed line The epistemic accessibility relation is reflexive as such every state is related to itself Y is the set of states returned from the knowledge pre image function upon the y Depth o Depth 1 Depth 2 Iteration 0 Iteration 0 Terion 0 Kx y 2 s1 s2 Terion Kx y o 0 Kx hh 5 2 1 Correctness of the Algorithm Satz The algorithm Satx is sound and complete Proposition 1 For every ECTLK formulae y IS F iff Satz p G G is the set of global states Proof gt By induction on the structure one Let y K w and let IS g E K w This means that there exists a g GA g i g such that IS g F Y By the induction step g y also we have Ri g g by definition of R This implies that g Ki w ie g y O Proof lt Straightforward as the induction steps above are symmetrical O 1Adapted from 53 65 5 3 Model Checking of ASCTLK with Seed States The method of partial state space evaluation that we use in our method of bounded model checking is both sound and complete when we look at the restriction we placed upon
84. el To allow us to effectively investigate the efficiency of our BMC implementation we required not only a scalable model The model also required the existence of meaningful and expressible properties that could be falsified at a variable depth but under certain parameters to the model could equally be true The resulting model is one that builds on Kacprazak s parameterised model of 29 allowing for a variable number of agents in the system Inspiration for the design of the new model was also taken from 19 in as much as this work was the catalyst for designing a possibly faulty multi agent system Our model is a combination of these two factors in the context of the Train Gate Controller model 2 5 1 Where it is necessary to make a distinction between the original model and our new model our model shall be referred to as the faulty train gate controller 4 4 1 The Faulty Controller We scale the number of agents by allowing the controller to handle the merging of an arbitrary number of tracks into a single track in the tunnel An automaton displaying the new behaviour can be seen in figure 4 11 the descriptions of the transitions including assignments and required preconditions from this automaton are shown in table 4 12 Note to the reader The protocol for an agent in a given local state can be inferred from the given precon ditions for each possible action in that state In a faulty model with N trains the controller contai
85. emp first Formula lt lt actl to_string lt lt is FALSE in the model lt lt endl cout lt lt If we have remaining unchecked formulae if bmc_formulae gt empty Clear the old formulae is_formulae gt clear And construct a new is_formulae vector for modal_formula_p_pair_vector iterator iter bmc_formulae gt begin iter bmc_formulae gt end iter modal_formula_p_pair temp modal_formula_p_pair iter modal_formula actl temp first is_formulae gt push_back act1 Use the regular check_formulae method check_formulae 105
86. es explored by every single host in the verification process Again a weakness in these results is that as soon as one slave returns a counterexample the whole verification process terminates and any intermediate results for the other slaves are lost Tables 5 10 5 12 and 5 14 show the decrease gained by using distributed bounded model checking against serial bounded model checking A decrease below one indicates an increase for that model method Depth 3 Table 5 9 ee resource usage of distributed bounded model checking i a seed depth of 3 PBMC Moe Slave Max __ Ma Toal aa e a a 70396964 825572 69742244 69459 69742244 69534 198678532 825572 175579220 258699 175579220 258774 39705828 825572 42212644 41681 42212644 3001032 Table 5 10 A comparison between BMC and distributed bounded model checking at a seed state generation depth of 3 Decrease Desa id Memory Time Save For a seed state generation depth of 3 Tables 5 9 and 5 10 we can see that for models in which the property can be falsified type 1 and type 2 the distributed approach is able to find a counterexample with less memory and less states which as stated above is to be expected in this model Verification of type 1 trains takes longer when distributed because bounded verification is able to quickly find a counterexample whereas our distributed approach has the various overheads the master to iterate over all of the reachab
87. es nothing until it receives a bit from S and then infinitely sends an ack to S If S receives the ack from R then S knows R has received the bit Given that S does not acknowledge the ack R will never know if S received the ack An expression such as this can be formalised in CTLK 41 TS F AG recack Ks Kp bit 0 V Kp bit 1 Lomuscio et al 42 extended this model to include possible failures Their work added the following faults to the receiver 1 The protocol for the agent no longer enforces it to send an acknowledgment when it receives a message and 2 It allows for the possibility that it can send an acknowledgment without previously receiving a message ACTLK Properties The property is true on the original BTP model and false on the faulty model Yarpl AF K Receiver bit or K Receiver bit1 The Dining Cryptographers The Dining Cryptographers is a problem that was introduced by Chaum in 1988 to illustrate the anonymous sending of messages with unconditional send and recipient untraceability The idea is as follows three cryp tographers are out for dinner and learn that their meal has already been paid for but they desire to discover who has paid one of them whilst staying anonymous or their employer the National Security Agency They devise the following protocol each of the cryptographers flips a coin behind their menu so that only they and the person to their right can see the output The cryp
88. etween states Lp j l encodes a backward loop connecting the k state to the state in the symbolic k computation j forO lt 1 lt k 19 The unrolled transition relation at bound k M is calculated as follows 48 MP Zs woo A AN AT wij Wit1 j JELL i 0 Where wo and wi j for i 0 k and j E LLY are vectors of state variables LL fr Finally the ECT L formula has to be translated into a propositional formula p The translation of this formula differs for paths that are and are not k loop paths These can be distinguished with Ly l At each state Wm n within a k path of index n the temporal sub formulae of the formula being translated to the k path n are translated to the k paths that start at that state Starting with wo Wm nVi E LL y uel is the translation of the formula y at Wm to a propositional formula Translation of an ECTL formula 48 pe Dl Wire p ok p Wain yee lev we pave olka typ Exe VY H wmm wo A la 1E LL k k EGY VY H wmn wos AV Laid A A P iE LL I 0 j 0 k E ppu Yo H wmn wos A v e In At lt 1E LL 0 To summarise to create the propositional formula that will be satisfiable for a model M and formula y at a bound k First the algorithm has to create M p which is representative of the unrolled transition relation at bound k Next the algorithm forms 4 M Which will be true if and only if
89. fter a certain number of next state computations These are then used to start bug hunting with multiple parallel SAT instances Figure 2 4 1 outlines their approach The large triangle represents the state space that can be realistically explored by conventional SAT based BMC Instead BDDS are used to generate an under approximated state space the ovals From this partitioned state space many parallel SAT instances are started at various depths within the state space ds1 dsa each representing a different BMC SAT instance This is what allows their process to reach errors that would otherwise be difficult to catch Figure 2 9 Seeding Multiple SAT BMC runs from POBDD reachability image adapted from 26 ds1 dso ds4 The justification for their work is to perform efficient bug finding 25 and as such their approach only 29 looks at verifying invariant properties Due to their under approximated state space their method also sacrifices completeness although it is sound by construction 26 Ifan error is found by a seed state then the error exists in the design and a trace can be generated from the initial states to the state where the invariant ceased to hold 2 5 Verifying Correctness in Real Life Models There is growing interest in being able to perform model checking on real life industrial models The rise of bounded model checking using SAT solvers caused the number of industrial cases to ris
90. g bound is lower than the minimum amount of joint actions performed by both the train and the controller to allow the train to enter the tunnel This is reflected by the similarities between the results for a breaking bound of 1 and 3 once the breaking bound is higher than the minimum number of joint actions we see a decrease percentage of resources required A point of distinction is that Figure 5 14 shows that although BMC may not show drastic improvements in terms of memory usage over full verification it does not show any significant penalties either The point made previously about this model showing that the breaking bound is less than that of the number of joint actions to enter the tunnel is also reiterated in this graph 71 Figure 5 12 Resource usage in a model with two type 1 trains and a maximum counter of 20 Yrec3 Bounded Model Checking Resource Usage LLLA SX sq w WORKING 18 15 I2 9 6 PY 423 SELES ER RA i RSRSRS S YL EE LE LE I Yt WEL Ke iW SS 6Q0 _ MELLO SSS SSS LLL gn x x x x x x x x O e e O e 0 a O o0 Ko a H H H SIDINOSIY jo Breaking Threshold of Train Figure 5 13 Resource usage in a model with two type 2 trains and a maximum counter of 20 Yrec3 Bounded Model Checking Resource Usage QLLLLLLLL Mw th ae RRR
91. g formula to see the effective of attempting to verify properties exposed to combinatorial explosion They generalise the property p2 with N trains N N p2 N AG 7in_tunnel gt Ketrain A in_iunmnel A Ktrain VV in_tunnel i 2 based on the bridge model I have re written them here in the LTL style as used previously in this report as well as adapting them to the tunnel scenario This can really be seen as a liveness property but the authors do not state this 33 34 Chapter 3 Preliminaries 3 1 Discussion on Prior Art Nearly all approaches to bounded model checking look at conversion of the model and the property to that of the Boolean satisfiability problem This is not an ideal solution there is no obvious way to directly convert an existing model checker using binary decision diagrams to the SAT problem without significant re engineering Plus this then adds an extra requirement for either an external SAT solver or the implementation of one This point is clearly illustrated with the exception of NuSMV by the distinct lack of existing model checkers supporting both BDD methods and a translation to SAT The conversion to SAT also ignores a lot of optimisations such as variable reordering which have been designed specifically for model checking The research that has been put into optimising BDD based methods heavily eclipses that of the research for model checking methods based on SA
92. gents a Purchaser and a Supplier The Supplier waits for an order from the purchaser and decides if it should accept or rescind the order The agent then waits to receive the payment which it can then accept or decline The e goods books are made available to the purchaser if the purchaser is unhappy with the goods the supplier can offer a remedy or a refund If at any stage the supplier does not follow protocol i e it performs terminate action the contract is violated The Purchaser initiates a contract with the supplier pays for the goods and downloads them If the Pur chaser is unwilling to accept the goods it can return them to the Supplier The agent can violate the contract by refusing to pay for the goods by performing the terminate action ACTLK Properties Yss1 AF K Supplier contract_success False The supplier at some stage knows that the contract has ended successfully That is both parties have adhered to the protocol and both goods and payment have transferred hands This is violated at any stage by either of the parties by performing the terminate action Yss2 AG payment_received gt AF supplier_compliance True When the supplier re ceives the payment it complies with the rest of the transaction ps3 AG payment_received gt AF AX supplier_compliance False When the supplier receives the payment from the next state it complies with the trans
93. global function get_nK_states BDD get_nK_states BDD state string name Look up the agent from its name basic_agent agent is_agents name Project the local state over phi BDD localstate agent gt project_local_state state v J and that state over the reachable states return reach localstate The function in figure 4 2 builds upon the previous method it takes the set of the states y the first argument state and a unique ID for the agent string agent Once a reference to the agent is found from is_agents the BDD representing the local state for that agent is constructed which is subsequently anped with the set of reachable states The resulting BDD represents the set of all reachable states in which the local state is indistinguishable from a local state in p for the given agent Figure 4 3 displays our additions to a skeleton modal_formula check_formula The integer constant 50 stored in op Section 3 3 2 is the formula identifier that MCMAS uses to represent formula of the kind KAcenr p _ The arguments to the formula K AGENT and y are stored in the obj local variable obj 0 is a pointer to agent class for AGENT whilst obj 1 is a pointer to the modal formula representing 4 7In the spirit of Karnaugh maps 46 Figure 4 3 A reduced check_formula method BDD modal_formula check_formula Returns a BDD encoding the set of states in which
94. gt gure 5 P Proel e model checking lt enterI enter enter gt lt idle back back gt lt idle break signal gt II x lt idle signal signal gt lt idle break enter gt x 8 8 SRP lt idle leave signal gt i lt enter1 signal service gt lt idle break signal gt lt enter1 signal service gt B lt idle break signal gt 4 lt enter1 signal service gt lt idle leave service gt lt enter1 signal signal gt lt idle leave signal gt 6 17 lt enter1 signal signal gt lt idle break signal gt g 8 a lt idle leave signal gt E lt enter1 signal service gt 8 lt idle break signal gt lt enter1 signal enter gt B lt idle break signal gt y lt enterI enter enter gt lt idle break signal gt lt idle break enter gt lt enter2 break signal gt II 23 Io serv E E A lt idle break service gt lt enter2 leave service gt lt idle leave signal gt lt enter2 break service gt lt idle leave enter gt 81 5 4 5 Stress Testing MCMAS BDD based BMC as shown previously can falsify properties on models requiring less memory than conven tional verification uses This means that there will be cases in which BDD based BMC will be able to verify the model whilst other verification techniques will be unable to complete Results showing this can be found in Table 5 6 T is the number of trains M is the maximum service counter B is the depth of the breaking boun
95. hat when a seed state has zero successors the slave returns maybe true Figure 4 5 The initial state of seeded BMC up to a seed depth of k k 1 Dashed states represent the set of seed states A return of false from a single slave means that a counterexample has been found from the seed state to which it was allocated As previously stated not only are the seed states reachable from the initial state by construction but the state in the seed tree that invalidated the property is also reachable represented by Seed 3 in fig 4 6 When a slave instance informs the master that a counterexample has been found the master can then kill off the other slave instances reducing the over processing It is then possible for the master instance to return a definite value of false to the user Unlike regular BMC which finds the minimum counterexample seeded BMC may not find the most optimal counterexample given that the execution trace found in the node could be longer In contrast a slave returning maybe true means that the slave cannot falsify the property from its given seed state This is not a complete indication of the actual result of the verification process It is possible that the 49 Figure 4 6 Seeded BMC in which one of the slave instances starting from Seed 3 can falsify the property fis gt selected seed for that slave may not have a reachable state that violates the invariant property it may not
96. he generation of counterex amples and witnesses NuSMV provides two alternative 76 ways of calculating the satisfiability of invariant properties that is properties of the form AG y An invariant property of that kind means that in all of the reachable states p must hold Rather than calculate the fixed point of AG y using gfp p A AXZ NuSMV can handle it in two ways If the full set of reachable states from the initial state has already been computed then the check is as follows Reachable Z C y where the function Reachable represents the set of reachable states from a given state It can check the property on the fly rather than calculate the full state space NuSMV can do the following check at each step of the reachability analysis Reachable Z C vy The function Reachable computes with a set of reachable states from the given state within k steps Verifying multi agent systems with NuSMV_ Raimondi et al 51 36 investigated a method for the verifica tion of multi agent systems with NuSMV as part of their tool set NuSMV was used as a tool to generate the set of reachable states for the model This was then processed to encode the epistemic relations and then passed to a third tool Akka 65 which was used to verify the epistemic properties The processing stage parsed the NuSMV output of all of the reachable states and generated the epistemic relation to the local states that were invariant across
97. i gt 7 Reach One Shot BMC The second method of BMC we have implemented is BMC with a one shot heuristic Algorithm 15 The crux of this approach is rather than checking yl against the current reachable states at every depth we build up the reachable states to the given one shot depth and only then do we compare y against the reachable states If the model satisfies y at the one shot depth the algorithm returns false p is the counterexample If we are unable to satisfy the negation we return true although this could possibly be an incomplete result as we have not built up all of the states Algorithm 15 One sHot BMC q ACTLK Formuta Z IniT1a State Trans TRANSITION RELATION OneShotBound int STRING X BOOLEAN x p aw p ECLTK Formuta 2 Reach Z Reach BDD for k 0 to OneShotBound do 3 4 Reach lt Reach V Reach Trans 5 if Reach Unchanged then 6 return FIXED POINT CASE t Y Reach 7 end if 8 end for 9 return ONE SHOT CASE y Reach The method employed in Algorithm 15 differs significantly from that of Algorithm 13 The original algo rithm will only terminate once a complete result has been found either from reaching a fixed point or from finding a counterexample The one shot BMC as presented here may return an incomplete and useless result As discussed previously the motivation for this approach is that the calculatio
98. ime of roughly 1500 seconds 5 5 Evaluation of One Shot BMC The proposed method of one shot BMC was an attempt to alleviate the memory overhead associated with performing a satisfiability check at every depth This BMC related penalty was our original justification for turning off automatic reordering within CUDD but as one shot BMC does not have this problem we were able to benchmark against a version of MCMAS linked against a vanilla CUDD zero sized initial cache with both variable reorderings and garbage collection enabled We used the script developed to perform iterative one shot model checking upon two models one with two type 2 at a breaking depth of 20 Figure 5 7 and the other with three type 2 at a breaking depth of 7 Figure 5 8 attempting to falsify Ysrr2 As before a decrease below 1 represents that the system had an increased resource requirement in that configuration As expected one shot BMC can in terms of memory used out perform the standard approach to model checking when the property can be falsified In a model in which a counterexample cannot be found the veri fication process performed by one shot is identical to that of regular model checking This is illustrated by the identical memory usage between the two approaches in a working model This approach was designed to alleviate the memory overhead at the expense of time and with the exception of the anomalous result at a breaking depth of 1
99. imilar to aircraft maintenance checks 73 where a plane requires a set of a mandatory checks after a certain number of flight hours This is still only a preventative measure and not a guarantee that no fault will occur before this 55 Figure 4 13 An automaton modelling a train from the faulty Train Gate Controller model t2 ti t3 t4 tg t5 t6 t7 Type 3 Correct table 4 16 Trains can never perform the break action the only action that can be performed in the tunnel is the leave action This is the same behaviour for the trains as in the original system 1 The tables for the descriptions of the actions of the three types of faulty train allow for implicit requirements for some actions to take place For example we require that once the service counter reaches the maximum counter that the train is serviced this requirement is modelled by the subsumption of the preconditions of the transition t2 by those of transition t in table 4 14 The action Back can only be performed when the service counter is strictly less than the maximum counter this means that the only action that is allowed by the protocol from this state is the SERVICE action A second example of this is the requirement that a train must break if it is in the tunnel and the service counter reaches the maximum counter again this can be seen in the subsumption of the preconditions of the transition tg by transition t7 table 4 14 Figure 4 1
100. ing In Tools and Algorithms for the Construction and Analysis of Systems volume 2619 2003 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 00898 9 ISSN 0302 9743 Print 1611 3349 Online 2003 pp 34 48 doi 10 1007 3 540 36577 X_4 URL http www springerlink com content 600uvxx254x1k8ta Christel Baier and Joost Pieter Katoen Principles of Model Checking The MIT Press May 2008 ISBN 026202649X M Benerecetti F Giunchiglia L Serafini Massimo Benerecetti and Luciano Serafini Model check ing multiagent systems In Journal of Logic and Computation volume 8 1998 pp 8 3 A Biere A Cimatti E Clarke O Strichman and Y Zhu Bounded Model Checking In Advances in Computers volume 58 2003 A Biere A Cimatti E M Clarke M Fujita and Y Zhu Symbolic model checking using SAT proce dures instead of BDDs In DAC 99 Proceedings of the 36th ACM IEEE conference on Design automation ACM New York NY USA ISBN 1 58133 109 7 1999 pp 317 320 doishttp doi acm org 10 1145 309847 309942 Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu Symbolic Model Checking without BDDs In Tools and Algorithms for the Construction and Analysis of Systems volume 1579 1999 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 65703 3 ISSN 0302 9743 Print 1611 3349 Online 1999 pp 193 207 doi 10 1007 3 540 49059 0_14 URL http www springerlink co
101. ins with a full service depth of 20 when checking various formulae Bounded Model Checking Time Usage i Preci ae Prec ZZZ2 Precs MASSS Tech RRR 120 H 100 ia 2 100 by z F N f 80 H ig 60 b 7 g p o 4 2 R IN 408 IN NS 40 H l iN IN sl 20 WIN W 4 AWA A A 0 ZASS N N NS IN 3 4 8 12 I6 WORKIN Breaking Threshold of Train 75 Figure 5 19 Time required for three type 2 trains with a full service depth of 7 when checking various formulae Bounded Model Checking Time Usage T T Precl 140 Prec ZZA Yrecd NNSS Proc RRRS oa 100 ie x 100 i F ZN Z ed 80 H i E GN Ei Y IN i we Ne Ne 40 N 3 P In YN 20 L NC 7X ir o P Ae 0 oe UN Ss JN 4 5 WORKING 3 Breaking Threshold of Train 5 4 3 MCMAS 0 9 8 5 Examples After running all of the examples that are included with MCMAS it is immediately obvious that with the exception of one model they are all very small trivial examples This means that the time required to check these models is very small when measured with usr bin time they all take 0 0s of real time to complete This means that with the exception of the larger model BMC never displays an overhead or a benefit when looking at time alone The Book Store The benchm
102. ion and the current reach set The disjunction of these next states with the current reachable states results in the next set of reachable states at a BMC depth of k 1 with k applications of the transition relation In the actual implementation the set of next states is stored in a temporary variable at function not loop scope allowing us to easily determine when a fixed point has been reached If the previous and the current set of next states are the same then the algorithm can no longer find any new reachable states the next set is a subset of the reachable states and as such fixed point has been reached 4 1 2 Variations on BDD BMC Checking the satisfiability of y at each successive depth is not a free operation This calculation may consume additional memory resources above and beyond the cost of only building the reachable states This is an unwanted overhead when compared to performing non bounded BDD based model checking Also the calculation of the set of satisfiable states is not an instantaneous process this results in a time penalty at each depth Again this is an overhead not exhibited by non bounded model checking In an attempt to alleviate the space time penalty of checking at each successive bound heuristics can be used to decide if a check should be performed at a specific bound This procedure is highlighted in Algorithm 14 It can be seen on Line 4 that we only perform the satisfiabili
103. ironment An imple mentation of such techniques into an existing model checker for multi agent systems MCMAS is presented as well as the provision of a scalable scenario that allows for a constructive evaluation of our methods against the existing implementation When variable reordering in the underlying library is disabled the serial bounded technique is shown to be effective for satisfiable formulae the overhead imposed is negligible The initial results for our distributed tech nique demonstrate that it out performs the sequential approach for falsifiable formulae Experimental data indicates that increasing the number of hosts improves verification efficiency Acknowledgments First and foremost I wish to thank my supervisor Alessio Lomuscio for his help and encouragement through out the project This project would not have been anywhere near as successful without his enthusiasm and willingness to listen to my problems as well as reading and replying to the gargantuan emails I started to send towards the later stages I would also like to thank Marek Sergot for reassuring me of this project s potential during the early stages and for marking this report Michael Huth for being amenable to my visits to his office to ask what must have seemed to him very random questions although they were all very related to this project William Harrower William Jones and Robin Doherty for their friendship and support thro
104. it uses to store the seeds as well as the depth to which it should perform BMC until the seed states are 50 generated The only extra argument the slave takes is a file which it should use as the initial seed state It can be seen that this method requires the model checker to be able to save and retrieve states from disk The DDDMP Library 79 which works with CUDD defines file formats that can be used for the storage of BDDs We use this library in both the master and the slave The slaves use Algorithm 13 which already takes an initial state from which it should start the state space traversal conventionally MCMAS would pass the initial state specified in the model We now pass the seed state as the initial state as specified in the arguments to MCMAS Figure 4 8 The master iterates over all of the states in the current frontier set writing each of them to the given directory and then exits This is highlighted in Figure 4 9 which generates the seeds when BMC reaches the specified depth Figure 4 8 The internals of the slave instance to load the given seed state DDDMP specifics Dddmp_VarMatchType varmatchmode DDDMP_VAR_MATCHIDS Dddmp_VarInfoType varoutinfo DDDMP_VARIDS Parse the file name char filename 100 strcpy filename initbddfile c_str Load the seed state DdNode b Dddmp_cuddBddLoad bddmgr gt getManager varmatchmode NULL NULL NULL DDDMP_MODE_DEFAULT filename NULL Con
105. itrary order in a parallel manner The intended result is hopefully a quicker and more efficient verification whilst avoiding the slow down associated with swapping Distributed techniques build on parallel methods and allow for the problem to be distributed between a number of machines each with disjoint memory For instance there has been research into parallelising BMC such that multiple solvers look for counterex amples at different lengths 27 2 4 1 Grid Based BMC with Seed States Another approach towards distributing bounded model checking is to start at different depth seed states within the state space 27 The approach that Iyer et al propose in 27 25 26 is to attempt to find various candidate deep reachable states that can be used as seeds to run parallel SAT solvers from in a grid environment They argue that when starting SAT based BMC at a deeper state it is possible to find states deeper in the model as well as locate errors that may not be locatable by existing methods Their method uses partitioned ROBDDs and under approximate to build up a partitioned state space such that generating the seeds remains tractable but this is done at the expense of completeness 26 Once the memory use of the system exceeds a threshold they then select only a subset of the next states to continue with forward verification Seed states are written out as conjunctive normal form clauses at regular intervals e g a
106. le state in which AG p does not hold That is we find a reachable state in which EF y holds We use lyer s terminology of seed states to represent the different reachable states in which we attempt to show the falsiftability of AG y 4 3 2 Outline of Grid Based BDD BMC In the design approach we have taken for this algorithm we have two types of hosts a single master and multiple slaves The single master instance performs initial verification and seed generation After this the node acts solely as a co ordination host between the multiple slaves Our method works in three stages Fixed Depth BMC Initially we perform a heuristics based approach to BMC we check the satisfiability of EF y at every depth attempting to find a counterexample until a predetermined depth Generate Seed States Once the given depth has been exceeded each unique state in the frontier set of next states is recorded in a way that makes them amenable to either network transfer or to storage to a backing device Parallel Seeded BMC Parallel BMC solvers search for a counterexample Algorithm 13 each starting with a different frontier state 48 The first two stages in the above are only performed on the master instance after which all of the compu tational work load is ofHloaded to the slaves Although as we have presented it here the master only performs BMC up to a specific depth our method allows us to be
107. le states and write them to disk as well as both instances having to read and parse the same ISPL code It should be noted here that the time taken for a slave to connected to the master subsequent communication to take place between the nodes and seeds to transfer to and from bitbucket is assumed to be negligible A model with type 3 trains is expected to under perform in distributed bounded verification because every single node for every single seed has to be explored to the fixed point which means the same state space is computed for every seed If one slave returns faster than another slave and has used less resources this is the maximum value used This is because when one slave finds a counterexample the master kills offall other instances which causes any running instances of MCMAS to be terminated without the recording of any statistics 84 The avid reader might wonder why verification from certain seeds may require more memory than the full BMC approach this is caused by reordering Starting from a different seed state may result in a different variable ordering reach BDD This in turn may result in some slaves requiring more memory to represent the set of all reachable states when compared to the memory required in serial bounded model checking Depth 4 Table 5 11 The resource usage of distributed bounded a at a seed depth of 4 BMC Mee Shve Mm Max Toal sl eee See ee aa ee Ge 70396964 1156980
108. ledge Common Knowledge 21 The modal operator Cry is true if all agents in the group T know y and every one in the group I knows that everyone in I knows y and so on and so forth The following abbreviations are useful to help define common knowledge Erg 9 Ery Ery Etto ErEfy As a formal definition TS g E Cry iff Vk 1 2 TS g E Ef The computation of common knowledge calculated using a fixed point is based upon the following equiv alence 21 Cry Er y A Cry IO Definition 12 Semantics of CTLK 52 For an interpreted system ZS global state g and a formula TS gFp iff pe V s TS gF y if gk TS gFEypvw iff LS gF y or ZS gF v TS gEypAw iff S g y and ZS g F4 TS gFEXy iff 3r Ji mi g ATi F IS g F EGy if dn Ji m gAVj inj Fo IS gF E pUy iff dn Ji m gA A3k gt 0 miy FYAVYj i lt Lj lt k tE IS gF Kip iff Yg G g ig implies TS g F y IS g Ery iff Yg G g E g implies TS g Fy IS g Cry iff Yg G g g implies ZS g E Y The relation E is the union of all such that E while amp is the transitive closure of the r r r icer E Ti represents the global state at position 7 in a run 7 The modalities of AX EF AF AG AU can be derived as in CTL 2 3 Model Checking Model checking 15 13 is a method of formal verification used to verify the correctness of a system
109. m content vf 286k9mq9jp05dh Randal E Bryant Graph Based Algorithms for Boolean Function Manipulation In IEEE Trans Comput volume 35 1986 8 pp 677 691 ISSN 0018 9340 doi http dx doi org 10 1109 TC 1986 1676819 Gianpiero Cabodi Paolo Camurati and Stefano Quer Can BDDs compete with SAT solvers on bounded model checking In DAC 02 Proceedings of the 39th conference on Design automation ACM New York NY USA ISBN 1 58113 461 4 2002 pp 117 122 doi http doi acm org 10 1145 513918 513949 A Cimatti E Clarke F Giunchiglia and M Roveri NuSMV a new symbolic model checker In International Journal on Software Tools for Technology Transfer volume 2 2000 p 2000 93 11 13 poy 14 15 16 17 18 Alessandro Cimatti Edmund Clarke Enrico Giunchiglia Fausto Giunchiglia Marco Pistore Marco Roveri Roberto Sebastiani and Armando Tacchella NuSMV 2 An OpenSource tool for symbolic model checking In Computer Aided Verification volume 2404 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 43997 4 ISSN 0302 9743 Print 1611 3349 On line 2002 pp 241 268 doi 10 1007 3 540 45657 0_29 URL http www springerlink com content 7hrq3m38utrrgywb Alessandro Cimatti Enrico Giunchiglia Marco Pistore Marco Roveri Roberto Sebastiani and Ar mando Tacchella Integrating BDD Based and SAT Based symbolic model checking In Frontiers of Combining Systems v
110. milarly for a5 ag is the joint action in which the train leaves and signals to the controller same as for ag and TRAINz2 Figure 2 12 Descriptions of Actions in the Train Gate Controller 29 Action Agent Pre State Post State a rom away wah train wait tunnel ag controller green red i train tunnel away controller red green 7 away wail traing waite tunnels a5 controller green red P traino tunnels away2 6 controller red green In 31 30 attempt to devise epistemic propositions based on a single controller and two trains They define the following two propositional atoms in_tunnel and in_tunnelg that take the obvious meanings the valuation function determining which states they hold as defined as in_tunnel E V g iff ltaam1 g tunnel forg E G in_tunnelg V qg iff ltaaia g tunnel forg E G Upon these propositional atoms they then build the following formulae H Yo 7AX 7in_tunnel It is possible that the first train will be in the tunnel in the next state N p AG in_tunnel gt Kirain in_tunnel2 When the first train is in the tunnel it knows the second train is not in the tunnel w p2 AG nin_tunnel gt Kirain in_tunnel2 A Kirain in_tunnel2 When the first train is not in the tunnel it does not know if the other train is in the tunnel or not The novel approach presented in 29 is to build a parameterised model and a supportin
111. model checking when checking formulae that are satisfiable on the model although possibly paying a slight overhead still performs with a resource requirement equivalent to that of conventional satisfiability model checking The crux of this problem is that the evaluation of these formulae on models is not known prior to starting the verification process Model checking is generally used with properties that the author believes are true with the intention of bug hunting In these circumstances attempting to use bounded model checking may be a better approach to take 87 88 Chapter 6 Conclusions 6 1 Project Review 6 1 1 Contributions The goal of this project was the development of BDD based bounded model checking techniques for a branch ing time logic and its epistemic extensions The main contributions that this project provides are Theoretical contributions Three different possible ROBDD based bounded model checking techniques full one shot and distributed as well as the BDD based methods required to also be able to check properties pertaining to knowledge upon these state spaces Considerations have been given towards the validity of calculation of the satisfiability sets for formulae based on existing fixed point methods The technique put forward in this report for evaluating ECLTK formulae on partial state spaces is a wholly original contribution The related recent developments in this field have only
112. much more flexible in our approach Realistically we can use any heuristic for instance seeds can be generated when The memory used to represent the reach set becomes too large e g it reaches the maximum memory of the machine which would mean that the swapping of the program s memory to disc would soon occur The number of states in the next set exceeds a threshold e g the state threshold could be related to the number of nodes in the grid The time taken to calculate EF y on the current reach exceeds a certain value 4 3 3 Uniqueness of the Approach The uniqueness of our approach hinges on attempting falsification in a concurrent way between multiple hosts Once the initial phase has terminated and the seed states have been generated fig 4 5 the master instance can then disseminate each of the seed states between the nodes If there are more seed states than slaves the master instance can re allocate a slave with a new seed state once it has completed its original processing The slaves all use Algorithm 13 which proceeds until either a counterexample is reached or a fixed point is established This means that the slaves can return two results false or maybe true Algorithm 13 takes an initial state as an argument here where this algorithm is utilised in a slave the initial state is the seed state allocated to that slave The final line of the algorithm Line 12 is replaced with p Reach such t
113. multiple global states Akka is a Kripke model editor that also supports model testing The methodology employed for this procedure is outlined in fig 2 3 8 Figure 2 7 Methodology employed to verify multi agent systems with NuSMV 51 XML Editor XML to SMV Specify interpreted system y Translate specification into a NuSMV model translator Java Y Use NuSMV to calculate reachable states NuSMV y i Build an epistemic model Parser Y Model check epistemic formulae Akka It should be noted that given that NuSMV was used just as a tool to generate the set of reachable states it would not be possible to make use of NuSMV s alternatives for handling invariant style properties Another approach was attempted by Raimondi et al 37 to reduce CTLK specifications to ARCTL Action Restricted CTL 45 specifications ARCTL is an extension to CTL in which qualifications are allowed over labelled paths interpreted over labelled transition systems ARCTL has the same temporal operators as CTL except that it allows for the restriction of paths whose actions satisfy a formula y There exists an experimental 25 extension to NuSMV that supports an extended syntax and allows for the verification of ARCTL properties that could possibly be a translation of CTLK specifications 37 provides an extension to the SMV language for the description of interpreted systems and CTLK formulae MCMAS Model Checking Multi Agent Systems MCMAS 40
114. n gains from the optimisations such as sift ed variable reorderings arising from an auxiliary library 5 4 2 The Faulty Train Gate Controller The faulty train gate controller model as presented in Section 4 4 provides us with a unique model for bench marking our BMC implementation This is because in a faulty model i e one that contains either type 1 or type 2 trains eventually there will be a demonstrable counterexample prior to reaching a fixed point in the entire state space Using a model such as this allows us to demonstrate the possible benefits and drawbacks of using such an approach under different circumstances such as a different number of agents using parameterised formulae with various size formulae or with formulae that are true on the model and as such a counterexample cannot be found In the graphs that follow the resource usage of our implementation is expressed as a percentage of that which is required to verify the same model in MCMAS s default approach Memory time and states should be immediately obvious as to which metrics they represent We can calculate the percent used by BMC with respect to full verification as follows BMC value full value 100 The depth metric represents the number of iterations i e checks that bounded model checking has to perform until it finds a counterexample or the state space reaches a fixed point The depth of model checking when performing full un
115. n of t yl at each depth is not a free operation it can affect the amount of memory used by the model checker In MCMAS s case this is the size of CUDD s cache This results in a memory increase that is not displayed in regular verification This algorithm avoids this overhead by only calculating the satisfiability set once and then exiting The implementation of this algorithm is not supposed to be used directly by a user due to the possibility of returning a false positive Instead we have developed a wrapper script to MCMAS that attempts an iterative depth approach to verification of a given model When one instance of MCMAS finishes we regain all of the memory used by that instance Then when a new instance of MCMAS is launched we start with a fresh 43 CUDD cache This implementation is intended to overcome the memory overhead of our first method but does this at the expense of time Each time we start with a deeper one shot bound we have to effectively recalculate the set of reachable states which may have already been calculated by the previous instance 4 1 3 An Implementation The remainder of this section discusses an actual implementation of our algorithm into MCMAS The devel oped code can be found in Appendix A In the following we attempt to outline the significant additions to the MCMAS code base to implement bounded model checking New Types Figure
116. nge i e at the end of a path through the model of the reachable states for which there does not exist a successor state In the following subsections we demonstrate that these fixed point methods are in fact correct even when used upon truncated paths through the model they do not return false positives 5 141 SATEXx To show the falsification of a universal next formula AX we attempt to check the satisfiability of its existen tial dual EX As noted in Section 3 3 3 the formula the implementation tries to satisfy is the following Init EX y that is are the initial states for the model a subset of the states in which EX y holds Within MCMAS checking an atomic proposition returns all of the reachable states in which the proposi tion holds This is performed through set intersection upon the set p and reach see Section 2 3 8 The pre image calculation is based upon vRT the per agent transition relation vector all calculations upon this set are also taken with conjunction i e intersection of the reachable states We can perform set intersection of the reachable states and the states returned by the pre image function such that we only get a set of states which is subsumed by the reachable set Figure 5 1 Checking AX y ESERE E ee ee Depth o Depth 1 In Figure 5 1 presume that L y 51 2 53 s4 ie L y Inr7 55 Initially at a depth of o the reach set contains only the In rT stat
117. nnected to the master and every host to bitbucket using gigabit ethernet 5 6 1 Depth of Seed States We attempted to falsify properties on three different models each with 3 trains a maximum service counter of 7 and a breaking threshold of 4 The difference between the three models was the type of trains in each model for the models that contained type 3 trains the property was not falsifiable All of these benchmarks were performed using a single master and three slaves It would be possible to perform next reach set minus here to give a strict set of next states but our implementation does not do this 83 In Tables 5 9 5 11 and 5 13 BMC memory and states is the total number of states and the memory bytes used to represent those states which our original BMC algorithm had to explore to find a counterexample or in the case of a working model reach a fixed point Master memory bytes is the memory required to explore the model up to the given depth prior to seed state generation whilst states is the number of seed states that are generated which in this model as noted above is in fact the set of reachable states Slave max memory bytes is the maximum memory used by any one slave during the entire process This value represents the maximum resource requirement for each slave for the particular model when performing distributed model checking The total states represents the summation of all the stat
118. nous system evolutions they have performed since they were last serviced The service action resets the service counter to zero whilst the break action occurs when a fault occurs in the train Faults occur in trains when they are not serviced regularly enough i e the service counter exceeds a predefined threshold and can only be exhibited when the train is in the tunnel An automaton displaying the state transitions for this faulty train model can be seen in figure 4 13 The trains also contain a max counter that once the service counter reaches this value forces a train to perform the service action We have modelled the faulty system with 3 types of trains Type 1 Faulty table 4 14 Once the service counter exceeds the breaking threshold the trains can non deterministically break in the tunnel Once a train has broken in the tunnel it is unable to repair itself and is in the tunnel for the rest of the run of that system If the service counter reaches the maximum counter the train can no longer non deterministically choose the leave action and definitely breaks Type 2 Faulty table 4 15 Same as type 1 with the exception that all the non deterministic break action allows is for the train to get stuck in the tunnel for a single evolution The train can break an infi nite number of times displaying the behaviour of always being in the tunnel or can eventually perform the leave action This can be seen as s
119. ns N cs edges table 4 12 each of which is the transi tion of a different train entering the tunnel This is represented in the table with the unquantified variable 54 Figure 4 11 An automaton modelling the controller in the faulty Train Gate Controller model C3 C1 C4 C5 C2 Figure 4 12 Descriptions of actions of the controller in the faulty Train Gate Controller model Label Action Assignments Preconditions C1 IDLE C2 EXIT_TRAIN C3 train _waiting true Train action SIGNAL C4 C5 ENTER_TRAIN i 0 Train action ENTER train _waiting false train _waiting true In comparison to the original train gate controller where both of the actions enter and exit were joint actions for the controller and a train in our faulty model we only have the per train joint action enter The controller has been extended to function under the assumption that trains take at most two synchronous system evolutions to leave the tunnel This is represented by the guard on the action Cg and the additional DLE action c1 This guard only enables the transition back to the green state when a counter representing the num ber of evolutions since the first train entered the tunnel has exceeded the threshold of two 4 4 2 The Faulty Train We have adapted the trains from the original model such that they now contain a SERVICE and a BREAK action The trains also contain an additional service counter representing the number of synchro
120. olume 2309 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 43381 1 ISSN 0302 9743 Print 1611 3349 Online 2002 pp 265 276 doi 10 1007 3 540 45988 X_5 URLhttp www springerlink com content ncfgrv2rf9kgwvqh E M Clarke E A Emerson and A P Sistla Automatic verification of finite state concurrent systems using temporal logic specifications In ACM Trans Program Lang Syst volume 8 1986 2 pp 244 263 Edmund Clarke Armin Biere Richard Raimi and Yunshan Zhu Bounded Model Checking Using Sat isfability Solving In Formal Methods in System Design volume 19 2001 1 pp 7 34 ISSN 0925 9856 Print 1572 8102 Online doi 10 1023 A 1011276507260 URL http www springerlink com content 6r6m9p 34 jh1a229 Edmund M Clarke and E Allen Emerson Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic In Logic of Programs Workshop 1982 pp 52 71 Edmund M Clarke Orna Grumberg and Doron Peled Model Checking MIT Press 1999 Fady Copty Limor Fix Ranan Fraer Enrico Giunchiglia Gila Kamhi Armando Tacchella and Moshe Y Vardi Benefits of Bounded Model Checking at an Industrial Setting In Computer Aided Verification volume 2102 2001 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 42345 4 ISSN 0302 9743 Print 1611 3349 Online 2001 pp 436 453 doi 10 1007 3 540 44585 4_43 URLhttp www springerlink com content 4p130c
121. on to clean them up these will cause an additional overhead that would not be present otherwise As such disabling this functionality is not necessarily a beneficial improvement for BMC Resource decreases for a build of CUDD with these features disabled can be seen in Table 5 4 The final result for a four train model italicised in Table 5 4 is a test that did not complete CUDD halted the execution of MCMAS with a non zero exit code and the string Unexpected error indicating a serious and unknown problem The test failed after 3101 51 s for regular verification 3100 11 s for BMC exhausting 967 09 MiB 967 14 MiB 3See 58 for more details 4Both of these function bodies now contain return as the first line 69 Table 5 4 Statistics with no default cache and with reordering and garbage collection both disabled Model Decrease TM B Memory Time Stare To allow for coherent and fair results the rest of the results in this chapter with the exception of the one shot results in Section 5 5 have all been gathered with an MCMAS build with a zero sized initial CUDD cache disabled asynchronous variable reordering and no garbage collection even though the latter two of these detrimentally hamstring the model checker Our justification for disabling these features is that we wished to evaluate our novel approach rather than benchmarking a specific implementation and assess the benefits that such an implementatio
122. orrect model for the bit transmission problem Figure 5 21 is true which means that BMC should pay an overhead The case here is that the fixed point is reached within two state space 76 Figure 5 20 The Book Store Bounded Model Checking Resource Usage Memory 140 Time zzz 4 States os Depth zee 120 gt 100 100 80 H 60 of Resources 40 H 20 F Wl o A nrw SHH WG GW Formula iterations meaning that BMC only performs two extra checks The memory required to both check and store the entire reachable states is negligible which means that BMC does not display any disadvantage The Faulty Bit Transmission Problem In the faulty BTP model Figure 5 22 Pgrp1 is falsifiable BMC can find a counterexample in the initial state Again we do not see any benefits in resource requirements This is because as the size of the model is small there is very little memory difference between holding just the initial states and holding the set of all reachable states the model has two initial states and only 18 reachable states in the full state space This means that although we can terminate early this is not demonstrable The initial states are representable with 545444 bytes BMC requires only 160 bytes to falsify the property whilst full verification only requires an extra 2848 bytes to represent and check the entire state sp
123. owledge pertaining to and express belief about their environment 2 2 1 Agents Definition 6 Agents 59 are autonomous systems that Perceive the environment in which they are situated via sensors Act upon the environment via effectors Are designed with certain performance requirements Maintain environment in a certain state Achieve certain state of its environment An agent 43 is Situated in an environment Capable of autonomous action Capable of social interaction with peers Acting to meet its design objective An agent has a set of local states that represents the current configuration of the agent This config uration might be an assignment to the local variables of the agent or the values within a knowledge base of known facts An agent has a set of actions A and a function that maps from the current state of the agent to the set of enabled actions a protocol for that state P L 24 It is then possible to define an evolution function for an agent T LXA gt L As well as having a set of local states the agent also has an initial state Z that the agent starts in This allows us to define the idea of a run of an agent Definition 7 59 A run of an agent is a set of states and actions o ao 1 1 such that eg ZT the initial state ag E P eq and Vi a E P e T ei ai er41 2 2 2 Interpreted Systems An interpreted sys
124. ows the total size and the average seed size in bytes required for storing the seeds at different depths in a model with three type 1 trains a maximum counter of 7 and a breaking threshold of 4 Table 5 16 Disk space used to hold the set of seed states Depth Seeds Toral Average 4416 552 41400 552 I92I2I 552 072 677426 552 099 The file system tested used a 4 0 KiB block size This means that the disk size for storing 1227 seeds was in fact 4 9 MiB rather than the total file size of only 652 KiB From this we can draw the conclusion that our distributed implementation requires almost 8 times the disk space than if a small block size was used but by today s standards 4 9 MiB is virtually nothing On average the size for an individual seed is approximately 552 bytes This allows us to realistically rule out any real network overhead for results previously with respect to time taken Our justification for this is y real k overhead for results p ly with respect to time taken Our justification for th We feel obliged to point out that not every seed state has an enabled joint action available from it This is why the total number of states 51017544 is less than the number of seeds multiplied by the fixed point states 41681 1227 In this case there are 3 seed states that do not have an enabled action and as such do not have any successor states The fixed point of states is immediately reached and a path
125. quired or time taken for falsifying different properties in the same model The formulae Yrec4 and Precs both use their parameterised versions and are based on the number of agents trains in the model The resource usage illustrated in models that have shallow breaking bounds Figure 5 17 and Figure 5 19 both display the same correlation of results as previously Again in these particular models there is a mini mum number of joint actions required until a train can enter a tunnel if the breaking depth is lower than this minimum number of moves then no savings can be garnered In the graphs showing memory usage Figure 5 16 Figure 5 17 we can see that there is a slight overhead when checking Precs at a deep breaking depth but this overhead appears to be less in the working model This is because the number of iterations required to find a counterexample at the deepest breaking bound is more than for reaching a fixed point in the working model For example in a model with 3 trains and a maximum counter of 7 BMC requires 15 iterations to find a counterexample at a breaking depth of 5 but in the working model it only requires 11 to reach the fixed point The figures depicting the time taken for verification Figure 5 18 and Figure 5 19 are the only ones that show any form of significant overhead for bounded model checking When checking the property Yrec1 it can be seen that in both models bounded model checking is not preferable It should be
126. re ment of having a representation of the entire state space that calculating the satisfaction of a universal formula would require Model checking the existential fragment of CTLK ECTLK can follow the same procedures as for model checking ECTL Algorithm 2 but with the addition of checking the dual of K K One possible way of calculating the satisfiability of a ae p would be to evaluate K a gens 7 using Algorithm 8 Although this would be a feasible strategy it has the disadvantage that it pays an overhead to perform two negations as well as being a rather inelegant solution A preferable way of calculating this procedure would be to provide and implement a direct method for Saty that is not dependent upon Sat Conceptually our method for satisfaction of formulae of the form Kacenr can be seen in algorithm 16 To find the set of states in which the previous formula holds we first calculate the set of states in which y holds Next we utilise the relation pre for the given agent which returns the set of all global states in which the local state for the agent is invariant as per Algorithm 8 Algorithm 16 Satz y Formuta i AGENT set of STATE x X Satornx y 2 Y pre X i 3 return Y 4 2 1 BDD Based Satz The first stage towards making a BDD based Sarg is to be able to easily locate and represent the reachable states for which the local states are invariant for a given agent The process for calculating
127. rn SATEx 1 else if p E p Up2 then return SaTgu 1 2 else if p EG y then ro return SatgG 1 11 else if p K y then 12 return Satk 13 else if p Ep y then 14 return SaTg 15 else if p Cp y1 then 16 return Satc 1 17 end if o2 2N oxe The functions EXer x EGerix and EUcrix are the same as in Section 2 3 1 except they use the relation R rather than the Kripke structure transition relation and G is used instead of S As for CTL we have to define functions to find the pre image for a set of states where pre is the function for the modality K pre and pre are defined similarly As previously X is a subset of G 7 is an agent and I is a set of agents pre X i g G 3g gKig and g X pre X T g EG Jg gREg and g X pre X T g EG Ag gREg and g X and g SaTerix y re is based on 2 2 3 prea Algorithm 8 Satx y Formuta i AGENT set of STATE ur X SaTerx 79 2 Y pre X i 3 return Y 21 Algorithm 9 Satg y Formuta T set of AGENT set of STATE tz X SaTorx 7y a Y pre X T 3 return Y Algorithm 10 Satc y Formuta T set of AGENT set of STATE x X SaTorix 7y YG while X Y do X Y Y pre X T end while return Y Y N DRRR Y 2 3 7 BMC for Multi Agent Systems Bounded model checking of interpreted system
128. roaches to Agent Based Systems volume 2699 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 40665 5 ISSN 0302 9743 Print 1611 3349 Online 2002 pp 115 125 doi 10 1007 b11729 URL http www springerlink com content qc9jeklam3w0tmgp A Lomuscio F Raimondi and M J Sergot Towards model checking interpreted systems In AAMAS 03 Proceedings of the second international joint conference on Autonomous agents and multiagent systems 95 Ha 37 bmi 38 tami 39 Sie 40 42 Simmi 43 44 ACM New York NY USA ISBN 1 58113 683 8 2003 pp 1054 1055 doi http doi acm org 10 1145 860575 860792 Alessio Lomuscio Charles Pecheur and Franco Raimondi Automatic verification of knowledge and time with nusmy In IJCAI 2007 pp 1384 1389 Alessio Lomuscio Hongyang Qu and Monika Solanki Towards verifying compliance in agent based web service compositions In AAMAS 08 Proceedings of the 7th international joint conference on Au tonomous agents and multiagent systems International Foundation for Autonomous Agents and Multiagent Systems Richland SC ISBN 978 0 9817381 0 9 2008 pp 265 272 Alessio Lomuscio Hongyang Qu and Monika Solanki Towards verifying contract regulated service composition In ICWS 08 Proceedings of the 2008 IEEE International Conference on Web Services IEEE Computer Society Washington DC USA ISBN 978 0 7695 3310 0 2008 pp 254 261
129. rom every seed 5 6 2 Number of Slaves Because every seed state in a model with type 1 or type 2 trains can lead to a demonstrable counterexample this makes using this model difficult when demonstrating how varying the number of seeds can affect the time taken for verification To allow for some meaningful results we used a model containing three type 3 trains with a maximum counter of 7 In this model no counterexample can be found meaning that every single seed state is explored to the fixed point of states Table 5 15 Time for seeded bounded model checking when compared to BMC for a varying number of hosts when a counterexample cannot be found F Hosts Time Decrease Table 5 15 illustrates the reductions in time gained through using different numbers of slaves at a seed generation depth of 3 The original time taken by BMC was 1 90s Although the table displays increases we can see that as the number of hosts is increased this increase gets lower As such in a model where a counterexample could be found we can see that using more slaves would decrease the verification time and increase verification efficiency 5 6 3 Disk Space Overhead Our current distributed implementation saves the set of all seed states to disk This is done through the DDBMP library version 2 0 3 It would be unfair to present the previous results without discussing the over head that saving these states to disk imposes Figure 5 16 sh
130. rstand due to the values chosen by a SAT solver By harnessing MCMAS s coun terexample methods we should generate understandable counterexamples when using bounded model checking 2 Biere et al 7 state that bounded model checking finds counterexamples of minimal length As such we should ideally generate counterexamples that are smaller or of equal length to that of regular verification A comparison between the length of the counterexample generated between MCMAS s regular behaviour and our implementation can be seen in Table 5 5 The counterexamples have been constructed for various formulae in a two train model composed of type 2 trains a maximum service counter of 20 and a breaking depth of 10 Table 5 5 Length of counterexamples generated between BMC and full verification Method Preci Yrec2 Yrec3 Precs Precs Regular 25 17 4 4 12 BMC 13 16 4 4 FAIL Figure 5 25 and Figure 5 26 show a counterexample for Yr c1 using regular and then bounded model checking The authors argue that the counterexample in Figure 5 26 is significantly easier to understand lt action action action gt represents the actions performed by the Controller Train and Train2 re spectively It can clearly be seen in the second figure that in the transition from state 10 to state 11 Train1 performs the break action and from then on that train is in the tunnel which invalidates the liveness property in the final state for both tr
131. s 47 35 46 62 is based upon the logic of CTLK and builds upon the bounded model checking method for ECTL The syntax of ECTL definition 3 has to be first ex tended to give an epistemic modality different from that of CTLK Syntax of ECTLK 35 As for ECTL definition 3 with the following If isa formula Kj is a formula i Agents In BNE y p y YV y EXy EGy E pUy Kip ECTLK also includes the following modalities Cry and Epy for T C Agents but these have been omit ted here for brevity The epistemic modalities as defined for the existential fragment of CTLK ECTLK are defined as the dual of those from CTLK that is def gt def lt ip Z AC ny def Eip AF Ay The modality Kj stands for agent i considers it possible y 62 21 Semantics of ECTLK 62 Again as per the ECT L semantics but with TS gFKiy iff 3g G g ig ATIS gF 6 22 Bounded Semantics of ECTLK 62 The definition of an interpreted system 2 2 2 allows for the specification of multiple initial states the set Z BMC reduces this to a single initial state 4 IS gF Kip iff 3r Paths n 0 e and Jo lt ci lt ck TS i E p and g T i In the above g and g are global states G is the set of all global states Ky holds in the global state g if there exists a global state g such that the local state for the agent i is invariant between the two and also holds in g
132. s become even more dependent on these systems and the systems themselves become increasingly more complex bugs in these systems can easily be overlooked Currently there is a migration from a testing approach to a more thorough formal methods approach to this problem The term model checking applies to a collection of formal techniques for the analysis and exhaustive state space exploration of these reactive systems Formal methods have led to a rise in tools such as model checkers which attempt to prove the correctness of software However these methods either require an abstracted model of the system and as such are not entirely representative of the entire system or they consume a lot of resources be these time or memory to perform the task with which they are presented The infamous state space explosion problem arises from the attempted verification of systems or software which contain a large number of concurrent processes The resulting interleavings can lead to an unfavourable amount of permutations of state orderings and these in turn lead to the explosion Bounded model checking BMC Section 2 3 5 on the other hand is an attempt to reason about the full system without the requirement of exploring the entire model 1 1 1 An Illustrative Scenario Consider an autonomous agent such as NASA s Mars Spirit and Opportunity both of which landed on Mars in 2004 The rovers were programmed to
133. s been located 90 6 2 6 Saving Reach to Disk in One Shot BMC In the same vein as the previous point given that MCMAS can now save a set of states to disk using DDDMP when we perform one shot BMC rather than throwing away the entire set of reachable states we could save the current reach set to disk When we start a new instance of MCMAS we can get a cleared CUDD cache but we do not lose the previous reach This would save on over calculation 6 2 7 More Models Benchmarks To provide a more thorough evaluation of our BMC implementation we could attempt to check with more benchmarks A set of examples such as BEEM BEnchmarks for Explicit Model checkers 66 could be used The original train gate controller model that our version was based upon is included in this set 6 2 8 Better Use of CUDD CUDD provides API calls to clean up temporary variables from the cache to limit the amount of memory that is used The two calls Cudd_RecursiveDeref and Cudd_Deref can be used to protect a return result but delete intermediate results calculated by a function 9I 92 Bibliography x R Alur T A Henzinger F Y C Mang S Qadeer S K Rajamani and S Tasiran MOCHA User Manual In cMocha Version 1 0 1 Documentation URL http mtc epfl ch software tools mocha doc c doc Nina Amla Robert Kurshan Kenneth L McMillan and Ricardo Medel Experimental Analysis of Different Techniques for Bounded Model Check
134. setting up all of the state variables the transition relation etc MCMAS required in the same model as the above 721188 bytes to represent the single initial state which then increased to 4152900 bytes to represent all of the 10605 in the fixed point state space The results of performing the same evaluation as above but without a default CUDD cache size can be seen in Table 5 2 Interestingly reducing the memory required to hold the initial state also reduced the total memory required to represent the full state space regardless of the method of verification performed 6210388 bytes originally 4152900 with the tweaked CUDD vector35 in the Department of Computing at Imperial College London 67 Figure 5 10 CUDD s default constructor with additional comments initial size of sub tables define CUDD_UNIQUE_SLOTS 256 default size of the cache define CUDD_CACHE_SLOTS 262144 Cudd C The initial number of BDD variables unsigned int numVars Q The initial number of ZDD variables unsigned int numVarsZ Q The initial size of the unique tables unsigned int numSlots CUDD_UNIQUE_SLOTS The initial size of the cache unsigned int cacheSize CUDD_CACHE_SLOTS Maximum memory occupation 0 is unlimited unsigned long maxMemory 9 Table 5 2 The relative reductions in memory time and states explored with no initial CUDD cache Model Decrease PT M B Memory Time Seve
135. some hidden anomalies happening behind the scenes that we are unable to detect To be able to properly evaluate the effectiveness shown when comparing bounded and conventional model checking it would be advantageous to have an internal visualiser for MCMAS There have already been at tempts at state space visualisation but this is only half the story It has been shown that for bounded model checking to be shown as advantageous we have to disable variable reordering and to a lesser extent garbage collection in the underlying library Although we have provided conjecture as to why this leads to more favourable results for bounded model checking it would be helpful if we could have more of an insight into the BDDs that are used to represent the state space Such a tool which could also be hooked into CUDD could be used to analyse the variable reorderings used at run time This would paint a better picture for model checker designers such that they can be aware of the behind the scenes optimisations that the library provides 6 2 2 Counterexample Generation for K In our current implementation we do not directly support counterexample generation When we find a witness to the negated formula we generate this from the satisfiability of the K modality and not the K modality A simple extension would be to see if generating the counterexamples with K can lead to shorter or more under standable counterexamples 6 2 3 Common and Distribut
136. spect to the current reach check_formulae_BMC Tf we satisfy them we exit the loop if bmc_formulae gt empty continue We re now searching a deeper bound k Construct the next set of states for unsigned int i 0 i lt agents gt size i nextl vRT il nextl Exists v nextl1 nextl next1l SwapVariables v pv nextl Exists a nextl1 Construct the new set of reachable states From the union of the current reach and the next ql reach next1 Tf the set of reachable states hasn t change We ve reached a fixed point if ql reach cout lt lt Fix point reached lt lt endl break else reach ql If not store the new reachable states 104 Figure A 6 The second half of the BMC method in MCMAS Printing out the values for each formula and a final check for formulae we have been unable to falsify When we reach here we ve either Reached a fix point of the state space Or disproved all of the formulae Tf we ve disproved any formulae with BMC if bmc_false_formulae gt size We print them out cout lt lt The following formulae have been verified lt lt using BMC on the negation lt lt endl for modal_formula_p_pair_vector iterator iter bmc_false_formulae gt begin iter bmc_false_formulae gt end iter modal_formula_p_pair temp modal_formula_p_pair iter modal_formula actl t
137. struct a BDD representing this state BDD temp bddmgr b Assign the state to both initial states and the initial reach states in_st temp reach temp BMC continues as previously Our Java wrapper contains Slave and Master classes each of which provide an interface to the two types of MCMAS instances The master acts as coordinator to the whole process performing the initial BMC and assigning states in an iterative manner to each of the slaves until a desired result is reached The slave instances connect to a given master and await information pertaining to the seed state which they should use After a slave has completed BMC from the given slave it conveys the result of the verification including statistics such as memory use back to the master When a slave indicates to the master that it has found a counterexample for its seed state the master then terminates all of the other slaves causing the verification of the other seed states to halt We implement this in a basic way by closing all of the sockets used by the slaves to communicated with the master Exception handling for a closed socket is used on the slave terminating the execution of MCMAS and exiting the Java process when this exception is detected A sequence diagram displaying the whole process can be seen in Figure 4 10 51 Figure 4 9 The internals of the master instance to save the next set of states to a file k is the current
138. t lt lt lt tp A 2 A 1 A T3 It is not hard to see how the labelling function can be represented in the same way The function for each variable will evaluate to true if the propositional atom holds in that state or not and false otherwise Figure 2 4 shows one possible BDD representing the function It uses the following variable ordering 1 lt T2 lt x lt xh The BDD contains 8 nodes and 16 edges each BDD has two outgoing edges Figure 2 4 One example of ROBDD for the transition relation in 2 3 The BDD in Figure 2 5 represents the same Boolean function except that it uses a different variable ordering x lt x lt 2 lt xh This second reordering only requires the ROBDD to have 6 nodes and 12 edges It is quite obvious to see why when using ROBDD to perform model checking selecting a good variable reordering is preferable as it allows for efficient state space handling 16 Figure 2 5 A smaller ROBDD representing the same transition relation 2 3 2 3 5 Alternatives to BDD Based Model Checking BMC amp SAT One alternative to symbolic model checking based on BDDs came with the introduction of bounded model checking BMC 7 5 6 14 BMC searches for the minimum length counterexample that violates the system specification The algorithm looks for a counterexample with an increasing length k 0 1 and checks if there exists a computation path in the model that violates the system
139. tate tunnel if broken true and state tunnel state tunnel and broken true if state tunnel and Action break state wait and serviced serviced 1 if serviced lt 20 and state wait and Action state wait and serviced serviced 1 if serviced lt 20 and state away and Action state tunnel and serviced serviced 1 if serviced lt 20 and state wait and Action and Environment Action enterl1 state away and serviced serviced 1 if serviced lt 20 and state tunnel and Action The only edge case is that the train cannot be serviced in the tunnel state away and serviced 20 if serviced 20 and state tunnel and Action leave end Evolution 60 end Agent Chapter 5 Evaluation 5 1 Fixed Point Methods on Non Total Transition Relations The core of any model checker is its implementation of the SATer x algorithm of Section 2 3 1 The sub procedures of this are based on either a least or greatest fixed point calculation i e the calculation continues until the result stabilises These methods rely on the serial transition relation of a Kripke structure M S Z R L Section 2 1 That is for all states s S there exists a state s S such that s s R When performing BDD based bounded model checking using these procedures the transition relation is not guaranteed to be serial It is quite possible that at our current depth there may be states on the fri
140. tem is a semantic structure representing the temporal evolution of a system of agents 52 56 We are now assuming that we have a set of n agents i i 1 the local states for an agent i are now represented as The same is true for the actions A agent i s actions the initial state Z agent t s initial state and the protocol P agent i s protocol The set of n agents acts within an environment L g which can also be modelled with a set of states This can be seen as a special agent that can capture any information that may not pertain to a specific agent Definition 8 Global States The set G of global states of a system is G C Lix X Ln XLE A tuple g l1 ln lz E G can be seen as a snapshot of the current system where each of the li Li If g is a global state then l g represents the local state of agent 7 in the global state g If we make the assumption that an interpreted system is a synchronous one that is all of the agents within the system transition at the same time then we can define the global transition relation T GX AIX X An gt G In addition to this we also have an evolution function that determines the transitions for an individual agent between its local states For an agent 2 the evolution function t is as follows ti Li X Le X A1 X X n X p gt Li Similarly we have an evolution function for the environment s local states t p tg Lge XA X
141. tems via Unbounded Model Checking In Formal Approaches to Agent Based Systems volume 3228 of Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 24422 6 ISSN 0302 9743 Print 1611 3349 Online 2005 pp 189 212 doi 10 1007 b105317 URL http www springerlink com content 8d9etbvuymu8nubx M Kacprzak A Lomuscio and W Penczek From Bounded to Unbounded Model Checking for Tem poral Epistemic Logic In Fundam Inf volume 63 2004 2 3 pp 221 240 ISSN 0169 2968 Magdalena Kacprzak Alessio Lomuscio and Wojciech Penczek Verification of multiagent systems via unbounded model checking In AAMAS 04 Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems IEEE Computer Society Washington DC USA ISBN 1 58113 864 4 2004 pp 638 645 doi http dx doi org 10 1109 AAMAS 2004 296 32 Joost Pieter Katoen Concepts Alogirthms and Tools for Model Checking Semester 1998 1999 33 34 35 36 Saul Kripke Semantical Considerations on Modal Logic In In Proceedings A Colloquium on Modal and Many Valued Logics Helsinki 1962 L Lamport Proving the Correctness of Multiprocess Programs In IEEE Trans Softw Eng vol ume 3 1977 2 pp 125 143 ISSN 0098 5589 doi http dx doi org 10 1109 TSE 1977 229904 A Lomuscio T asica and W Penczek and Bounded model checking for interpreted systems Prelim inary experimental results In Formal App
142. that it has not yet considered enough states to find a counterex ample But in this situation AF q is true so will continue until the full state space has been explored and a fixed point is reached Prior to reaching the fixed point the distributed version of BMC will reach the depth at which the seed states should be generated and seeded BMC will begin Attempting to find a counterexample with EG y will now be true at every seed state because transition relation is serial resulting in an incorrect result Our algorithm will assume that the counterexample would also be valid from the initial state and return false This situation can be avoided by modifying the initial bounded check as performed by the master A final check prior to generating the seed states can be performed to check the satisfaction of AF y and if it is satisfied on the current truncated model returns true to the user and does not continue with seeded BMC If we are unable to satisfy this extra check we generate seeds such that they are the final state in a path through the model along which y is never satisfied If from such seed we are able to find a path witnessing EG y representing a k loop then a path starting from the original initial state which passes through this state and includes the loop is an infinite path upon which y is never satisfied This path is then a counterexample to the original formula that exists in the full model 4 4 A Scalable Mod
143. the current formula is true BDD result af string name Object id switch op JF F oae ae ae e e ae ae e ae ae ae ae a ae ae ae ae ae ae ae ae ae ae ae ae ae ae ae ae e ae a ae ae ae ae ae ae ae ae ae ae ae e ae ae e e ae e e e e a e e e e e e e e e e SNIP case 50 KB id is the identity of an agent id Cmodal_formula obj 0 gt get_operand Q Name is the name of agent name Catomic_proposition id gt get_proposition af is the set of reachable states in which the formula holds af CCmodal_formula obj 1 gt check_formula result is the reachable states which are indistinguishable for agent name result get_nK_states amp af name break return result 47 4 3 Distributed Verification of ACTLK This section presents an extension to our algorithm in Section 4 1 in which we demonstrate how the technique can be distributed in an attempt to utilise the available resources in a disjoint memory architecture Our work builds on the ideas of Iyer et al in 25 but rather that just hunting for bugs we can also show correctness of the system under verification We display a technique of using a Java based wrapper for MCMAS that enables the model checker to work in a networked fashion using multiple hosts in a grid to both reduce the time taken and the memory used for verification 4 3 1 The Key Idea of Grid Based BDD BMC Our approach uses a method of state spa
144. the efficient manipulation of BDDs The default and maximum size of CUDD s cache can be chosen by the user too small a cache will cause useful BDDs to be overwritten It is the cache that is scanned by the garbage collector to regain memory Garbage Collection CUDD uses a stop world garbage collector that is it stops the entire execution of the program whilst a garbage collection takes place CUDD keeps a reference count for each node produced by it recording both internal references nodes that are internal to CUDD or nodes that reference other nodes as well as external references such as those from the external program It should be obvious that garbage collection is an asynchronous process and only initiates once the cache reaches a pre defined threshold at which stage CUDD tries to release some memory Dynamic Reordering As covered in Section 2 3 4 the size of a BDD is greatly affected by the variable order ing CUDD supports a number of dynamic reordering algorithms that attempt to reduce the size of a BDD Reordering within CUDD can either be invoked directly via a call to Cudd_ReduceHeap or it can be triggered asynchronously when the number of nodes in the unique table exceeds a threshold The reordering process is iterated until no further improvement is possible CUDD contains numerous reordering algorithms an example of an algorithm is CUDD_REORDER_SIFT It is based upon Rudell s sifting algorithm 55 an
145. the local states for each agent Action The actions that an agent can perform A Protocol The individual protocol for each agent P Ev The evolution function t InitStates The set of initial states Z Formulae The formulae to be evaluated on the whole MAS Evaluation This allows the user to declare atomic propositions based on the local states of each agent Groups Allows for the grouping of individual agents into groups T ISPL files allow for the definition of red states for an agent These are states that violate some property of the MAS These states are defined over the local variables of an agent as well as observable global variables All other states in the set of local states are labelled as green states if the set of red states is empty all the local states are marked as green states Although the core of MCMAS is written using C the parsing of the ISPL files is done using Flex 70 and GNU s Bison 71 The grammar for these files is specified in the parser directory of the source tree nssis 11 is a description file for the lexer while nssis yy is the file for the parser One of the options supported by MCMAS is to print bdd stats These are statistics about the BDD and corresponding memory usage which have been consumed in model checking the provided MAS MCMAS is able to generate Graphviz Dot files that represent counterexamples
146. these states can be seen in figure 4 1 showing a simplified project_local_state method Figure 4 1 The simplified project_local_state method BDD basic_agent project_local_state BDD state BDDvector v BDD tmp bddmgr gt bddOne For all of the state variables before the agent for int j 0 j lt get_var_index_start j J and them on tmp tmp v j and after the agent for int j get_var_index_end 1 j lt v gt count j and them on tmp tmp v j return state gt ExistAbstract tmp The actual implementation does not differ much but it also has to quantify over the set of global observable variables and as these have not been discussed previously they have been omitted for clarity 45 This method is in the basic_agent class which is MCMAS s lowest encapsulation of agent The two methods get_var_index_start and get_var_index_end return the first and last index respectively into the vector of states v for that agent A temporary BDD temp is constructed from the conjunction of all the other state variables for all the other agents in the system Finally the BDD representing a quantification of these states is constructed and returned The BDD returned from project_local_state is in essence a BDD representing only the local states for the agent with all of the other states in v being set to don t cares Figure 4 2 The
147. tion between two sets of state variables from the current state to the next state One way of doing this is to assign each s S a unique Boolean vector v1 Un Vi lt n v 0 1 n should be chosen such that 2 lt S lt 2 where S represents the total number of states in the model The Boolean vector expressing a state in the system can be based upon the propositional formulae that hold at that state e g for s S the BDD state vector can be based upon the atoms in s If there are not enough Boolean variables to give each state a unique Boolean vector then it should be padded with additional variables such that the value of n is large enough It is easy enough to see how Z should be represented given that Z C S The transition relation R C S x S can be represented as two Boolean vectors the first being the Boolean vector representing the originating state and the second being the Boolean vector representing the target state L is the function mapping of s S onto propositional atoms in AP It is more convenient to consider it as the converse mapping atoms to subsets of S that satisfy that atom This set of states Lp s S p L s 16 It is easy to see how this set can be represented in the same way as Z or any other s S for that matter 2 3 4 BDDs and Variable Orderings The number of nodes and edges and as such memory that a ROBBD requires is directly linked to the variable ordering th
148. to the tunnel state can be seen as being a guarded action i e the action can only be performed when the condition is met One limitation of the work in 1 was that the authors did not discuss the properties that should be checked upon the model The functionalities that the controller should exhibit are briefly discussed in 23 The con troller should Ensure that two trains are never in the tunnel at the same time and Ensure a smooth running of the system e g the trains can always eventually move through the tunnel Sirjani et al 57 further investigate the Train Gate Controller problem with respect to modelling and verifying the system using Rebeca 78 an actor based language with a formal foundation Their paper This property is attempting to express that starvation does not occur within the model 30 provides some more concrete properties in LTL that they use to verify their Train Gate Controller based Rebeca model Mutual exclusion G Traint INTunnez Tratn2 INTunneEL Only one train should be in the tunnel at one time No deadlock GF Trarnt InTunnez V Tratn2 INTuNNEL Both trains should eventually pass through the tunnel No starvation G F Train1 INTunnez A F Train2 InTunnez Both trains finally pass through the tunnel there is always progress It should be noted that the final property is attempting to see if the controller acts in a fair way and will eventually
149. tographers then announce if the two coins that they can see theirs and the one to their left is the same or different If one of the cryptographers has paid of the meal then he or she will announce the opposite to the difference of the coins that they can see If an even number of same the NSA has paid This problem can be modelled as a multi agent systems problem where each of the cryptographers is an agent and the environment encapsulates the values of the coins The environment non deterministically chooses if a cryptographer or the NSA has paid A cryptographer agent has four local variables one for each coin one stating if the coins are the same or different and one saying if that agent has paid or not The protocol of each agent determines if they should lie or not given if they are the payer or not MCMAS can then be used to check if there is an odd number of same which means that a cryptographer has paid If an agent has not paid and there is an odd number of same utterances then the agent knows that someone paid but he does not know who ACTLK Properties Ppc1 AGC Codd and clpaid gt K DinCrypt1l c2paid or c3paid True Ppc2 AG odd and clpaid gt K DinCrypti c2paid or c3paid and K DinCryptl c2paid or K DinCrypt1 c3paid False 3As of version MCMAS 0 9 8 3 4Some of these do not have obvious translations to English 38 Software Development The work of
150. traverse the Martian landscape collecting data and measurements from rocks on the surface They were instructed to give priority to rocks which had green patches in which NASA scientists were particularly interested The rovers had limited resources the batteries could only charge from sunlight and priority was given to transmitting data back to earth They had interruptible activities but during integration a mistake was made in the code For example the following error was introduced if the sun went down during data collection the rover would blindly continue to scrape the rock and the data was lost This point is illustrated with a trace of such a system in Figure 1 1 1 Figure 1 1 A simple model of a Mars rover start Find Rock Scrape Rock Process Data Y Transmit Data cC NASA uses model checking to verify its systems Assume that they wish to verify that their rovers will always transmit the data this means that there cannot exist a trace of an execution through the model for the agent which does not transmit the data The approach taken by Regular model checking is to build up a set of every single possible reachable state in the model and then see if the property does or does not hold In comparison bounded model checking attempts to find a trace through the system in which the rover never transmits the data This is performed as an incremental check prior to attempting to find any more
151. tributed Knowledge Heuristics for Seed State Generation Intersection Based BMC Saving Reach to Disk in One Shot BMC More Models Benchmarks Better Use of CUDD eH et e ee vii 90 90 90 90 90 9I 9I 9I 92 98 IOI Vili Chapter 1 Introduction It is fair to state that in this digital era correct systems for information processing are more valuable than gold H Barendregt The quest for correctness 1996 1 1 The Problem Providing assurances about systems is not easy Our daily lives are becoming more and more dependent upon computerised systems but without any reassurance of the reliability of these devices The systems with which humans generally interact are classed as reactive systems because of their continual interaction with their envi ronment It is apparent that some of these systems may contain errors in their software but in the context of a safety critical control system for a nuclear power plant or a plane s flight control system it should be obvious that any kind of bug is unacceptable Systems verification looks at determining if a given system meets the required specification Currently most verification is a manual effort by humans which is just as error prone as the design of the system itself The current approaches to verification are based around exhaustive testing and simulation but as human
152. ty check when the heuristic is satisfied Examples of possible heuristics for selecting when to check for satisfaction include Different size increments our original implementation did a check at every bound alternatively it could be performed after a certain number of iterations e g at every 10 depth ie k 10 0 One shot see Section 4 1 2 Number of states the satisfaction check could be guarded on the number of reachable or next states exceeding a certain threshold Memory used similar to above except the guard is on the memory used to hold the reachable state Time consumed rather than checking on a depth bound the check could be performed after a variable unit of time When we refer to non bounded model checking we refer to MCMAS s default behaviour of building up the state space until a fixed point is reached Only once a fixed point is reached is a single satisfiability check performed This is not the same as unbounded model checking 29 42 Algorithm 14 Heuristic BDD BMC w ACTLK Formuta TZ INITIAL STATE Trans TRANSITION RELATION Heuristic STRING X BOOLEAN x p aw y ECLTK FormuLa 2 Reach Z Reach BDD 3 while True do 4 if Heuristic met then 5 if yl Reach then 6 return HEURISTIC MET X FALSE 7 end if 8 endif 9 Reach Reach V Reach A Trans to if Reach Unchanged then II break 12 endif 13 end while 14 return Fixen point X
153. typedef std vector lt modal_formula_p_pair gt modal_formula_p_pair_vector Figure A 2 New global variables to store formulae to prove Pairs of formulae we need to check modal_formula_p_pair_vector bmc_formulae Pairs of formulae which we ve found counterexamples to modal_formula_p_pair_vector bmc_false_formulae Initialize them bmc_formulae new vector lt modal_formula_p_pair gt bmc_false_formulae new vector lt modal_formula_p_pair gt IOI Figure A 3 The calculation of the ECLTK formulae from the ACTLK Loop over all the given formulae for unsigned int i 0 i lt is_formulae gt size i Pick up the ACTL formula modal_formula actl amp is_formulae i Push through any existing negations modal_formula actl_pushed actl gt push_negations 0Q Create the negation of the formula modal_formula actl_pushed_negated new modal_formula 3 actl_pushed Push those negations through We now have an ECTL formula modal_formula ectl actl_pushed_negated gt push_negations 9Q Double check that we ve got an ACTL and ECTL if Cactl gt is_ACTLK_BMC amp amp ectl gt is_ECTLK_BMC bmc_formulae gt push_back modal_formula_p_pair actl ectl 102 Figure A 4 A function to check all the ECTLK formulae void check_formulae_BMC void _init atom only holds at the the initial states string str _init is_evaluation str is_istates
154. ugh the entire degree despite their abuse about my love of formal methods As well as somehow at various stages of the degree finding it in themselves to manage to live with me I have no idea how Rob managed three years of it And saving the most important until last my parents without whose unconditional love support and proof reading this report would not have been possible iii Contents I1 Introduction LI 1 2 1 3 The Problem I I 1 Ce a ee ee ed An Illustrative Scenario Motivation s es assess Contributions sess 2 Background 2 1 2 3 2 4 2 5 3 Preliminaries 3 1 3 2 343 3 4 Temporal Logics 4 445 4 2 1 1 2 1 2 Linear Temporal Logic Computational Tree Logic Multi Agent Systems 2 2 1 24242 2 2 3 Agents soo trawa Interpreted Systems A Logic of Knowledge Model Checking Explicit Model Checking 2 961 2 3 2 243 3 2 3 4 24365 2 3 6 2 3 7 2 3 8 2 3 9 2 4 1 Counterexamples and Witnesses Symbolic Model Checking BDDs and Variable Orderings Alternatives to BDD Based Model Checking Model Checking Multi Agent Systems BMC for Multi Agent Systems Current Model Checking Technology BDD Based BMC Distributed Model Checking Grid Based BMC with Seed States Verifying Correctness in Real Life
155. ula as follows Depth o Depth 1 X lt Init X lt Inrr X Init s1 X lt Inrt s1 X lt Inrt s1 Z lt Init Z Z In1r s1 Y Y Y lt mit EG o 0 EG y 0 Depth 2 Iteration 0 Iteration 1 Iteration 2 Iteration 3 X lt In1T 51 52 X lt Inrt 51 52 X lt Inr7 51 52 X INnrT7 51 52 Z Inrv 1 52 Z lt In17 s1 Y lt rn1T s1 Y imir EG y 2 0 62 Depth 3 Iteration 0 Iteration 1 Xe Init 1 52 s4 Z In ir S1 52 s4 X lt In17 1 52 S4 Ze In1 1 52 3 sa Y lt IniT 51 52 53 54 Y INIT 51 52 53 54 EG y 3 IN1T 1 2 53 54 We can see that the calculation of Sarge only returns a result once the result is definitely true in the model we do not get any kind of false positive 5 1 3 SATE We can repeat the same for the calculation of a formula of the form EF the satisfiability for an EF is the least fixed point for EX Figure 5 4 Checking AG y Depth o X lt Z lt Init Z Y EF y o 0 Depth 2 Iteration 0 X x2 Z INIT 1 2 53 Y In17 1 52 53 EF y 2 In1t Si 2 53 Figure 5 5 The labelling function and existential pre image function for Figure 5 1 3 L y 81 83 INIT Lp s2 prej Inir pres si Inrt s3 pres s2 si prea s3 51 82 Depth 1
156. ult behaviour The authors felt that the most plausible explanation for the under performance of BDD based BMC was as a consequence of CUDD s automatic variable reordering If CUDD performs asynchronous reorderings more frequently during state space generation this could cause a sub optimal variable reordering to be selected Such an ordering could be preferential for the current reach set but might be an adverse ordering for the reach set generated in the next state space generation iteration CUDD only allows a certain time per attempt to find an optimal reordering and if one is not found does not change the ordering Sift ing the variables to such a reordering could provide possible preferential orderings for either the regular approach or the bounded approach This is heavily dependent upon the possible ordering generated that is it is not possible to say if a reordering should or should not be applied for a given method To provide a fair benchmark between MCMAS s regular approach and the approach set forward in this document we edited a version of CUDD to permanently turn off both variable reorderings and garbage collec tion The internal CUDD function cuddGarbageCollect in cuddTable c and the method Cudd_ReduceHeap in cuddReorder c available in the API were changed such that they return immediately on function entry It should be noted that as stated above BMC utilises temporary variables and without garbage collecti
157. used for this evaluation was a dual core PC with 4GB of memory and an Intel Core 2 Duo clocked at 3 00GHz with a 4096 KiB cache The machine was running 32 bit Ubuntu Linux 8 04 2 a vanilla 2 6 24 19 generic kernel and glibc 2 7 All experiments were performed four times with the results presented here being the average across all four runs Realistically the only metric that required averaging was time given that MCMAS is a deterministic process and will yield the same results each time for all other metrics The initial evaluation of our algorithm seemed to suggest that it massively under performed that of regular model checking Even though the implementation would in some cases only explore 25 of the state space compared to full forward verification it still required more memory These first tests were performed using MCMAS linked against a vanilla version release 2 4 1 of the CUDD library i e using garbage collection asynchronous sift reorderings and a default cache We initially looked at various sized models containing Type 2 trains whilst attempting to falsify the Yrecs5 property The results of these initial benchmarks can be seen in Table 5 1 T represents the number of trains in the model M is the maximum value of the service counter for those trains and B denotes the service counter threshold at which the trains exhibit a fault Decrease shows the comparative resource utilisation between BDD based BMC and MCMAS
158. uter Science modelling and reasoning about systems second edition Cambridge University Press 2004 ISBN 052154310X Subramanian Iyer Jawahar Jain Debashis Sahoo and E Allen Emerson Under approximation heuristics for grid based bounded model checking In Electronic Notes in Theoretical Computer Science volume 135 2006 2 pp 31 46 ISSN 1571 0661 doi DOI 10 1016 j entcs 2005 10 017 Proceedings of the 4th International Workshop on Parallel and Distributed Methods in Verification PDMC 2005 URL http www sciencedirect com science article B75H1 4377I57 4 2 084089258526b 0b960e083f 42c4a74 Subramanian K Iyer Jawahar Jain Mukul R Prasad Debashis Sahoo and Thomas Sidle Error detec tion using BMC in a parallel environment URL http www stanford edu sahoo Research papers subbu deep bmc pdf Subramanian K Iyer Jawahar Jain Mukul R Prasad Debashis Sahoo and Thomas Sidle Error detection using BMC in a parallel environment In Correct Hardware Design and Verification Methods Lecture Notes in Computer Science Springer Berlin Heidelberg ISBN 978 3 540 29105 3 ISSN 0302 9743 Print 1611 3349 Online 2005 pp 354 358 doi 10 1007 11560548_30 URL http www springerlink com content cl2jyu4mfg2691r4 Rune M Jensen A Comparison Study between the CUDD and BuDDy OBDD Package Applied to AI Planning problems September 2002 M Kacprzak A Lomuscio T asica W Penczek and M Szreter Verifying Multi agent Sys
159. z et al volume 2067 of Lecture Notes in Computer Science pp 3 38 Springer Verlag Berlin 2001 Charles Pecheur and Franco Raimondi Symbolic model checking of logics with actions In 2007 pp 113 128 doizhttp dx doi org 10 1007 978 3 540 74128 2_8 W Penczek and A Lomuscio Bounded model checking for interpreted systems 2002 URL http www doc ic ac uk alessio papers Penczek Lomuscio TR ps W Penczek and A Lomuscio Verifying epistemic properties of multi agent systems via bounded model checking 2003 URLhttp citeseer ist psu edu article penczek03verifying html Wojciech Penczek Bozena Wozna and Andrzej Zbrzezny Bounded model checking for the universal fragment of CTL In Fundam Inf volume 51 2002 1 pp 135 156 ISSN 0169 2968 Franco Raimondi Model Checking Multi Agent Systems Ph D thesis 2006 http www cs ucl ac uk staff f raimondi pubs thesis pdf 96 50 51 53 54 55 59 60 61 Ku 62 Franco Raimondi Notes from the course GSo3 4203 Verification and validation 2007 2008 URL http www cs ucl ac uk staff F Raimondi teaching Franco Raimondi and Alessio Lomuscio A tool for specification and verification of epistemic properties in interpreted systems In Electronic Notes in Theoretical Computer Science volume 85 2004 2 pp 176 191 ISSN 1571 0661 doi DOI 10 1016 S1571 0661 05 82609 X LCMAS 2003 Logic and Commu nication in Multi Agent Systems

Download Pdf Manuals

Related Search

Related Contents

INSTALLATION for PIXWRITER v3.2  Le projet de Service à l`AST 62-59 : mode d`emploi  Sangean Digital Alarm Clock Extension Unit    取扱説明書 NS-HD56MPX  pDoc Pro Client User Manual  « Mettre l`élève et le management au centre du système »  

Copyright © All rights reserved. Failed to retrieve file