A Model Checking Approach to Protocol Conversion
Contents
1. and M 2 Node s state labels set of formulas type either OR or AX counters s state s state labels set of formulas type either AND or OR counters F set of formulas counters Figure 3 The structure of nodes and leaves 2 1 2 Fairness In order to ensure that converters always allow meaningful communication be tween protocols it may be desirable that additional fairness conditions are sat isfied which can be again defined using ACTL formulas For converter synthesis the goal is to ignore as well as disable all unfair behaviours of the protocols For the producer consumer example we use the following fairness conditions e AGAF D_Outg F1 The producer can always eventually write data e AG D_Outg gt AXA Req_Out U Data_Inig F2 Once some data is writ ten no further requests are allowed before a read operation is performed e AGAF R_Out F3 The producer can always eventually emit requests 2 2 Tableau Construction Algorithm The proposed technique is based on model checking and involves on the fly tableau construction similar to 2 Given the inputs P and Pz describing participating protocols some invariants over data counters and the set WV of desired properties including fairness properties the tableau construction algo rithm proceeds as follows We illustrate the working of the tableau construction algorithm using the producer consumer example given in Fig 2 The first step2. consumer allowed multiple reads with each handshake This allowed handling arbitrary read write pairs The final three results are well known NuSMV examples modified to create mismatches The mutex example was modified such that a violation of the mutual exclusion property occurred The missionaries and cannibals problem an abstraction of data communication between two protocols was also handled successfully It involved constraining data communication between protocols such that size of the communication medium boat was not exceeded and at the same time further restrictions on data variables number of cannibals never exceeds the number of missionaries were also handled The 4 bit alternating bit protocol example was modified to create a control mismatch between the sender and the 14 receiver which introduced many faulty paths in the combined system Using the tableau construction algorithm a converter that effectively disabled such faulty communication paths was realized Note that size entry in the second column for the final two results is the combined size of the system size of P P2 4 Conclusions Protocol conversion to resolve protocol mismatches is an active research area and a number of solutions have been proposed Some approaches require signifi cant user effort while some only partly address the protocol conversion problem Most formal approaches work on protocols that have unidirectional communi cation and use finit
3. i lt n the values of interest lie in K 2 partitions where K max min 1 K partitions are singleton 11 Figure 6 The resulting system C P P2 sets containing one element each from the range max to mini one partition containing all data points in lt min and another containing all data points gt mazi In other words if the valuation of the counter goes beyond the limits min or mazi it is not required to record the exact valuation This stems from the fact that if c takes values outside the allowed range the invariant min lt ci lt mazi is violated and leads to a failed path in the tableau It follows from the above observation that for each state s in P P2 there may be several exactly K 2 valuations for each counter variable c resulting in multiple states corresponding to the same state in P P2 each with a different valuation of counters Therefore the total number of states S that can be traversed by the algorithm in the worst case is S S1 x S2 x K 2 x K2 2 x x Kn 2 We use to denote a valuation of all counters and use S to denote the expanded state space Having defined the maximum size of the state space to be traversed we first note that for any state s in S if refers to a valuation of the counters where any one counter is outside its allowed range the tableau leaf automatically results in a failed path function create_leaf solve_tleaf is onl
4. is consistent i e c is constructed such that s c satisfies all obligations Yaz Therefore if we can generate an environment for s corresponding to rule unr then s w where w is the conjunction of the elements of the set AXy p Vaz The other direction can be proved likewise 3 Results A protocol conversion tool employing the tableau construction approach has been implemented by extending the NuSMV model checker 4 The results table Table 1 contains four columns The first two columns contain the description and size number of states of the participating protocols The ACTL properties used are shown in the third column with the size of the converter shown in column 4 The first five problems are well known protocol conversion problems with control mismatches 10 7 The next problem is the multi write producer and single read consumer protocol pair used as the motivating example in this paper The size of the output of the producer was kept constant at 8 bits and the input size of the consumer were varied in multiples of 8 bits and the size of the converter is noted in the fourth column Note that when the input size was not a direct multiple of the output size 9 bits and 2 bits respectively no converter could be generated This was due to the fact that the consumer 13 Pi Sp P Spl Slave 3 E Event sequencing one grant per request requests precede grants ABP sender NP rec
5. is the computation of the unrestricted combined behaviour P P2 of P and Pz also called the parallel composition similar to the syn chronous parallel in Argos 8 defined as follows Definition 2 Parallel Composition Given two Kripke structures P AP 1 so 41 Ri Li and Py AP2 S2 S03 42 R2 Le their parallel composition denoted by P P2 is 0 0 type AX c 0 labels AX S1 AX S2 AX S3 AX F1 AX F2 AX F3 AXA tt U R_Out AXA tt U D_Out8 req req 1 1 type AX c 0 labels AX S3 AX F1 AX F2 AX F3 Defi F2F3 At U AXA tt U D_Out8 R_Out AXA tt U D_Out8 ack ck 3 2 type AX c 1 os cs labels AX S3 AX F1 AX F2 F S3 F1 F2 F3 A tt U AX F3 AXA tt U R_Out R_Out AXA tt U D_Out8 AXA Req_Out U Data_In16 A Req_Out U Data_In16 3 3 type AX c 0 labels AX S3 AX F1 AX F2 AX F3 AXA tt U R_Out a b c Figure 4 Tableau construction procedure a states of P P2 b tableau nodes c synthesized converter APij 2 Sill2 S01 2 Xiz Rajj2 Laj where APijj2 AP UAP Sijj2 S1 x S2 S012 s01 S02 and Xij C My Xx Ue Ryo Cc Silj2 x Zl x Sijl such that s1 ajA 23 8h gt 81 82 e Finally L4 2 s1 2 L1 s1 U Lo s2 Some states of the parallel composition of the producer consumer example are shown in Fig 4 a Algorithm 1 check so Y 1 Initialize counters create a set A of leaves 2 call create_leaf s count
6. 8 March 1986 7 S Lam Protocol conversion IEEE Transactions on Software Engineering 14 3 353 362 1988 15 F Maraninchi and Y Remond Argos an automaton based synchronous language Computer Languages 27 61 92 2001 K Okumura A formal protocol conversion method In ACM SIGCOMM 86 Symposium pages 30 37 1986 R Passerone L de Alfaro T A Henzinger and A L Sangiovanni Vincentelli Convertibility verification and converter synthesis Two faces of the same coin In International Conference on Computer Aided Design ICCAD 2002 J C Shu and Ming T Liu A synchronization model for protocol con version Proceedings of the Eighth Annual Joint Conference of the IEEE Computer and Communications Societies Technology Emerging or Con verging INFOCOM 89 pages 276 284 1989 R Sinha P Roop and S Basu Automatic synthesis of converters for proto col matching using model checking Technical Report 00000482 Iowa State University 2006 16
7. A Model Checking Approach to Protocol Conversion Technical Report No 0000482 Roopak Sinha Partha Roop Department of Electrical and Computer Engineering University of Auckland and Samik Basu Department of Computer Science Iowa State University Iowa STATE UNIVERSITY Department of Computer Science November 2006 2006 All rights reserved Abstract Protocol conversion for mismatched protocols has been addressed in a number of formal and informal settings However existing solutions address this problem only partially This paper develops the first on the fly local approach to protocol conversion based on temporal logic model checking The tableau based approach verifies the existence of a converter and if a converter exists it is automatically synthesized Our approach handles control and data mismatches under a single unifying framework A NuSMV based implementation has been developed and we provide results for some non trivial protocol mismatch examples 1 Introduction A system on a chip SoC is built by reusing components connected using a central bus such as AMBA 3 A major problem with this reuse is the inher ent mismatch between protocols of components an active area of research for about two decades 7 Mismatches occur because components are developed independently without any intention of eventual integration and can result from control signal mismatches 6 inconsistent naming conventions 11 differ ent c
8. after removing AX from the formulas to the set F of each of the newly created leaves Node 1 becomes an AX_NODE as only those successors of the state t state can be enabled that satisfy these future commitments Another case when a node may be expanded is when an OR formula is encountered and the success of the parent node depends on the success of any of its children When a leaf is expanded as in the case of the root leaf for the producer consumer example the keyword EXPANDED is a2 e EO prop riety peL v CK emp s e H piny u Y s e e Hgrp2 U V s c H vive U Y V s c K piVy2 U 4 1 s e e E Hy U Y 2 8 e E Ky U Y s e c H Ale U Y U YY unrau s e Je F EVel UY U T s c acy UY unTag s e ce E I PAAKAGy U T Wax yk AXYk Y unr gem woes u Tey TS ol s 7 S s0 ene 6 SEA D o 0 Figure 5 Tableau Rules for converter generation returned by solve_leaf For the producer consumer example root node 1 Fig 4 b has 4 children check iteratively calls solve_leaf on all newly created leaves When solve_leaf operates on leaf 1 a child of node 1 it returns a FAILURE This happens because the violation of the property S1 S1 is broken down to the current state commitment R_Out V AR_InA AXA R_In U R_Out which is not satisfied by the state so 51 the state corresponding to leaf 1 The check procedure then passes the returned
9. ata width mismatches are addressed The main contributions of this paper are e We propose the first model checking based solution to protocol match ing guaranteed to produce a converter if one exists no further proof of correctness is required unlike some other approaches 3 e We present a novel tableau based algorithm to address data and control mismatches in a unifying manner unlike earlier solutions that deal with them separately or in an ad hoc manner e We present an on the fly algorithm for converter synthesis one where pro tocol states are explored only when needed The algorithm is polynomial in the size of the protocols and specifications The rest of this paper is organized as follows Section 2 presents the au tomatic converter synthesis approach based on tableau generation Section 3 provides some implementation results with concluding remarks in section 4 2 Methodology The proposed protocol conversion algorithm takes as input the KS descriptions of two protocols and a set of ACTL properties It then employs a local on the fly tableau construction algorithm to verify the existence of a converter more Producer Consumer Figure 2 Producer consumer protocol pair 2 1 Input description The conversion algorithm takes as input two protocols represented as Kripke structures Definition 1 A Kripke structure KS is a finite state machine represented as a sextuple AP S so R L where AP is a se
10. but there are no outputs corresponding to the control inputs d_rdy and more control incompatibility Furthermore there is also a data incompatibility as P writes 8 bit data whereas P gt can only read 16 bit data In addition to addressing the above issues the intended communication be tween the producer consumer protocols can be further described using addi tional ACTL formulas ACTL is a fragment of the branching time temporal logic CTL and only allows universal path quantifiers Semantics of an ACTL formula y denoted by y as are given in terms of set of states in a KS M which satisfies the formula A state s S is said to satisfy a ACTL formula y denoted by s H y if s p m We also say that M H y to indicate that the initial state so of the model M satisfies y We restrict ourselves to formulas where negations are applied to propositions only For the producer consumer example in Fig 2 the following properties are needed 1 A Req In U R_Out S1 A request cannot be read before one is made 2 A D_Outs U Req In S2 No data is written data before a request has been received 3 AG Error 3 The communication never enters a state labelled by Error 2 1 1 Describing data width mismatches The producer consumer protocol pair has a data width mismatch as P writes 8 bit numbers to the data channel whereas P gt reads 16 bit numbers We for mally describe the desired data communication behaviour as follow
11. e state machines to describe specifications In this paper we propose a formal approach to protocol conversion which alleviates the above problems Specifications are described in temporal logic and bidirectional com munication is allowed A tableau based approach using the model checking framework is used to generate converters in polynomial time We use invari ants to handle data width issues Fairness properties are used to generate fair converters We prove that the approach is sound and complete and provide implementation results References 1 Rajeev Alur and David L Dill A theory of timed automata Theoretical Computer Science 126 2 183 235 1994 2 Girish Bhat Rance Cleaveland and Orna Grumberg Efficient on the fly model checking for CTL In Proceedings of the Tenth Annual Symposium on Logic in Computer Science pages 388 397 June 1995 3 Vijay D Silva S Ramesh and Arcot Sowmya Synchronous protocol au tomata A framework for modelling and verification of soc communication architectures In DATE pages 390 395 2004 4 R Cavada et al NuSMV 2 1 User Manual June 2003 5 Saurav Gorai et al Session 42 simulation assisted formal verifica tion Directed simulation assisted formal verification of serial protocol and bridge In Proceedings of the 43rd annual conference on Design automation DAC 06 pages 731 736 2006 6 P Green Protocol conversion IEEE Transactions on Communications 34 3 257 26
12. eiver 4 7 Control Signal matching Master 3 Ack Nack Sender 3 Poll End Receiver 2 Data communication resolution one data in per data out Handshake 2 Multi write Producer protocol 3 8 bit Write 8 bit Write 8 bit Write 8 bit Write 2 bit Write Multi write Producer protocol 3 2 bit Write 2 bit Write 3 bit Write 3 bit Write 9 bit Write 7 bit Write 11 bit Write Serial 2 10 Single read Consumer protocol 4 8 bit Read 16 bit Read 24 bit Read 32 bit Read 9 bit Read Multi read Consumer protocol 4 9 bit Read 11 bit Read 10 bit Read 11 bit Read 2 bit Read 64 bit Read 256 bit Read 6 4 I7 j j ABP receiver 8 NP sender 3 7 Control signal matching 2 Control signal matching 3 and event sequencing Alternating A and B labels AG Error A D Out U Req_In A Req In U R_Out Error is never encountered no data written before requests and no requests read before any requests are made Failed AG Error A D Out U Req_In A Req In U R_Out Error is never encountered no data written before requests and no requests read before any requests are made Mutex Process 1 8 Mutex Process 2 3 4 MCP cannibals GOM 4 bit ABP Sender Modified Receiver 166432 4 Liveness checking based on 14312 control signal matching Table 1 Implementation Results allowed only a single read after each handshake with the producer The next set of results were obtained when the
13. er_vals Y Nil 3 while A is non empty do 4 remove one leaf t from A 5 result solve_leaf t 6 if result SUCCESS or FAILURE then 7 result notify_parent t result 8 if globalresult SUCCESS then 9 return SUCCESS 10 end if 11 end if 12 end while 13 return FAILURE The proposed algorithm constructs a tableau which has nodes and leaves Fig 3 Nodes are parents that have one or more children Each node cor responds to a state in P P2 and a specific valuation of all data counters and is labelled with a set of formulas labels Leaves on the other hand do not have children and have no labels A leaf contains a set of formulas F that its corresponding state must satisfy The tableau can be extended only when a leaf is expanded into a node Given the states of P P2 for the producer consumer example Fig 4 a the algorithm proceeds as follows The initial state so so of P P2 and the set S1 2 3 F1 F2 F3 are passed to the top level tableau construc tion procedure check which initializes data counters and creates a set A which contains all leaves created during tableau construction check then contains the initial top level tableau leaf corresponding to so so and the set of properties Y This is the root of the tableau which contains the initial state of P P and the original set of properties Y The method create_leaf is used to create new leaves If the creation of a leaf results in the vio
14. ialize Y Ax 3 while Y is non empty do remove one formula f from Y if f TRUE then continue else if f FALSE then return FAILURE else if f p AP then return FAILURE if not f L s else if f p p AP then return FAILURE if f L s else if f AGP then insert P A AXAGP in Y else if f A P U Q then insert Q V P A AXA P U Q in Y else if f PAQ then insert P Q in Y else if f PV Q then t type OR_NODE create_leaf s UU P U Vax t create_leaf s U Q U Vax t return EXPANDED else if f AXP then if P A Q U R and P occurs earlier in tableau at s then return FAILURE else add f to the set Vax end if if P AGQ and no ancestor of t contains P at state s then add f to the set V_AX end if end if end while if Vax is non empty then Wy p AXp E Vax t type AX_NODE t labels label for each successor s of s do create_trace s V i y t end for return EXPANDED end if return SUCCESS SUCCESS This results in the tableau being folded back with a reference to node 1 A similar leaf may return FAILURE if the future commitments are of the type AU The return values SUCCESS or FAILURE returned by solveteaf for a leaf t is passed to the notify_parent method which recursively passes the result to its parent ancestors if needed A node returns SUCCESS if at least on of its children returns SUCCESS An OR NODE does not disable any transitions as only one child is needed to satisfy co
15. ities between P and P gt as follows The input output events in P P2 are output input events for the converter The converter can read an output generated by either protocol and may pass it to the other Using this underlying control the controller can perform inhibition buffering and synthesis The converter inhibits an event when the transition resulting from an event is disabled in C itself In this case the converter disallows or absorbs the input instead of passing it on The converter may buffer an event where it holds an input for a while before passing it on Finally in case a control input expected by one protocol is not provided by the other the converter synthesizes it as an output itself in order to avoid blocking states The converter C Fig 7 for the producer consumer example resolves the control incompatibility between the two protocols by synthesizing the signals more and d_rdy artificially when required The data incompatibility is resolved as all paths leading to states where a mismatch happens the counter variable in the tableau exceeds invariant range are disabled using inhibition Furthermore buffering and inhibition are used such that only those paths that satisfy the given ACT L specifications and fairness properties are also satisfied Formally the control of a converter C over given protocols P and P called the lock step composition C P P2 is defined as follows Definition 3 Lock step Converter Compos
16. ition Given the KS Py APijj2 Sill2 SOijj2 gt yyy 25 Railz Lijl2 and a converter C APe Se SCO Xe Re Lc the lock step composition C P P2 APij2 Se a 2 s Ziz Rey al2 Le cajj2 such that Seala C Se x Sy 2 and Scj jall2 soc gji Re 1 2 is defined as 80 1 2 2 01 02 ofo 01 02 se gt se A sija gt gt sij A Doi 01 A D o3 02 gt seyal gt sealg Finally Le 1 2 sP se Lijlsij The transition relation of the protocols composed with a converter ensures that protocols move only when the converter allows that move As such the lock step composition is different from unrestricted composition Defini tion 2 For the producer consumer example the corresponding controlled sys tem C P P2 is given in 6 The following theorem follows from the above Theorem 3 Sound and Complete Two protocols P and P gt with n defined data counters c1 C2 Cn with the constraints min lt ci lt mazi can be made compatible wrt to a set Y of ACTL formulas by using an automatically generated converter C iff check returns SUCCESS Proof The first step in proving the above theorem is to realize the size of the state space to be traversed during tableau construction Given P with total number of states S1 and P with total number of states S2 the input to the check method P P2 would contain a maximum of S1 x S2 states Observation 1 For each counter c 0 lt
17. lation of any invariants the leaf is deemed invalid After creating the root leaf check calls the procedure solve_tleaf for this newly created leaf Algorithm 2 createlea f s prev ounter als V parent 1 Update counters based on labels of s 2 return if counters violate invariants if there exists a leaf t with t state s and t counter_status current counter status then w 4 t formulas t formulas Y 5 else 6 create a new leaf t with t state s 7 t formulas Y t parent parent t type LEAF 8 amp t counter_status updated counter status 9 end if The solveteaf method receives a tableau leaf t as input and proceeds to individually break down formulas contained in t F into current state and future commitments lines 4 18 This decomposition of formulas is based on a set of tableau rules Fig 5 For example for root leaf of the producer consumer example the formula 3 AG Error is broken down into the subformulas Error and AXAG Error The sub formula Error being a current state com mitment a proposition is checked against the leaf state so so The future commitment AXAG Error is stored in the set label Once all current state commitments have been checked the root leaf is expanded to become a node Node 1 in Fig 4 b and a leaf is created for each successor of the state so so All future commitments including AXAG Error are added to the set labels of the newly expanded node and
18. lock speeds and difference in data widths 3 Mismatches are corrected if possible by synthesizing extra glue logic called a converter 10 to control communication between given protocols in order to satisfy given specifications A number of techniques address the problem of protocol conversion in a wide range of formal and informal settings with varying degrees of automation projection approach 7 conversion seeds 9 and synchronization 11 Some approaches like conversion seeds 9 and protocol projections 7 require signif icant user expertise and guidance While this problem has been studied in a number of formal settings 6 7 9 11 only recently have some formal verifica tion based solutions been proposed 3 5 10 In 5 a hybrid simulation verification approach to protocol conversion in SoC designs is proposed 10 proposes an approach towards protocol conversion employing a game theoretic framework to generate a converter This solution is restricted only to protocols with half duplex communication between them with specifications represented as finite state machines D Silva et al 3 present syn chronous protocol automata to allow formal protocol specification and matching as well as converter synthesis The technique addresses the problem of limited communication medium capacity but data communication between protocols cannot be constrained any further Specifications Figure 1 Protocol conversion In con
19. mmitments whereas an AX_NODE enables transitions to only those children that satisfy the future commitments passed to them The algorithm finishes when the root leaf corresponding to so So returns SUCCESS Algorithm 4 noti fy_parent t result 1 if t is a top level trace then 2 globalresult result 3 return 4 end if 5 parent t parent 6 if parent type OR_NODE then 7 if result FAILURE then 8 call noti fy_parent parent FAILURE if no unchecked child remains 9 else 10 call noti fy_parent parent SUCCESS 11 end if 12 else if parent type AX_NODE then 13 if result FAILURE then 14 remove the link from parent to t 15 if child set of parent is empty then 16 call notify parent parent FAILURE if successor set of parent state is empty 17 else call notify parent parent SUCCESS 18 end if 19 end if 20 end if 2 3 Converter Synthesis The converter is synthesized automatically during tableau construction if it completes successfully We traverse the nodes starting from the root node that returned SUCCESS in the tableau and select the AX nodes encountered to form states in the converter The converter states synthesized for the states of P P2 for the producer consumer example shown in Fig 4 a are shown in Fig 4 c Note how each converter state corresponds to an AX node in the tableau Fig 4 b The full converter C is shown in Fig 7 10 The converter resolves incompatibil
20. s Given the data widths N and M of the outputs and inputs respectively we first compute the minimum width needed for the communication medium between the two protocols If N lt M then the minimum capacity must be N x f such that f is the smallest integer for which N x f gt M otherwise the minimum ca pacity is N This ensures that there are enough preceding outputs before any one input While the minimum bound of communication medium buffer can be computed as above the maximum bound is be any value greater than the minimum bound In our setting we assume that the maximum bound of the communication medium buffer is LCM N M Given a capacity K of the com munication medium between these bounds the maximum number of outputs possible when the medium is empty is x K N while the maximum number of inputs possible when the medium is full is y K M We use an auxiliary counter for every input output pair such that the counter is incremented by y for every output decremented by x for every input and verify that the counter always remains between 0 and z x y using the invariant 0 lt counter lt x x y In addition we can also force that maximum number of outputs are done before inputs start and vice versa expressed by the following ACTL formulas AG counter 0 A input U counter x x y AG counter x x y A output U counter 0 For the producer consumer example in Fig 2 we use the invariant 0 lt counter lt 2 as N 1
21. t of atomic propositions S is a finite set of states so S is the initial state is a finite set of input and output events R C S x x S is the transition relation and L S 24 is the state labelling function States in a protocol are labelled by unique identifiers Transitions between states each labelled with a priority trigger with respect to a clock At each clock cycle the KS checks for the presence of input output events that can trigger a transition from the current state If multiple input output triggers are present the transition using the highest priority is taken An event a represents an input whereas represents an output The relations s a s R are represented as ss Fig 2 shows the protocols of two devices a producer and a consumer rep resented as Kripke structures The producer protocol P sends sends a request before producing any data and in the next cycle awaits the input signal ack If ack is absent the protocol enters an error state s2 Else it goes on to write 8 bits on to the data channel D_outg and is capable of writing multiple 8 bit data if the signal more is present in subsequent cycles The 16 bit consumer P reads the request from the producer and then emits an acknowledgement ack It then waits for the input d_rdy to read one 16 bit data from the data channel The protocols have a number of incompatibilities Although P and P gt can share the input output channels req and ack
22. trast to the above techniques we present a technique using model checking for automatic converter synthesis Protocols in our setting are rep resented using Kripke Structures KS and specifications and their negations are expressed in the temporal logic ACTL ACTL a branching time temporal logic with universal path quantifiers is particularly relevant for protocol conversion as mismatches in protocols must be addressed for every path of their KS de scriptions Given two KSs P and P and a set W of desired ACTL properties the protocol conversion via converter synthesis problem illustrated in Fig 1 may be stated as Can a converter C be synthesized for P and P such that all for mulas in Y can be satisfied The proposed approach involves the local and on the fly construction of a tableau 2 where satisfaction of ACTL formulas in W is defined in terms of the satisfaction of their subformulas by the states of the protocols The tableau construction results in the automatic synthesis of the converter if one exists If no converter is found failures can be identified without exploring states irrel evant for failure inference Not only are temporal logic specifications succinct and more intuitive to write additional constraints such as fairness can also be specified Fairness constraints ensure that converters allow meaningful commu nication to take place between protocols We use invariants to specify bounds on data widths 1 so that d
23. value to the method noti fy parent which effectively results in the transition from so so to so 1 to be disabled in the tableau Another child leaf of node 1 corresponding to s1 s1 satisfies all its current state commitments and hence is further expanded into node 2 with 4 children Its child leaf 2 corresponding to the state s2 s2 in P P2 returns a FAILURE as it is labelled by Error violates 3 The child leaf corresponding to the state s3 2 is expanded node 3 with only 3 children even though the state s3 52 has 4 successors This is so because the child leaf 3 corresponding to the state so s3 is invalid as the data read D_Injg in this state results in the counter c taking a value 1 which is outside the allowed invariant range 0 lt c lt 2 One of the children of node 3 corresponding to the state s3 s3 is further expanded into node 4 with 2 child leaves one for each successor 53 9 and so S0 The leaf corresponding to s3 9 returns FAILURE counter out of bounds whereas so so returns SUCCESS This happens because all formulas passed to this child leaf are contained in the labels of the ancestor node 1 corresponding to the same state so so and counter valuation c 0 Due to this solve_leaf does not store any further future commitments all of the type AXAG lines 24 33 and as all current state commitments are met returns Algorithm 3 solve_leaf t 1 2 s t state Y t F Init
24. y called for leaves which are associated states in S that have valid valuations for all counters The proof then proceeds by realizing the soundness and completeness of each of the tableau rules For brevity we present here the proof sketch for unrs proofs for the other rules are straightforward Recall that s e H Y s T S where W is the set of formula ex pressions with temporal operators AX is satisfiable if the next states proof obligations are satisfied by destination states reachable via transitions enabled by the converter C The converter can enable any subset barring of transi tions The tableau rule therefore considers all possible subsets of destination states of enabled transitions 12 Figure 7 The converter C As each transition is annotated by an event we construct II the set of events of out going transitions In other words o Il gt so Co is reach able via the transition with event o We are required to identify one possible subset of II which represents the enabled transitions whose destinations con form to the obligations in the consequent see 3r C II in the consequent Let Ts 85 Co o T be the next states reachable via selected enabled transitions The consequent of the tableau rule has the following obligations All ele ments of 7 in parallel composition with the converter must satisfy the expres sions in Yaz This ensures that the converter constructed
Download Pdf Manuals
Related Search