IMITATOR II User Manual
Contents
1. high Give much debugging information total Give really too much information inclusion default false Consider an inclusion of region instead of the equality when performing the Post operation In other terms when encoun tering a new state IMITATORIT checks if the same state same location and same constraint has been encountered before and if yes does not consider this new state However when the inclusion option is activated it suffices that a previous state with the same location and a constraint greater or equal to the constraint of the new state has been encountered to stop the analysis This option corresponds to the way that e g Hy TECH works and suffices when one wants to check the non reachability of a given bad state log prefix default lt input_file gt Set the prefix for log states and graphical gif files 13 mode default inversemethod The mode for IMITATOR II reachability Parametric reachability analysis see Section 4 3 1 inversemethod Inverse method see Section 4 3 2 cover Behavioral Cartography Algorithm with full coverage see Section 4 3 3 randomXX Behavioral Cartography Algorithm with XX iterations see Section 4 3 3 no dot default false No graphical output using DOT no log default false No generation of the files describing the reachable states no random default false No random selection of the ro incompatible inequality select the first found By defaul2. SRlatch v0 The program will call the inverse method on 100 points randomly selected within Vo Since some points may be generated several times or some points may belong to previously generated tiles see Section 4 3 3 the number n of tiles generated will be such that n lt 100 The program will generate n files of the form SRlatch imi gif giving the reachability graph of tile 2 for i 1 n 15 R Q s R S Q tH Figure 5 SR latch left and environment right 5 Example SR latch We consider a SR latch described in e g 13 and depicted on Fig 5 left The possible configurations of the latch are the following ones s R 9 Q O O latch latch 0 1 0 1 i 0 1 0 11 0 o We consider an initial configuration with R S 1 and Q Q 0 As depicted in Fig 5 the signal S first goes down Then the signal R goes down after a time t We consider that the gate Nor resp Nor gt has a punctual parametric delay 6 resp 52 Moreover the parameter t corresponds to the time duration between the fall of S and the fall of R 5 1 Parametric Reachability Analysis We first perform a reachability analysis The launch command for IMITATOR II is the following one IMITATOR2 SRlatch imi mode reachability Considering this environment the trace set of this system is given in Fig 6 where the states q i 0 6 correspond to the foll
3. corresponding trace set under a graphical form The description of all the parametric reachable states is also returned Behavioral Cartography Algorithm When calling IMITATORII to apply the behavioral cartography algorithm the tool takes as an input two files one 5An interface to accept as well files given using the PHAVer syntax is currently being implemented Figure 2 IMITATOR II inputs and outputs in inverse method mode describing the network of PTAs modeling the system and the other describ ing the reference rectangle i e the bounds to consider for each parameter As depicted in Figure 3 it synthesizes a list of tiles as well as the trace set corresponding to each tile under a graphical form The description of all the parametric reachable states for each tile is also returned Figure 3 IMITATOR II inputs and outputs in behavioral cartography mode 3 2 Structure and Implementation Structure Whereas IMITATOR was a prototype written in Python calling HYTECH for the computation of the Post operation IMITATORII is a stan dalone tool written in OCaml The Post operation has been fully implemented and the inverse method algorithm entirely rewritten As depicted in Figure 4 IMITATOR II makes use of an external library for manipulating convex polyhedra Depending on the user s preference IMITATOR II can call either the NewPolka library available in the APRON library 18 or the Parma Polyhedra Library PPL 9 The
4. i e 7 m H C We define Post a xy 5 as the set of states reachable from S in exactly i steps and Post 4 y S as the set of all states reachable from S in A K i e Posta 5 Ui gt o Posta 5 Given two sets of states S and S we write SE S iffVs S Is e S s t s s Application to the Root Contention Protocol Applying the inverse method algorithm to the PTA modeling the Root Contention Protocol described in Section 2 2 and the reference valuation Ty the following constraints is gen erated by IMITATOR II in 2 3 seconds rc_slow_min gt 2 x delay rc fast_maz rc fast min gt 2 x delay By definition of the inverse problem this constraint corresponds to parame ter valuations having exactly the same behavior i e exactly the same trace set as for mo However there may be other parameter valuations having different good behaviors i e different good trace sets Finding those other parameter valuations is the purpose of the next section 2 4 The Behavioral Cartography Algorithm We recall here the behavioral cartography algorithm as defined in 5 By iterating the above inverse method M over all the integer points of a rectangle Vo of which there are a finite number one is able to decompose most of the parametric space included into Vo into behavioral tiles Formally Algorithm 2 Behavioral Cartography Algorithm BC A Vo input A PTA A a finite rectangle Vo C RA output Tiling lis
5. name gt prolog locations end prolog initialization sync_labels sync_labels initialization sync_labels 28 initialization initially lt name gt state_initialization state_initialization convex_predicate prolog synclabs sync_var_list sync_var_list sync_var_nonempty_list loe sync_var_nonempty_list lt name gt sync var nonempty_list lt name gt locations location locations locations loc lt name gt while convez_predicate wait transitions loc lt name gt while convex_predicate wait transitions transitions transition transitions transition when convex_predicate update synchronization goto lt name gt update_synchronization updates syn_label updates syn_label syn_label updates loe updates do update list update list update_nonempty_list loe update_nonempty_list update update_nonempty_list update 29 update_nonempty_list lt name gt linear_expression syn_label sync lt name gt convex_predicate linear_constraint amp convex_predicate linear_constraint linear_constraint linear_expression relop linear_expression True False linear_expression linear_term linear_expression linear_term linear_expression linear_term l
6. of reachable states and then the intersection with the bad states to terminate in practice Application to the Root Contention Protocol To find other valua tions of the parameters for which the system still behaves well we com pute a cartography of the Root Contention Protocol with the following Vo rc_slow_min 140 200 re_slow_mazx 140 200 and delay 1 50 The two other parameters remain constant as in To The cartography computed by IMITATORII is given in Figure 1 For the sake of clarity we project onto delay and rc_slow_min In each tile the pa rameter rc_slow_maz is only bound by the implicit constraint rc_slow_min lt rc_slow_maz Note that tiles 1 and 6 are infinite towards dimension rc_slow_min and all tiles are infinite towards dimension rc_slow_maz Moreover although all the integer points within Vo are covered from the algorithm note that the real valued part of Vo is not fully covered because there are some holes real valued zones without integer points in the lower right corner An example of point which not covered by the cartography is delay 50 re_slow_min 140 4 and rc_slow_maz 141 It can be shown that tiles 1 to 3 correspond to good tiles whereas the other tiles correspond to bad tiles As a consequence the solution to the good parameters problem for this example corresponds to the parameter valuations included in tiles 1 2 and 3 The corresponding constraint is the following o
7. the whole set of reachable states from a given initial state The syntax in this case is the following one IMITATOR2 lt input_file gt mode reachability options Note that there is no need to provide a 7 or Vo file in this case if one is provided it will be ignored In this case IMITATOR II outputs two files e A file lt input_file gt states containing the set of all the reachable states with their names and the associated constraint on the clocks and parame ters If one wants to generate also the constraint on the parameters only use the with parametric log option This file also contains the source for the generation of the graphical file using the DOT syntax This log file is not generated in the case where the no log option is activated e A file lt input_file gt gif which is a graphical output in the gif format generated using DOT corresponding to the trace set This graphical out put is not generated in the case where the no dot option is activated Note that the location and the name of those two files can be changed using the log prefix option 4 3 2 Inverse Method Given a PTA A and a valuation mo of the parameters the inverse method compute a constraint Kg on the parameters guaranteeing that for any 7 Ko the trace sets of A z and A ro are the same 4 The syntax in this case is the following one IMITATOR2 lt input file gt lt pi0_file gt mode inversemethod options Note that the mode inv
8. trace sets are output under a graphical form using the DOT module of the graph visualization software Graphviz IMITATOR II contains about 9000 lines of code and its development took about 6 man months Figure 4 IMITATOR II internal structure Internal Representation States are represented using a triple q v C made of the current location q in each automaton a value for each discrete variable v and a constraint C on the clocks and the parameters In order to optimize the test of equality between a new computed state and the set of states computed previously the states are stored in a hash table as follows to a given key q v of the hash table we associate a list of constraints C1 Ch corresponding to the n states g v C1 q 0 Cn Note that unlike HYTECH IMITATOR II uses exact arithmetics with unlim ited precision Contrarily to HyTECH which performs an apriori static composition of the automata thus leading to a dramatical explosion of the number of locations IMITATOR II performs an on the fly composition of the automata This on the fly composition allows to analyze bigger systems and decrease drastically the computation time compared to IMITATOR 3 3 Features IMITATOR II includes the following features e Reachability analysis given a PTA A compute the set of all the reachable states as it is done in tools such as e g HYTECH and PHAVer e Inverse method algorithm given a PTA A and a refere
9. IMITATOR II User Manual Etienne Andr June 11 2010 Abstract We present here the user manual of IMITATOR II a tool implementing the inverse method in the framework of parametric timed automata given a reference valuation of the parameters its generates a constraint such that the system behaves the same as under the reference valuation in terms of traces i e alternating seguences of locations and actions This is useful for safely relaxing some values of the reference valuation and optimizing timing bounds of the system Besides the inverse method IMITATOR I also implements the behavioral cartography algorithm al lowing to solve the following good parameters problem find a set of val uations within a given rectangle for which the system behaves well We give here the installation requirements and the launching commands of IMITATOR II as well as the source code of a toy example 1 Introduction Timed automata 2 are finite control automata equipped with clocks which are real valued variables which increase uniformly This model is useful for reasoning about real time systems with a dense representation of time because one can specify guantitatively the interval of time during which the transitions can occur using timing bounds However the behavior of a system is very sensitive to the values of these bounds and it is rather difficult to find their correct values One can check the correctness of the system for
10. Norl 0 goto Norl1_ 011 when True sync overQ Down do ckNorl 0 goto Nor1_101 when ckNorl gt dNorl l sync Q_Down do goto Nor1_110 end norGatel AKC AKC OC A AO AOI IG A I A k k aK k k k k k kk ak ak kk automaton norGate2 GROG OR RO GG ORCA OO AO IG IGA IG k k k k k k k aK k k k kkk kk synclabs Q Up Q_Down S_Up S Down overQ Up overQ_Down initially Nor2_110 initially Nor2_001 24 UNSTABLE loc Nor2_000 while ckNor2 lt dNor2 u wait when True sync Q Up do goto Nor2_100 when True sync S_Up do goto Nor2 010 when ckNor2 gt dNor2_1 syne overQ_Up do goto Nor2_001 STABLE loc Nor2_001 while True wait when True sync Q_Up do ckNor2 0 goto Nor2_101 when True sync S_Up do ckNor2 0 goto Nor2_011 STABLE loc Nor2_010 while True wait when True sync Q_Up do goto Nor2 110 when True sync S Down do ckNor2 0 goto Nor2_000 UNSTABLE loc Nor2_011 while ckNor2 lt dNor2_u wait when True sync Q_Up do ckNor2 0 goto Nor2 111 when True sync S_Down do goto Nor2 001 when ckNor2 gt dNor2_1 sync overQ_Down do goto Nor2_010 STABLE loc Nor2 100 while True wait when True sync Q Down do ckNor2 0 goto Nor2_000 when True sync S_Up do goto Nor2_110 UNSTABLE loc Nor2_101 while ckNor2 lt dNor2_u wait when True sync O Down do goto Nor2_001 when True sync S_Up do c
11. R II in Section 3 and give details on its internal structure and its various features We give in Sec tion 4 the most useful in order to install and use IMITATOR II We present in lhttp www lsv ens cachan fr andre IMITATOR2 Section 5 a full example and show the application of the inverse method and the behavioral cartography algorithm using IMITATOR II We give final remarks in Section 6 We also give in Appendix A the source code of the example and in Appendix B the full grammar of IMITATOR II 2 Behavioral Cartography of Timed Automata In this section we first briefly recall the framework of Parametric Timed Au tomata Section 2 1 We then introduce the Root Contention Protocol as a motivating example Section 2 2 We then recall the inverse method algo rithm described in 4 Section 2 3 and the behavioral cartography algorithm described in 5 Section 2 4 2 1 Parametric Timed Automata We use in this paper the same formalism as in 5 Throughout this paper we assume a fixed set X 21 y of clocks and a fixed set P pi PM of parameters We assume familiarity with timed automata 2 Parametric timed automata are an extension of timed automata to the parametric case allowing within guards and invariants the use of parameters in place of constants 3 Given a set of clocks X and a set of parameters P a parametric timed automaton PTA A is a 6 tuple of the form A 9 go K I where is
12. TATOR II on a theoretical point of view and to find applications both from the literature and real case studies Abdelrezzak Bara provided several examples from the hardware literature Jeremy Sproston pro vided examples from the probabilistic community Bertrand Jeannet has been of great help on the installation part and the linking with Apron 18 Ul rich Kithne started to improve IMITATOR II and added the link with PPL 20 References 1 10 11 12 13 14 15 R Alur C Courcoubetis T A Henzinger and P H Ho Hybrid automata An algorithmic approach to the specification and verification of hybrid systems In Hybrid Systems pages 209 229 1992 R Alur and D L Dill A theory of timed automata TCS 126 2 183 235 1994 R Alur T A Henzinger and M Y Vardi Parametric real time reasoning In STOC 93 pages 592 601 ACM 1993 Andr T Chatain E Encrenaz and L Fribourg An inverse method for parametric timed automata International Journal of Foundations of Computer Science 20 5 819 836 2009 Andr and L Fribourg Behavioral cartography of timed automata In RP 10 LNCS Springer 2010 To appear Andr L Fribourg and J Sproston An extension of the inverse method to probabilistic timed automata In AVoCS 09 volume 23 of Electronic Communications of the EASST 2009 Etienne Andr IMITATOR II web page http www lsv ens cachan fr and
13. TOR II is written in OCaml and makes use of the following libraries e The APRON numerical abstract domain library 18 and its interface with OCaml e The OCaml ExtLib library Extended Standard Library for Objective Caml e The Parma Polyhedra Library PPL 9 Various binaries are available on IMITATOR II s Web page 4 2 The Imitator II Input File The syntax of the automata in IMITATORII is similar to the syntax of the automata for HY TECH 4 2 1 Variables Discrete variables clocks and parameters variable names must be disjoint The synchronization label names may be identical to other names automata or variables The automata names may be identical to other names variables synchronization labels 4 2 2 Parametric Timed Automata See Appendix B 4 2 3 Initial region and To See Appendix B 4 3 Calling Imitator II IMITATOR II can be used with three different modes 1 Reachability analysis given a PTA A compute the whole set of reachable states from a given initial state 2 Inverse Method given a PTA A and a valuation Ty of the parameters compute a constraint on the parameters guaranteeing the same behavior as under To 4 3 Behavioral Cartography Algorithm given a PTA A and a rectangle Vo bounded interval of values for each parameter compute a cartography of the system 5 We detail those three modes below 11 4 3 1 Reachability Analysis Given a PTA A the reachability analysis computes
14. a finite set of actions Q is a finite set of locations go O is the initial location K is a constraint on the parameters is the invariant assigning to every q Q a constraint Ig on the clocks and the parameters and is a step relation consisting in elements of the form q g a p q where q EQ a E pC X is a set of clocks to be reset by the step and g the step guard is a constraint on the clocks and the parameters In the sequel we consider the PTA A 2 Q q0 K 1 gt We simply de note this PTA by A K in order to emphasize the fact that only K will change in A For every parameter valuation 7 71 M Afr denotes the PTA A K where K is A pi mi This corresponds to the PTA obtained from A by substituting every occurrence of a parameter p by constant m in the guards and invariants We say that p is instantiated with 7 Note that as all param eters are instantiated A 7r is a standard timed automaton Strictly speaking Alm is only a timed automaton if 7r assigns an integer to each parameter A symbolic state s of A K is a couple q C where q is a location and C a constraint on the clocks and the parameters A run of A K is an alternating sequence of states and actions of the form 6 Bs 3 Ss Sm such that for alli 0 m 1 a Nand si 544 is a step of A K Given a PTA A and a run R of A of the form go Co Y dm Cm the trace associated to R is the alternating seque
15. ation of the whole parametric state space In 12 they propose an extension based on the counterezample guided ab straction refinement CEGAR 11 When finding a counterexample the sys tem obtains constraints on the parameters that make the counterexample in feasible When all the counterexamples have been eliminated the resulting constraints describe a set of parameters for which the system is safe The tool IMITATORII presented in this paper is based on the inverse method 4 which supposes given a good instantiation mo of the parameters that one wants to generalize More precisely IMITATOR II generates a constraint Ko on the parameters that corresponds to an infinite dense set of valuations such that for all instantiation 7 of parameters in this set the behavior of the timed automaton A is time abstract equivalent to the behavior of A under ro in the sense that they have the same trace sets This is useful to relax timing bounds and gives a criterion of robustness Moreover IMITATOR II implements the behavioral cartography algorithm 5 which generates a constraint on the parameters tile by calling the inverse method for each integer point located within a given rectangle Vo This algo rithm allows us to partition the parametric space into a subset of good tiles which correspond to good behaviors and a subset of bad ones Often in practice what is covered is not the bounded and integer subspace
16. drawn followed by the sending of a message to the contending neighbor This is repeated by both nodes until one of them receives a message before sending one at which point the root is appointed We consider the following five timing parameters e rc fast min resp rc fast _maz gives the lower resp upper bound to the waiting time of a node that has drawn 1 e rc slow min resp rc_slow_maz gives the lower resp upper bound to the waiting time of a node that has drawn 0 e delay indicates the maximum delay of signals sent between the two con tending nodes Those timing parameters are bound by the following implicit constraint rc_fast_min lt rc_fast_maz A re slow_min lt rc_slow_maz We consider the following instantiation mo of the parameters given in 19 and rescaled from the original IEEE valuation rc_fast_min 76 re_fast_maz 85 delay 36 rc_slow_min 159 rc_slow_max 167 Let us consider the following property Prop The minimum probability that a leader is elected within five rounds is greater or equal to 0 75 We consider that the system behaves well if this property is satisfied We can 2The IEEE reference instantiation is given in ns but due to the rescaling we omit the unit here 3Recall that we model here the Root Contention Protocol using non probabilistic para metric timed automata in which the random choice between 0 and 1 is modeled by non determinism as in 17 Therefore in order t
17. ersemethod option is not necessary since the de fault value for mode is precisely inversemethod Note that unlike the algorithm given in 4 at a given iteration the 7o incompatible state is selected deterministically for efficiency reasons However the ro incompatible inequality within a ry incompatible state is selected ran domly unless the no random option is activated In this case IMITATOR II outputs the resulting constraint Ko on the standard output Moreover IMITATOR II outputs the same two files as in the reachability analysis 4 3 3 Cartography Given a PTA A and a rectangle Vo bounded interval of values for each param eter the Behavioral Cartography Algorithm computes a cartography of the system 5 Two possible variants of the algorithm can be used 1 The standard variant covers all the integer points within Vo The syntax in this case is the following one IMITATOR2 lt input file gt lt VO file gt mode cover options 12 2 The alternative variant calls the inverse method a certain number of times on a random point Vo The syntax in this case is the following one IMITATOR2 lt input file gt lt VO_file gt mode randomX options where X represents the number of random points to consider If a point has already been generated before the inverse method is not called If a point belongs to one of the tiles computed before the inverse method is not called neither Therefore in practice the number
18. es of the parameters Our tool has been successfully applied to various examples of asynchronous circuits and protocols Future works include e an automatic generation of the cartography under a graphical form so far only the trace sets are automatically generated under a graphical form the cartography itself is given under the form of a list of constraints e an automatic verification of the property one wants to check e g by using a tool such as UPPAAL 20 e a dynamic cartography where the scale so far the integers can be refined to fill the possible holes e a backward analysis i e considering a Pre operation instead of Post computation in Algorithm 1 e the reachability analysis of a given state and the generation of a trace from the initial state to this given state e the extension to hybrid systems e the automatic generation of the probabilities of a given property in the probabilistic framework without the use of an external tool e g Prism 16 e the automatic generation of the next point not covered by Tiling with out testing all the integer points note that a random generation of points is already implemented e the possibility to compute several tiles in parallel in the cartography al gorithm e a user friendly graphical interface e the possibility to save and load sets of states Acknowledgments Emmanuelle Encrenaz and Laurent Fribourg have been great contributors of IMI
19. fore Q can occur thus leading to event O 18 5 0001 Figure 11 Trace set of tile 5 for the SR latch Tile 6 This tile corresponds to the values of the parameters verifying the following constraint tt gt g The trace set of this tile is given in Fig 12 Da tou Figure 12 Trace set of tile 6 for the SR latch Since t gt ds o occurs before St The system is then stable Cartography We give in Fig 13 the cartography of the SR latch example For the sake of simplicity of representation we consider only parameters 1 and 03 Therefore we set t 1 02 l Figure 13 Behavioral cartography of the SR latch according to 01 and 62 Note that tile 1 corresponds to a point and tiles 2 and 4 correspond to lines The rectangle Vo has been represented with dashed lines Note that all tiles except tile 1 are unbounded so that they cover not only Vo but all the positive real valued plan 19 The source code of this example is available in Appendix A 6 Final Remarks The tool IMITATOR II allows us to solve the good parameters problem for timed automata by iterating the inverse method algorithm on the integer points of a given rectangular parameter domain Vo In practice our cartography algorithm covers not only most of Vo but also a significant part of the whole parametric space beyond Vo This is of interest to classify the behavior of the system into good or bad for dense and unbounded valu
20. iming information to each output of the program with parametric log default false For any constraint on the clocks and the parameters in the description of the states in the log files add the constraint on the parameters only i e eliminate clock variables In such a case the synchronization label is actually completely removed before the exe cution in order to optimize the execution and the user is warned of this removal 14 4 3 5 Examples of Calls IMITATOR2 flipflop imi mode reachability Computes a reachability analysis on the automata described in file flipflop imi Will generate files flipflop imi states containing the description of the reachable states and flipflop imi gif depicting the reachability graph IMITATOR2 flipflop imi flipflop pi0 Calls the inverse method on the au tomata described in file flipflop imi and the reference valuation ro given in file flipflop pi0 The resulting constraint Kg will be given on the standard output Moreover IMITATORII will generate the file flipflop imi states containing the description of the parametric states reachable under Ko and the file flipflop imi gif depicting the reachability graph under any point T Ko IMITATOR2 flipflop imi flipflop pi0 no dot no log Calls the in verse method on the automata described in file flipflop imi and the reference valuation given in file flipflop pi0 The resulting constraint will be given on the standard output No file wil
21. inear_term rational rational lt name gt rational lt name gt lt name gt C linear_term rational integer integer pos_integer integer pos_integer pos_integer pos_integer lt int gt B 1 2 Initial State init init_declaration init_definition reach_command 30 init_declaration var init region reach_command print reach forward from init endreach loe init_definition init region_expression region_expression state_predicate region_expression region_expression region_expression state_predicate loc lt name gt lt name gt linear_constraint B 2 Reserved Words The following words are keywords and cannot be used as names for automata variables synchronization labels or locations and automaton clock discrete do end endreach False forward from goto if in init initially loc locations not or parameter print reach region sync synclabs True var wait when while 31
22. kNor2 0 goto Nor2_111 when ckNor2 gt dNor2_1 sync overO Down do goto Nor2 100 STABLE loc Nor2_110 while True wait when True sync Q Down do goto Nor2 010 when True sync S Down do goto Nor2 100 UNSTABLE loc Nor2_111 while ckNor2 lt dNor2_u wait 25 125 128 130 131 132 133 134 135 136 137 138 139 140 141 142 143 145 146 147 148 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 when True sync O Down do ckNor2 0 goto Nor2 011 when True sync S Down do ckNor2 Nor2_101 when ckNor2 gt dNor2_1 sync overQ_Down do goto Nor2_110 0 goto end norGate2 KOK KKK KOK RI K K K K K K K K K K K K K K K K K K K K KK KK K K K K K K K K K K K K KK kK KKK KKK KK automaton env KOK KOK KKK OK E K K K K K K K K K K K K K K K K K k K K K KK KK K K K K K K K K KK KK K K kK KKK KKK kK synclabs R Down R Up S Down S Up initially env 11 ENVIRONMENT first S then R at constant time loc env 11 while True wait when True sync S Down do s 0 goto env_10 loc env_10 while s lt t_down wait when s t_down sync R Down do goto env final loc env final while True wait end env var init region init True INITIAL LOCATIONS S and R down amp loc no
23. l be generated IMITATOR2 flipflop imi flipflop pi0 with parametric log Calls the inverse method on the automata described in file flipflop imi and the ref erence valuation mg given in file flipflop pi0 The resulting constraint Ko will be given on the standard output and IMITATOR II will generate the file flipflop imi states containing the description of the parametric states reachable under Kp Moveover for any state in this file both the constraint on the clocks and the parameters and the constraint on the parameters will be given IMITATOR II will also generate the file flipflop imi gif depicting the reachability graph under any point 7 Ko IMITATOR2 SRlatch imi SRlatch v0 mode cover Calls the behavioral cartography algorithm on the automata described in file flipflop imi and the rectangle Vo given in file SRlatch v0 The algorithm will cover at least all the integer points within Vo The resulting set of tiles will be given on the standard output Given n the number of generated tiles i e the number of calls to the inverse method algorithm the program will generate n files of the form SRlatch imi_i states resp n files of the form SRlatch imi_ gif giving the description of the states resp the reachability graph of tile for 1 1 n IMITATOR2 SRlatch imi SRlatch v0 mode random100 no log Calls the behavioral cartography algorithm on the automata described in file flipflop imi and the rectangle Vo given in file
24. me Thus the order of those two events is unspecified which explains the choice between going to q2 or q3 When in state q2 Qt can not occur since 9 gt 0 so O occurs immediately after R which leads to stability 17 St Q 7 Oe Figure 8 Trace set of tile 2 for the SR latch Tile 3 This tile corresponds to the values of the parameters verifying the following constraint bg gt th The trace set of this tile is given in Fig 9 a _ Figure 9 Trace set of tile 3 for the SR latch In this case since d2 gt tt 6 St will occur before the gate Nors has the time to change For the same reason will change before Nor has the time to change With Q 1 the system is now stable Nor does not change Tile 4 This tile corresponds to the values of the parameters verifying the following constraint tY 6 A gt gt 01 A gt 0 The trace set of this tile is given in Fig 10 UI St gt a RY Figure 10 Trace set of tile 4 for the SR latch Since ti 6 69 both Q or a can occur Once one of them occured the system gets stable and no other change occurs Tile 5 This tile corresponds to the values of the parameters verifying the following constraint de gt tt A th 6 gt 62 The trace set of this tile is given in Fig 11 Since gt gt tt the gate Norz can not change before R occurs However since tt 6 gt 62 the gate Norz changes be
25. nce of locations and actions am 1 do Byrn T dm The trace set of A refers to the set of traces associated to the runs of A In the following we are interested in verifying properties on the trace set of A For example given a predefined set of bad locations a reachability property is satisfied by a trace if this trace never contains a bad location such a trace is good w r t this reachability property A trace can also be said to be good if a given action always occurs before another one within the trace see 5 Actually the good behaviors that can be captured with trace sets are relevant to linear time properties 10 which can express properties more general than reachability properties Formally given a property on traces we say that a trace is good if it satisfies the property and bad otherwise Likewise we say that a trace set is good if all its traces are good and bad otherwise 2 2 A Motivating Example Consider the Root Contention Protocol of the IEEE 1394 FireWire High Performance Serial Bus studied in the parametric framework in 17 As de scribed in 17 this protocol is part of a leader election protocol in the physical layer of the IEEE 1394 standard which is used to break symmetry between two nodes contending to be the root of a tree spanned in the network tech nology The protocol consists in first drawing a random number 0 or 1 then waiting for some time according to the result
26. nce valuation To synthesize a constraint guaranteeing the same trace set as for A mo e Behavioral cartography algorithm given a PTA A and a rectangular pa rameter domain Vo compute a list of tiles Two different modes can be considered 1 cover all the integer points of Vo or 2 call a given number of times the inverse method on an integer point selected randomly within Vo which is interesting for rectangles containing a very big number of integer points but few different tiles e Automatic generation of the trace sets for the reachability analysis and for both algorithms M and BC e Output of the trace sets under a graphical form As shown in Table 1 all those features except the inverse method are new features which were not available in IMITATOR Tool Inverse Method Cartography Computation of traces Graphical output IMITATOR Yes IMITATOR II Yes Yes Yes Yes Table 1 Comparison of the features of IMITATOR and IMITATOR II See Section 4 3 4 for the list of options available when calling IMITATOR II SDiscrete variables are syntactic sugar allowing to factorize several locations into a sin gle one In IMITATORII discrete variables are integer variables that can be updated using constants or other discrete variables 10 4 How to Use Imitator II 4 1 Installation See the installation files available on the website for the most up to date infor mation In short IMITA
27. ne recall that rc_fast_min 76 and rc_fast max 85 2 rc slow min gt 3 delay 170 A delay lt 38 A re slow min lt re slow mar 3 General Structure and Implementation 3 1 Inputs and Outputs The input syntax of IMITATOR II to describe the network of PTAs modeling the system is given in 7 and is very close to the HYTECH syntax Actually all standard HYTECH files describing only PTAs and not more general systems 4Note that what IMITATORII computes is a list of tiles as well as the associated trace sets We then use an external tool here PRISM in order to verify for each tile whether the considered property Prop is satisfied or not Note that this step could be easily integrated to IMITATOR II in automatic manner see final remarks in Section 6 re slow_min 220 210 200 190 180 170 160 150 140 130 120 110 90 80 00 10 20 30 40 50 60 70 80 90 100 delay Figure 1 Behavioral cartography of the Root Contention Protocol according to delay and rc_slow_min like linear hybrid automata 1 can be analyzed directly by IMITATORII with very minor changes Inverse Method When calling IMITATOR II to apply the inverse method al gorithm the tool takes as input two files one describing the network of PTAs modeling the system and the other describing the reference valuation As de picted in Figure 2 it synthesizes a constraint on the parameters solving the inverse problem as well as the
28. o compute probabilities we need to consider a model involving probabilistic timed automata i e timed automata augmented with probabil ities It can be shown see 6 that the minimum or maximum probability of satisfying a given property can be computed directly from the non probabilistic trace set As a consequence the property that we consider for this example is purely a trace property show that for the reference valuation 7 the system behaves well i e its trace set is a good trace set We are now looking for other valuations around Ty such that the system has the same good behavior More formally we are interested in solving the following inverse problem The Inverse Problem Given a PTA A and a reference valuation mo generate a constraint Kg such that 1 TO Ko and 2 for all 7 72 Ko the trace sets of Al n and A r2 are equal 2 3 The Inverse Method We recall here the inverse method algorithm IM A 7 as defined in 4 which solves the inverse problem Starting with K true we iteratively compute a growing set of reachable states When a r incompatible state q C is encoun tered i e when 7 4 C K is refined as follows a r incompatible inequality J i e such that m 4 J is selected within the projection of C onto the parameters and J is added to K The procedure is then started again with this new K and so on until no new state is computed We finally return the intersecti
29. of the param eter rectangle but two major extensions first not only the integer points but a major part of the dense set of real valued points of the rectangle is covered by the tiles second the tiles are often unbounded w r t several dimensions hence are infinite and cover most of the parametric space beyond Vo thus giving a solution to the good parameters problem IMITATOR IT is a new version of IMITATOR 8 a prototype written in Python implementing the inverse method and calling the model checker HYTECH 14 IMITATOR II has been entirely rewritten and is a now standalone tool making use of the APRON library 18 and the Parma Polyhedra Library 9 Compared to IMITATOR the computation timings of IMITATOR II have dramatically de creased Moreover IMITATOR II offers new features such as the implementation of the behavioral cartography algorithm the generation of the trace sets of the models and a graphical output We present in this paper the new features and optimizations of IMITATOR II as well as a range of case studies This tool is being developed at LSV ENS Cachan France The tool can be downloaded on its Web page as well as a bunch of case studies Organization of this user manual We first recall the framework of Para metric Timed Automata the inverse method algorithm and the behavioral car tography algorithm in Section 2 We also apply those two algorithms to the Root Contention Protocol We then introduce IMITATO
30. of tiles generated is smaller than X 4 3 4 Options The options available for IMITATOR II are explained in the following acyclic default false Does not test if a new state was already encoun tered In a normal use when IMITATORII encounters a new state it checks if it has been encountered before This test may be time consuming for systems with a high number of reachable states For acyclic systems all traces pass only once by a given location As a consguence there are no cycles so there should be no need to check if a given state has been encountered before This is the main purpose of this option However be aware that even for acyclic systems several different traces can pass by the same state In such a case if the acyclic option is activated IMITATOR II will compute twice the states after the state common to the two traces As a conseguence it is all but sure that activating this option will lead to an increase of speed Note also that activating this option for non acyclic systems may lead to an infinite loop in IMITATOR II debug default standard Give some debugging information that may also be useful to have more details on the way IMITATOR II works The admissible values for debug are given below nodebug Give only the resulting constraint standard Give little information number of steps computation time low Give little additional debugging information medium Give quite a lot of debugging information
31. on of the projection onto the parameters of all the constraints associated to the reachable states The output of IM is a behavioral tile in the following sense A constraint K is said to be a behavioral tile or more simply a tile if for all 71 72 K the trace sets of A r1 and A r2 are equal Note that a tile corresponds to a convex and dense set of real valued points Given a tile K the trace set of A K will be simply referred to as the trace set of K Note that such a trace set is a possibly infinite set of traces Algorithm 1 IM A 7 input A PTA A of initial state so qo Ko input Valuation 7 of the parameters output Constraint K on the parameters 1i 0 K lt true S lt so 2 while true do 3 while there are r incompatible states in S do 4 Select a r incompatible state q C of S i e s t m FC 5 Select a r incompatible J in AX C ie st m FJ 6 KeKAAJ 7 Se Uj o Post 50 8 if Post 4k S E S then return K amp Nu oes AX C 9 1 1i 1 10 S lt SU Posta S S Wyn Postic 30 The algorithm M is given in Algorithm 1 Given a linear inequality J of the form e lt e resp e lt e the expression J denotes the negation of J and corresponds to the linear inequality e lt e resp e lt e Given a constraint C on the clocks and the parameters the expression 1X C denotes the constraint on the parameters obtained from C after elimination of the clocks
32. one particular timing value for each timing bound using model checkers such as e g UPPAAL 20 but this does not give any information for other values Actually testing the correctness of the system for all the timing values even in a bounded interval would reguire an infinite number of calls to the model checker because those timing bounds can have real or rational values It is therefore interesting to reason parametrically by considering that these bounds are unknown constants or parameters and try to synthesize a constraint i e a conjunction of linear inegualities on these parameters which will guar antee a correct behavior of the system Such automata are called parametric timed automata PTA 3 The Good Parameters Problem for Timed Automata In order to find correct values of the parameters we are interested in solving the following good parameters problem as defined in 12 in the framework of linear hybrid au tomata Given a PTA A and a rectangular parameter domain Vo what is the largest set of parameter values within Vo for which A is safe The parameter design problem for timed automata and more generally for linear hybrid automata was formulated in 15 where a straightforward solution is given based on the generation of the whole parametric state space until a fixpoint is reached Unfortunately in all but the most simple cases this is is prohibitively expensive due in particular to the brute explor
33. owing values for each signal State SIR OO do 1 17 70 O q 017 000 q2 007 0 0 43 0 1 0 1 da 0 0 011 q5 010 110 qe 0 0 011 5 2 Behavioral Cartography Algorithm Using IMITATOR II we now perform a behavioral cartography of this system We consider the following rectangle Vo for the parameters 16 Figure 6 Parametric reachability analysis of the SR latch tte 0 10 01 O 10 03 O 10 The launch command for IMITATOR II is the following one IMITATOR2 SRlatch imi SRlatch vO mode cover We get the following six behavioral tiles Note that the graphical outputs automatically generated by IMITATOR II in the gif format were rewritten in TeX in this document Tile 1 This tile corresponds to the values of the parameters verifying the following constraint th do A 6 0 The trace set of this tile is given in Fig 7 Figure 7 Trace set of tile 1 for the SR latch Since t 6 R and o will occur at the same time Thus the order of those two events is unspecified which explains the choice between going to qa or ga When in state q2 either Qt can occur since 6 0 in which case the system is stable or o can occur which also leads to stability Tile 2 This tile corresponds to the values of the parameters verifying the following constraint th 62 A 6 gt 0 The trace set of this tile is given in Fig 8 Since t 69 R and al will occur at the same ti
34. rGatel Nor1_100 amp loc norGate2 Nor2_010 amp loc env env ll INITIAL CONSTRAINTS amp ckNorl 0 amp ckNor2 0 amp s 0 amp dNor1_1 gt 0 26 o Yo a A Ww No amp dNor2_1 gt amp dNor1_1 lt amp dNor2_1 lt A 2 V File dNorl_u dNor2_u VO amp dNor1_1 amp dNorl_u amp dNor2_1 amp dNor2_u amp t_down 20 20 n nw Ww 27 B Complete Grammar B 1 Grammar of the Input File IMITATOR II input is described by the following grammar Non terminals appear within angled parentheses A non terminal followed by two colons is defined by the list of immediately following non blank lines each of which represents a legal expansion Input characters of terminals appear in typewritter font The meta symbol e denotes the empty string The text in green is not taken into account by IMITATOR II but is allowed or sometimes necessary in order to allow the compatibility with HYTECH files imitator_input automata_descriptions init We define each of those two components below B 1 1 Automata Descriptions automata_descriptions declarations automata declarations var var_lists var_lists var_list var_type var_lists loe var_list lt name gt lt name gt var list var_type clock discrete parameter automata automaton automata automaton automaton lt
35. re IMITATOR2 tienne Andr IMITATOR A tool for synthesizing constraints on timing bounds of timed automata In CTAC 09 volume 5684 of LNCS pages 336 342 Springer 2009 R Bagnara P M Hill and E Zaffanella The Parma Polyhedra Library Toward a complete set of numerical abstractions for the analysis and veri fication of hardware and software systems Science of Computer Program ming 72 1 2 3 21 2008 C Baier and J P Katoen Principles of Model Checking The MIT Press 2008 E M Clarke O Grumberg S Jha Y Lu and H Veith Counterexample guided abstraction refinement In CAV 00 pages 154 169 Springer Verlag 2000 G Frehse S K Jha and B H Krogh A counterexample guided approach to parameter synthesis for linear hybrid automata In HSCC 08 volume 4981 of LNCS pages 187 200 Springer 2008 D Harris and S Harris Digital Design and Computer Architecture Morgan Kaufmann Publishers Inc San Francisco CA USA 2007 T A Henzinger P H Ho and H Wong Toi Hytech A model checker for hybrid systems Software Tools for Technology Transfer 1 460 463 1997 T A Henzinger and H Wong Toi Using HYTECH to synthesize control parameters for a steam boiler In Formal Methods for Industrial Applica tions Specifying and Programming the Steam Boiler Control LNCS 1165 Springer Verlag 1996 21 16 A Hinton M Kwiatkowska G Norman and D Parker PRISM A tool for automatic verification of p
36. robabilistic systems In TACAS 06 volume 3920 of LNCS pages 441 444 Springer 2006 17 T S Hune J M T Romijn M I A Stoelinga and F W Vaandrager Lin ear parametric model checking of timed automata Journal of Logic and Algebraic Programming 2002 18 B Jeannet and A Min Apron A library of numerical abstract domains for static analysis In CAV 709 volume 5643 of LNCS pages 661 667 Springer 2009 19 M Kwiatkowska G Norman and J Sproston Probabilistic model check ing of deadline properties in the IEEE 1394 FireWire root contention pro tocol Formal Aspects of Computing 14 3 295 318 2003 20 K G Larsen P Pettersson and W Yi UPPAAL in a nutshell International Journal on Software Tools for Technology Transfer 1 1 2 134 152 1997 22 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 A Source Code of the Example A 1 Main Input File GIGS RIL LE SSIS SIS GE kk k k k kk Laboratoire Specification et Verification Race on a digital circuit SR Latch Etienne ANDRE Created 2010 03 19 Last modified 2010 03 24 GIGI kkk kk GSS kaka var ckNorl ckNor2 s clock dNor1_1 dNorl_u dNor2_1 dNor2_u t_down parameter OSGI GCG dd kkk automaton norGatel GOSS dd kkk synclab
37. s R_Up R Down overQ Up overQ Down Q Up Q Down initially Nor1_110 UNSTABLE loc Norl_000 while ckNorl lt dNorl_u wait when True sync R Up do goto Nor1_100 when True sync overQ_Up do goto Nor1_010 when ckNorl gt dNorl_l sync Q_Up do goto Nor1_001 STABLE loc Norl_001 while True wait when True sync R_Up do ckNorl 0 goto Nor1_101 when True sync overQ_Up do ckNorl 0 goto Nor1_011 STABLE loc Norl_010 while True wait when True sync R_Up do goto Norl 110 23 44 45 47 48 when True sync overQ_Down do ckNorl 0 goto Nor1_000 UNSTABLE loc Norl_011 while ckNorl lt dNorl u wait when True sync R_Up do ckNorl 0 goto Nor1_111 when True sync overQ_Down do goto Norl 001 when ckNorl gt dNorl_l sync Q Down do goto Nor1_010 STABLE loc Norl_100 while True wait when True sync R Down do ckNorl 0 goto Nor1_000 when True sync overQ_Up do goto Nor1_110 UNSTABLE loc Norl_101 while ckNorl lt dNorl_u wait when True sync R Down do goto Nor1_001 when True sync overQ_Up do ckNorl 0 goto Nor1_111 when ckNorl gt dNorl_l sync O Down do goto Nor1_100 STABLE loc Norl_110 while True wait when True sync R Down do goto Norl 010 when True sync overQ_Down do goto Norl 100 UNSTABLE loc Norl_111 while ckNorl lt dNorl u wait when True sync R Down do ck
38. t select an inequality in a random manner post limit lt limit gt default none Limits the number of iterations in the Post exploration i e the depth of the traces In the cartography mode this option gives a limit to each call to the inverse method sync auto detect default false IMITATOR II considers that all the au tomata declaring a given synchronization label must be able to synchronize all together so that the synchronization can happen By default IMITATOR II considers that the synchronization labels declared in an automaton are those de clared in the synclabs section Therefore if a synchronization label is declared but never used in at least one automaton this label will never be synchronized in the execution The option sync auto detect allows to detect automatically the synchro nization labels in each automaton the labels declared in the synclabs section are ignored and the IMITATOR II considers that only the labels really used in an automaton are those considered to be declared time limit lt limit gt default none Try to limit the execution time the value lt limit gt is given in seconds Note that in the current version of IM ITATORII the test of time limit is performed at the end of an iteration only i e at the end of a given Post iteration In the cartography mode this option represents a global time limit not a limit for each call to the inverse method timed default false Add a t
39. t of tiles initially empty 1 repeat 2 select an integer point 7 Vo 3 if m does not belong to any tile of Tiling then 4 Add IM A 7 to Tiling 5 until Tiling contains all the integer points of Vo Note that two tiles with distinct trace sets are necessarily disjoint On the other hand two tiles with the same trace sets may overlap In practice most of the real valued space of Vo is covered by Tiling Fur thermore the space covered by Tiling often largely exceeds the limits of Vo see 5 for a sufficient condition of full coverage of the parametric space Partition Between Good and Bad Tiles According to a given property on traces one wants to check it is possible to partition trace sets between good and bad Once one has decided which tiles are good and which ones are bad one can partition the rectangle Vo into a good subspace union of good tiles and a bad subspace union of bad tiles Advantages First the cartography itself does not depend on the property one wants to check Only the partition between good and bad tiles involves the considered property Moreover the algorithm is interesting because one does not need to compute the set of all the reachable states On the contrary each call to the inverse method algorithm quickly reduces the state space by removing the bad states This allows us to overcome the state space explosion problem which prevents other methods such as the computation of the whole set
Download Pdf Manuals
Related Search