IMITATOR User Manual
Contents
1. sync auto detect default false IMITATOR considers that all the IPTA declaring a given action must be able to synchronize all together so that the synchronization can happen By default IMITATOR considers that the actions declared in an IPTA are those declared in the synclabs section Therefore if an action is declared but never used in at least one IPTA this label will never be synchronized in the execution The option sync auto detect allows to detect automatically the actions in each IPTA the actions declared in the synclabs section are ignored and IMITATOR considers as declared actions only the actions really used in this IPTA time limit limit default none Try to limit the execution time the value limit is given in seconds Note that in the current version of IMITATOR the test of time limit is performed at the end of an iteration only i e at the end of the exploration of the state space at the current depth 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 timing information to each shell output of the program tree default false Does not test if a new state was already encountered To be set only if the reachability graph is a tree with all states being different otherwise analysis may loop verbose default standard Give some debugging information that may also be useful to have more details on2. c 1 constant Then any occurrence of c in the model is replaced with 1 Constants are unbounded exact integers Hint 1 In fact a variable e g a parameter can be turned to a constant as follows in the definition of the parameters p 2 parameter An alternative is an automatic recognition of the actions used see option sync auto detect in Chapter 7 3In this case IMITATOR will detect this situation and will entirely delete this action from the model while issuing a warning 17 This is equivalent to replacing p with 2 everywhere in the model this is partic ularly useful when some parameters should be instantiated In contrast if the parameter is instantiated in the initial definition IMITATOR still counts it as a parameter which makes all constraints suffer from an additional dimension 18 Chapter 4 Parameter Synthesis Using IMITATOR We give here the commands corresponding to the main analysis features of IMITATOR We only give the most useful options For more detailed commands and a complete list of options see Chapter 7 4 1 State Space Computation IMITATOR can compute the entire symbolic state space parametric zone graph Of course the state space may be infinite and this analysis is not guar anteed to terminate The standard command is imitator model imi mode statespace output states The option output states generates a file with a textual description of all
3. International Journal of Foundations of Computer Science 20 5 819 836 2009 4 21 Rajeev Alur Costas Courcoubetis Thomas A Henzinger and Pei Hsin Ho Hybrid automata An algorithmic approach to the speci fication and verification of hybrid systems In Robert L Grossman Anil Nerode Anders P Ravn and Hans Rischel editors Hybrid Sys tems 1992 volume 736 of Lecture Notes in Computer Science pages 209 229 Springer 1993 5 Etienne Andr Camille Coti and Hoang Gia Nguyen En hanced distributed behavioral cartography of parametric timed automata In ICFEM 15 Lecture Notes in Computer Science Springer November 2015 28 tienne Andr and Laurent Fribourg Behavioral cartography of timed automata In Antonin Ku era and Igor Potapov editors Pro 45 AFKS12 AFS13 AHHH 13 AHV93 ALNS15 AM15 And13a ceedings of the 4th Workshop on Reachability Problems in Compu tational Models RP 10 volume 6227 of Lecture Notes in Computer Science pages 76 90 Springer August 2010 4 21 22 tienne Andr Laurent Fribourg Ulrich K hne and Romain Soulat IMITATOR 2 5 A tool for analyzing robustness in schedul ing problems In Dimitra Giannakopoulou and Dominique M ry editors Proceedings of the 18th International Symposium on For mal Methods FM 12 volume 7436 of Lecture Notes in Computer Science pages 33 36 Paris France August 2012 Springer 4 tienne Andr Laurent Fribourg
4. editors TACAS 95 volume 1019 of Lecture Notes in Computer Science pages 41 71 Springer 1995 5 16 33 IMITATOR Team IMITATOR Web page 2015 4 26 Aleksandra Jovanovi Didier Lime and Olivier H Roux Integer parameter synthesis for timed automata IEEE Transactions on Software Engineering TSE 2015 To appear 4 20 29 Bertrand Jeannet and Antoine Min Apron A library of numerical abstract domains for static analysis In CAV 09 volume 5643 of LNCS pages 661 667 Springer 2009 42 Kim Guldstrand Larsen Paul Pettersson and Wang Yi UPPAAL in a nutshell International Journal on Software Tools for Technology Transfer 1 1 2 134 152 1997 16 Jun Sun Yang Liu Jin Song Dong and Jun Pang PAT Towards flexible verification under fairness In CAV volume 5643 of Lecture Notes in Computer Science pages 709 714 Springer 2009 5 47
5. CS2 while True wait when True sync exit 2 do counter counter 1 turn IDLE x2 0 goto idle2 end proc2 automaton observer ee ae e e ae ae OGG IGG GIO E A e A fe A De AF A AGRI IC ACCC aca e dle d a ak synclabs enter 1 enter 2 exit 1 exit 2 loc obs waiting while True wait when True sync enter 1 goto obs 1 when True sync enter 2 goto obs 2 loc obs 1 while True wait when True sync exit 1 goto obs waiting when True sync enter 2 goto obs violation 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 loc obs 2 while True wait when True sync exit_2 goto obs_waiting when True sync enter 1 goto obs violation NOTE no outgoing action to reduce state space loc obs violation while True wait end observer Cee ARIA C REOR ORAE ER ER EE e o ee HOOK e RR e Initial state ee ae e fe ae ae EEE SES SIRET AF A A E AF A ICICI fe A A AF ICI IGG AC Ca a ata aca a init INITIAL LOCATION amp loc procl idlel amp loc proc2 idle2 amp loc observer obs waiting e INITIAL CLOCKS amp xl gt 0 amp x2 gt 0 e INITIAL DISCRETE amp turn IDLE amp counter 0 e PARAMETER CONSTRAINTS amp delta gt 0 am
6. Installation 22 6646 ey Ry oro ox E Ro Gee a 7 List of Options 13 13 13 14 15 16 16 17 17 19 19 19 20 21 21 22 23 23 23 24 24 25 25 25 26 27 8 Grammar 8 1 VariableNames 8 2 Grammar of the Input File 8 2 1 Automata Descriptions 8 2 2 Initial State 8 3 Grammar of the Reference Valuation File 8 4 Grammar of the Reference Hyperrectangle File 85 Reserved Words 9 Missing Features 9 1 ASAP Transitions o re 9 2 Parameterized Models 9 3 Other Synchronization Models 9 4 Intervals for Discrete Variables 9 5 Complex Updates for Discrete Variables 10 Acknowledgments 11 Licensing and Credits References 33 33 33 34 37 38 39 39 40 40 40 41 41 41 42 43 45 Chapter 1 Introduction IMITATOR is an open source software tool to perform automated parameter synthesis for concurrent timed systems AFKS12 IMITATOR takes as input a network of IMITATOR parametric timed automata NIPTA NIPTA are an exten sion of parametric timed automata AHV93 a well known formalism to specify and verify models of systems where timing constants can be replaced with pa rameters i e unknown constants IMITATOR addresses several variants of the following problem given a concurrent timed system what are the values of the timing constants that guarantee that the model of the system satisfies
7. editors Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems FORMATS 15 volume 9268 of Lecture Notes in Computer Science pages 27 43 Springer September 2015 4 21 tienne Andr Dynamic clock elimination in parametric timed automata In Christine Choppy and Jun Sun editors Ist 46 And13b AS13 BHZ08 HHWT95 IMI15 JLR15 JM09 LPY97 SLDP09 French Singaporean Workshop on Formal Methods and Applica tions FSFMA 13 volume 31 of OpenAccess Series in Informatics OASIcs pages 18 31 Schloss Dagstuhl Leibniz Zentrum f r In formatik Dagstuhl Publishing July 2013 28 tienne Andr Observer patterns for real time systems In Yang Liu and Andrew Martin editors 18th IEEE International Confer ence on Engineering of Complex Computer Systems ICECCS 13 pages 125 134 IEEE Computer Society July 2013 20 21 tienne Andr and Romain Soulat The Inverse Method ISTE Ltd and John Wiley amp Sons Inc 2013 176 pages 28 R Bagnara P M Hill and E Zaffanella The Parma Polyhedra Library Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems Sci ence of Computer Programming 72 1 2 3 21 2008 25 Thomas A Henzinger Pei Hsin Ho and Howard Wong Toi A user guide to HyTech In Ed Brinksma Rance Cleaveland Kim Guld strand Larsen Tiziana Margaria and Bernhard Steffen
8. in a graphical form option output trace set output the constraints synthesized in a graphical form in two dimensions option output cart or output the result to a text file op tion output result The option step specifies the interval between any two points of which the coverage is checked see AF10 By default it is 1 setting i often leads to full coverage when 1 was not enough Behavioral Cartography with Random Coverage An alternative to the behavioral cartography is a random coverage it can be seen as a kind of sampling The command is imitator model imi model vO mode randomXX where XX is the number of times an integer point is randomly selected within the domain defined in model v0 If this point is already covered by one of the tiles the inverse method is not called an another point is selected Note that XX represents the number of integer points randomly selected the number of calls to the inverse method can be significantly smaller 4 6 Parametric Reachability Preservation IMITATOR implements an algorithm solving the following problem given a reference parameter valuation v and some location l synthesize other valua tions that preserve the reachability of By preserving the reachability we mean that Lis reachable for the other valuations iff l is reachable for v This algorithm PRP that combines EFsynth and IM see ALNS15 for de tails is called as follows imitator model imi m
9. it is useful and readable mostly for very small trace sets PRP default false Option used to activate PRP or PRPC ALNS15 These options must be used in addition to the mode option That is in order to call PRP use imitator model imi model piO PRP And in order to call PRPC use imitator model imi model vO mode cover PRP PTA2GrML default false Translates the input model to a GrML format used by CosyVerif AHHH 13 and exits PTA2JPG default false Translates the input model to a graphical human readable form in jpg format and exits PTA2TikZ default false Translates the input model to a BIFX representation of the model using the tikz package without performing any analysis and exits Note that node positioning is not much supported so may want to edit manually some positions states limit default none Will try to stop after reaching this number of states Warning the program may have to first finish computing the current it eration i e the exploration of the state space at the current depth before stop ping statistics default false Print info on number of calls to PPL and other statistics about memory and time Warning enabling this option may slightly slow down the analysis and will certainly induce some extra computational time at the end 31 step default 1 Step for the behavioral cartography Integers can be used or rationals in the form x y
10. parameters are bound to be positive or null this is not assumed by default by IMITATOR so users are strongly advised to add this constraint Note that the initial definition can introduce more complex constraints on clocks parameters and discrete variables see Section 3 3 for details 3This observer is not really necessary to check the correctness of this protocol instead of adding this observer and checking unreachable loc observer obs violation one could just check either counter gt 1 orloc proci CS1 amp loc proc2 CS2 However IMITATOR does not yet support checking global variables or more that one location in the unreachable property which should be fixed very soon furthermore introducing an observer is also useful as it is often used for verification 11 Property specification In this model the correctness property is that two pro cesses cannot be in the critical section at the same time as explained above this is equivalent to the fact that the obs violation location of the observer IPTA is unreachable This is input in the model as follows property unreachable loc observer obs violation More elaborate properties are detailed in Section 4 3 however they all reduce to reachability so more complex properties such as B chi like properties or fair ness are not yet supported by IMITATOR Parameter synthesis Finally let us run IMITATOR on this case study Quite naturally what we would be int
11. the case of BC This option makes use of the external utility graph which is part ofthe GNU plotting utils available on most Linux platforms The generated files will be lo cated in the same directory as the source files unless option output prefix is used 29 Additional useful options are output cart x min output cart x max output cart y min output cart y max to tune the values of the axes and output graphics source to keep the plot source output cart x min default off Set minimum value for the x axis when plotting the cartography not entirely functional in all situations yet output cart x max default off Set maximum value for the x axis when plotting the cartography not entirely functional in all situations yet output cart y min default off Set minimum value for the y axis when plotting the cartography not entirely functional in all situations yet output cart y max default off Set maximum value for the y axis when plotting the cartography not entirely functional in all situations yet output graphics source default false Keep file s used for generating graphical output e g trace set cartography these files are otherwise deleted after the generation of the graphics output prefix default lt input_file gt Setthe path prefix for all generated files The path can be either relative to the path to the imitator binary or absolute and must be followed by the file name Examp
12. the way IMITATOR works The admis sible values for verbose are given below mute No output the result can be output to a file using output result warnings Prints only warnings standard Give little information number of steps computation time low Give little additional information medium Give quite alot of information high Give much information total Give really too much information version Prints IMITATOR header including the version number and exits lIn such a case action label is actually completely removed before the execution in order to optimize the execution and the user is warned of this removal 32 Chapter 8 Grammar 8 1 Variable Names A variable name represented by lt name gt in the grammar below is a string start ing with a letter small or capital and followed by a set of letters digits and un derscores _ By letter we mean the 26 letters of the Latin alphabet without any diacritic mark The set of clock names parameter names and discrete variable names must quite naturally be disjoint However the sets of IPTA names location names action names and variable names are not required to be disjoint That is the same name can be given to a clock an automaton an action and a location Furthermore the names of the sets of locations of various IPTA are not necessarily disjoint either that is a same name can be given to two different locations in two different IPTA and they stil
13. IMITATOR User Manual Version 2 7 1 Butter Gu m n Build 1245 July 27 2015 www imitator fr o9 Contents Tableofcontenis s ess ox 39 o XUR Eo vow v 9k wey X 0e X xod e 4 1 Introduction 2 A Brief Introduction to the Syntax 3 IMITATOR Parametric Timed Automata 3 1 Bormal Definition lt du dus owe Bode ae om 3 1 1 Linear Constraints o s e a ace ae Lee Ra 3 1 2 IMITATOR Parametric Timed Automata 3 1 3 Networks of IMITATOR Parametric Timed Automata 3 2 Discrete Variables lt lt 29cm oo 4 RR Rod 3 3 Initial State and Initialization of Variables 3 4 Synchronization Model 3 5 Constants co ocs 4 24 405 8B etes BER eR E Lu 4 Parameter Synthesis Using IMITATOR 4 1 State Space Computation s 4 4 4 e pea den a x s 4 2 EF Synthesis s so ee e PPG ae coq Re EX Er a 4 3 Parametric Verification using Properties 4 4 Inverse Method Trace Preservation 4 5 Behavioral Cartography 4 6 Parametric Reachability Preservation 5 Graphical Output and Translation Sil JIGCESBE cuo Boh is RE S Rb de a Shah A 5 2 Constraints and Cartography So Exportto JPEG wc 52 pin d manu Ro EUR 5 1 Expono DES auos aoe SM aoe Le Ur AURAS RATS 6 Inside the Box 6 1 Language and Libraries gt o 64 cos ee a ae OA ee Ex 62 Symbolic States n eee aaa we we om om a E 6 3
14. ame gt then eventually lt name gt once before next lt name gt within linear_expression then lt name gt happened within linear_expression before lt name gt then lt name gt happened within linear_expression before lt name gt then lt name gt happened once within linear_expression before then eventually lt name gt within linear_expression lt name gt then eventually lt name gt within linear_expression lt name gt then eventually lt name gt within linear_expression once before next sequence var_list sequence always var_list 8 3 Grammar of the Reference Valuation File The reference valuation file usually named model pi0 gives a constant value to any parameter of the model this file is used for IM and PRP It basically consists of a sequence of equalities parameter constant sep arated or not by the amp symbol All parameters of the model must be given a valuation in this file but the file may also use names that do not appear in the model a warning will just be issued Arithmetic expressions using integers and rationals can even be used in stead of just constants 38 8 4 Grammar of the Reference Hyperrectangle File The hyperrectangle file usually named model v0 defines a bounded parame ter domain i e a hyperrectangle having as dimensions the parameters of the model this file is used for BC and PRPC It basically consists of a sequence of either equalities parameter
15. and Romain Soulat Merge and conquer State merging in parametric timed automata In Dang Van Hung and Mizuhito Ogawa editors Proceedings of the 11th In ternational Symposium on Automated Technology for Verification and Analysis ATVA 13 volume 8172 of Lecture Notes in Computer Science pages 381 396 Springer October 2013 12 29 42 tienne Andr Lom Messan Hillah Francis Hulin Hubard Fab rice Kordon Yousra Lembachar Alban Linard and Laure Petrucci CosyVerif An open source extensible verification environment In Yang Liu and Andrew Martin editors 18th IEEE International Con ference on Engineering of Complex Computer Systems ICECCS 13 pages 33 36 IEEE Computer Society July 2013 4 28 31 Rajeev Alur Thomas A Henzinger and Moshe Y Vardi Parametric real time reasoning In Proceedings of the twenty fifth annual ACM symposium on Theory of computing STOC 93 pages 592 601 New York NY USA 1993 ACM 4 5 13 20 tienne Andr Giuseppe Lipari Hoang Gia Nguyen and Youcheng Sun Reachability preservation based parameter synthe sis for timed automata In Klaus Havelund Gerard Holzmann and Rajeev Joshi editors Proceedings of the 7th NASA Formal Methods Symposium NFM 15 volume 9058 of Lecture Notes in Computer Science pages 50 65 Springer April 2015 4 22 31 tienne Andr and Nicolas Markey Language preservation prob lems in parametric timed automata In Sriram Sankaranarayanan and Enrico Vicario
16. ansition 9 4 Intervals for Discrete Variables Discrete variables must be set to a constant integer in the init definition e g i 0 Setting a variable to an arbitrarily value eg i in 0 10 iscur rently not supported This can be simulated using an initialization IPTA that nondeterministically sets i to any of the values in 0 time so as to not disturb the model 9 5 Complex Updates for Discrete Variables So far discrete variables can only be set to linear terms in ZF D hence as signing a discrete variable to a clock or to a parameter or to any more complex expression is not allowed A reason for this restriction is that the value of the discrete variables would not anymore be constant recall that discrete variables are syntactic sugar for locations However this can be partially simulated with stopwatches we can replace a discrete variable with a clock that is stopped in all locations i e it does not evolve with time and that is updated to the desired value recall from Defi nition 1 that the clock updates are more permissive than the discrete variable updates 41 Chapter 10 Acknowledgments Etienne Andr initiated the development of IMITATOR in 2008 and keeps de veloping it Emmanuelle Encrenaz and Laurent Fribourg have been great sup porters of IMITATOR on a theoretical point of view and to find applications both from the literature and real case studies Abdelrezzak Bara provided sev eral e
17. cal section then process 1 is indeed ready to enter the critical section by synchro nizing access 1 and resetting x1 If turn is different from 1 that is another An empty model template with all these comments ready to be filled out containing also a sample IPTA and its initial definitions is available at https github com etienneandre imitator blob master examples model imi turn IDLE try 1 xt xl lt delta update 1 x1 0 turn 1 turn 1 exit 1 Axl gt gamma xl 0 no access 1 counter counter 1 x1 0 turn IDLE xl gt gamma tum 1 access 1l x1 0 enter 1l counter counter 1 a Process 1 exit 1 exit 2 enter 1 enter 2 enter 1l b PTA observer Figure 2 1 Fischer mutual exclusion protocol 10 process attempted in the meanwhile to enter the critical section and it is not safe for process 1 to enter then process 1 returns to its idle location by synchro nizing no access 1 and resetting x1 Note that we have to use two transitions checking that either turn lt 1 or turn gt 1 to compensate that the different from operator 7 is not yet supported by IMITATOR In location accessi process 1 can remain any time and eventually enters the critical section by synchronizing enter 1 and incrementing the global vari able counter by 1 In location C 1 process 1 can remain any time and eventually leaves it b
18. constant or intervals parameter constant constant separated or not by the amp symbol All parameters of the model must be given an interval possibly punctual in this file again the file may also use names that do not appear in the model a warning will just be issued Again arithmetic expressions using integers and rationals can even be used instead of just constants 8 5 Reserved Words The following words are reserved keywords and cannot be used as names for automata variables actions or locations always and automaton bad before carto clock constant discrete do end eventually everytime False goto happened has if init initially loc locations next not once or parameter projectresult property region sequence stop sync synclabs then True unreachable urgent var wait when while within 39 Chapter 9 Missing Features Although we try to make IMITATOR as complete as possible it misses some features not implemented due to lack of time contributors are welcome or due to complexity or to keep the tool consistent We enumerate in the following what seems to us to be the most missing features and when applicable we give hints to overcome these limitations 9 1 ASAP Transitions ASAP as soon as possible transitions are transitions that can be taken as soon as all IPTA synchronizing with this transition can execute their local transition This is different from urgent trans
19. d algorithms such as the inverse method and the cartography on the other hand However many correctness properties can be encoded using reach ability using observers see ABL98 ABBL98 And13b Encoding observers can be done manually using ad hoc IPTA or using pre defined correctness properties commonly met in the literature If using a predefined property the property must be specified as follows at the end of the model after the initial state definition property PROP PROP must conform to one of the following patterns where AUTOMATON is an automaton name LOCATION is a location name a a1 a2 are actions and the deadline d is a possibly parametric linear expression property unreachable loc AUTOMATON LOCATION property if a2 then ai has happened before property everytime a2 then ai has happened before property everytime a2 then ai has happened once before property a within d property if a2 then ai has happened within d before property everytime a2 then ai has happened within d before property everytime a2 then al has happened once within d before 20 property if ai then eventually a2 within d e property everytime ai then eventually a2 within d e property if ai then eventually a2 within d once before next property sequence al an property always sequence al an The semantics of these properties is detailed in And13b Then the comma
20. del is bounded in IMITATOR by some very large num ber most probably 2 but well you don t seriously plan to build such a large model do you 3 2 Discrete Variables Discrete variables are global integer valued variables Their value is global in the sense that they are shared by all IPTA of the model They can be seen as syntactic sugar to represent a possibly unbounded number of locations In IMITAT OR integers are exact and unbounded just as in maths i e they are not represented using a limited number of bits such as 32 or 64 bits Hence no overflow can occur and the representation of the constraints is always exact Note that floating point numbers are totally absent from the IMITATOR imple mentation except for th generation of graphical outputs Discrete variables must be initialized to a single constant value in the init definition if they are not a warning is issued and they are arbitrarily set to 0 Discrete variables can be tested in guards and updated along transitions They are first tested then updated If two IPTA in parallel update the same vari able on the same synchronized transition e g an IPTA performs i 2 while another one performs i 3 then a warning is issued and the behavior of the NIPTA becomes unspecified i e IMITATOR will choose one or the other assignment in a non deterministic manner 3 3 Initial State and Initialization of Variables For each IPTA a unique initial location mus
21. ection this variable will not be used for the verification but was used in the original PAT model and we choose to keep it Finally a global constant IDLE is set to 1 just as in the original PAT model and encodes that no process is attempting to enter the critical section Automata This model contains three IPTA the first and second ones proci and proc2 model the first and second process respectively The third one observer is an observer i e an IPTA that checks the system behavior with out modifying it The first process Let us first describe the IPTA proci a graphical represen tation is given in Fig 2 1a This IPTA uses six actions given in the synclabs declaration proci is initially in location idlei with no invariant depicted by while True wait At any time when the discrete variable turn is equal to IDLE then this IPTA may synchronize on action try 1 reset its clock x1 and enter location activel The invariant of this location is x1 lt delta ie proci can only remain in activei as long as the value of x1 does not exceed delta At any time this IPTA may synchronize on action update 1 reset its clock x1 and set the global variable turn to 1 and enter location check1 In location check1 the process wait at least gamma time units modeled by the inequality x1 gt gamma in all outgoing transitions If turn is still equal to 1 that is no other process attempted in the meanwhile to enter the criti
22. ef png if the algorithm is EFsynth model cart bc png if the algorithm is BC and its variant or model cart patator png if the algorithm is the distributed BC and its variants The 2 dimensions chosen for the plot are the first two non constant pa rameter dimension in the model Additional useful options are output cart x min output cart x max output cart y min output cart y max to tune the values ofthe axes and output graphics source to keep the plot source The graphical output of the constraint is not yet available for the inverse method 23 5 3 Export to JPEG To generate a graphic representation of the model without performing any anal ysis use imitator model imi PTA2JPG IMITATOR will generate a file model pta jpg 5 4 Export to TEX To generate a BIEX representation of the model using the tikz package with out performing any analysis use imitator model imi PTA2TikZ IMITATOR will generate a file model tex This file is a standalone BIFX file containing a single figure which contains the different IPTA in subfigure en vironments The node positioning is not yet supported locations are depicted vertically so you may need to manually position all nodes and bend some tran sitions if needed 24 Chapter 6 Inside the Box 6 1 Language and Libraries In short IMITATOR is written in OCaml and contains about 26 000 lines of code IMITATOR makes use of the following external lib
23. er float integer pos integer 36 integer pos_integer pos integer pos integer int float pos float pos float pos float float 8 2 2 Initial State init init declaration init definition property definition projection definition other commands init declaration var init region other commands end rest of commands rest of commands anything rest of commands anything 2 lt name gt init bad init definition init region expression region expression amp region expression fol region expression fol 37 region_expression_fol state_predicate C region expression fol region expression fol amp region expression fol state predicate loc lt name gt lt name gt linear constraint loc predicate loc lt name gt lt name gt property_definition property pattern pattern unreachable loc_predicate if lt name gt everytime everytime if lt name gt everytime everytime if lt name gt everytime everytime if lt name gt everytime everytime then lt name gt has happened before lt name gt then lt name gt has happened before lt name gt then lt name gt has happened once before then eventually lt name gt lt name gt then eventually lt name gt lt n
24. erested in is knowing for which parameter valua tions this protocol is correct i e no more than one process can be present in the critical section at one time Assuming this model is input in file fischer imi the command calling IMITATOR is as follows imitator fischer imi mode EF merge In this command mode EF calls the algorithm EFsynth that synthesizes valuations reaching a given location see Section 4 2 and merge is a merg ing technique reducing the state space that for this model ensures termination see AFS13 for more details on merging The result of the call to IMITATOR is Final constraint such that the property is violated 1 constraint delta gt gamma amp gamma gt 0 That is the system is safe if delta gamma which is the well known con straint ensuring mutual exclusion for this protocol 12 Chapter 3 IMITATOR Parametric Timed Automata 3 1 Formal Definition IMITATOR performs parametric verification of models specified using networks of IMITATOR parametric timed automata hereafter NIPTA An IMITATOR parametric timed automaton hereafter IPTA is a variant of parametric automata as introduced in AHV93 A first difference between IPTA and the PTA of AHV93 is that IPTA have no accepting final location fur thermore IPTA augment the expressiveness of PTA with several features such as invariants discrete integer variables complex guards and invariants i e not on
25. following expression can be used in a guard or an invariant ii 5 xi 3 x2 gt 2 pi i2 amp p2 lt 1 3 where i1 i2 are discrete variables x1 x2 are clocks and p1 p2 are parameters This syntax includes in particular diagonal constraints e g xi x2 lt 2 not always supported in other model checking tools Actions Transitions can be synchronized on an action in 2 or have no syn chronized action e which is often referred to in the literature as a silent transition or an e transition For the semantics of the synchronization model between various IPTA refer to Section 3 4 Clock updates Observe that clocks can be updated to any value i e a clock can be assigned not only to 0 but to any linear term over the other clocks the parameters and the discrete variables However discrete variables can only be assigned to a linear term over D including a constant If clocks are always reset i e not assigned to more complex linear terms IMITATOR will apply some optimizations that may increase the analysis speed Stopwatches There are no distinction between clocks and stopwatches That is any clock can potentially be stopped in some location IMITATOR will de tect whether a model has or not stopwatches if there is no stopwatch in some model IMITATOR will apply some optimizations that may increase the analy sis speed 3 1 3 Networks of IMITATOR Parametric Timed Automata Definition 2 NIPTA Given a
26. itions that must be taken in 0 time Here time can elapse but not after all IPTA are ready to execute their local transition This is not supported by IMITATOR and we do not see a way to simulate it easily in the current implementation 9 2 Parameterized Models Parameterized models are understood here as models with an arbitrary number of components e g Fischer s mutual exclusion protocol with n processes that would be instantiated e g n 15 before performing the analysis IMITATOR does not currently support such parameterized models and one should use copy paste utilities to instantiate n models For complicated models with many processes we usually write short scripts to generate the model a script CSMACDgenerator py to model the varying part of parameterized models for the CSMA CD case study is available on GitHub 40 9 3 Other Synchronization Models One to one synchronization could possibly be simulated by using as many tran sitions as pairs of IPTA in the model although this may make the model rather complex Broadcast synchronization only the IPTA ready to execute a given transi tion execute it is not supported Once more it could possibly be simulated by using as many transitions as subsets of IPTA in the model although this will make the model definitely complex Message passing is not supported This can be easily simulated using dedi cated discrete variables that would be read written in the tr
27. key svg by KaterBegemot on Wikimedia Commons License Creative Commons Attribution Share Alike 3 0 Unported https commons wikimedia org wiki File Typing monkey svg IMITATOR s 2 7 version logo comes from Andouille Scheiben jpg by Pwagenblast on Wikimedia Commons License Creative Commons Attribution 3 0 Unported The background erasing was done by Fabrice Kordon https commons wikimedia org wiki File Andouille Scheiben Jpg 44 Bibliography ABBL98 ABL98 ACE14 ACEF09 ACHH93 ACN15 AF10 Luca Aceto Patricia Bouyer Augusto Burguefio and Kim Guld strand Larsen The power of reachability testing for timed au tomata In Vikraman Arvind and Ramaswamy Ramanujam ed itors FSTTCS 98 volume 1530 of Lecture Notes in Computer Sci ence pages 245 256 Springer 1998 20 Luca Aceto Augusto Burguefio and Kim G Larsen Model check ing via reachability testing for timed automata In Bernhard Stef fen editor TACAS 98 volume 1384 of Lecture Notes in Computer Science pages 263 280 Springer 1998 20 tienne Andr Camille Coti and Sami Evangelista Distributed behavioral cartography of timed automata In Jack Dongarra Yu taka Ishikawa and Hori Atsushi editors 21st European MPI Users Group Meeting EuroMPI ASIA 14 pages 109 114 ACM Septem ber 2014 28 Etienne Andr Thomas Chatain Emmanuelle Encrenaz and Lau rent Fribourg An inverse method for parametric timed au tomata
28. l represent two different things 8 2 Grammar of the Input File The IMITATOR input model 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 but allows some backward compatibility with HYTECH files HHWT95 imitator input automata descriptions init We define each of those two components below 33 8 2 1 Automata Descriptions automata_descriptions declarations automata declarations var var_lists var lists var list var type var lists var list name lt name gt rational name var list name rational var list var type clock discrete parameter automata automaton automata automaton automaton lt name gt prolog locations end prolog initialization sync labels sync labels initialization sync labels initialization initialization initially lt name gt state_initialization state_initialization amp convex_predicate sync labels synclabs name list 34 name list name nonempt
29. les e output prefix log output prefix log output prefix home imitator outputs output result default false Writes the result of the analysis to a file named input file result output states default false Generates a file input file states de scribing the reachable states in plain text value of the location of the discrete variables associated constraint and its projection onto the parameters output trace set default false Graphical output using dot In this case IMITATOR outputs a file lt input_file gt jpg which is a graphical output in the jpg format generated using dot corresponding to the trace set Note that the path and the name of those two files can be changed using the log prefix option 30 output trace set nodetails default false In the graphical output of the trace set see option output trace set does not provide detailed infor mation on the local locations of the composed IPTA and instead only outputs the state id Enabling this option may yield a smaller graph which is useful when generating large trace sets output trace set verbose default false In the graphical output of the trace set see option output trace set provides very detailed information by adding to the right of the local locations of the composed IPTA the associ ated constraint as well In addition the parametric constraint is printed too Enabling this option will yield a very large graph and
30. ly comparing a single clock to a single parameter stopwatches i e the abil ity to stop some clocks in some locations and arbitrary clock updates i e not necessarily to 0 3 1 1 Linear Constraints Clocks Parameters Discrete Variables Clocks are real valued variables all evolving at the same rate unless they are stopped which is allowed in IMITATOR A set of clocks is X x1 xH a clock valuation is w X Ryo Parameters are rational valued variables that act as unknown constants A set of parameters is P pi Pm a parameter valuation is a function v P gt R We will often identify a valuation v with the point v pi v pM Discrete variables are integer valued variables A set of discrete variables is D d dy a discrete variable valuation is a function D N Linear Constraints Let us formalize the set of linear constraints allowed in IMITATOR Given a set of variables Var z1 zn in the following this set will be instantiated with X and or P and or D a linear term over Var is an ex 13 pression of the form DE izi d l lt i lt n for some n N where z Var x Q for 1 lt i lt n and dEQ An atomic constraint over Var is an expression of the form t lt 0 where It is a linear term over Var and lt lt gt A constraint over Var is a conjunction of atomic constraints We denote by Var the set of linear terms over Var and by 7 Var the set
31. nd suffices when one wants to check the non reachability of a given bad state merge default false Use the merging technique of AFS13 This option is safe and advised for the EFsynth algorithm However not all the properties of the inverse method are preserved when using merging see AFS13 for details mode default inversemethod The mode for IMITATOR statespace Generation of the entire parametric state space see Section 4 1 EF Parametric non reachability analysis EFsynth JLR15 see Section 4 2 inversemethod Inverse method see Section 4 4 cover Behavioral Cartography Algorithm with full coverage see Section 4 5 randomXX Behavioral Cartography Algorithm with XX iterations see Section 4 5 no random default false In the inverse method no random selection of the 7 o incompatible inequality select the first found By default select an inequal ity in a random manner output cart default off After execution of the behavioral cartography or EFsynth plots the generated zones as a png file This will generate file model cart ef png if the algorithm is EFsynth model cart bc png if the al gorithm is BC and its variant or model_cart_patator png if the algorithm is the distributed BC and its variants If the model contains more than two param eters then output cart will plot the projection of the generated zones on the first two parameters of the model or on the two varying parameters in
32. nd to synthesize parameters is the same as for the EF synthesis imitator model imi mode EFsynth merge incl 4 4 Inverse Method Trace Preservation Given a NIPTA and a reference parameter valuation the inverse method IM synthesizes a parameter constraint such that for any parameter valuation in that constraint the set of traces is the same as for the reference valua tion ACEF09 This problem is known as the trace preservation synthesis The trace preservation emptiness problem being undecidable AM 15 the analysis is not guaranteed to terminate although it often does in practice The command is imitator model imi model piO The reference valuation is described in model pi0 IMITATOR can also output the trace set in a graphical form op tion output trace set or output the result to a text file option output result 4 5 Behavioral Cartography Given a NIPTA and a bounded parameter domain the behavioral cartogra phy BC synthesizes tiles i e parameter domains such that for any parameter valuation in that domain the set of traces is the same AF10 The corresponding problem being undecidable the analysis is not guaranteed to terminate when it terminates it may also leave holes i e parameter domains not covered by any tile The command is imitator model imi model vO mode cover The bounded parameter domain is described in model vo 21 IMITATOR can also output all trace sets
33. ns The options available for IMITATOR are explained in the following Note that some more options are available in the current implementation of IMITATOR If these options are not listed here they are experimental or deprecated If needed more information can be obtained by contacting the IMITATOR team acyclic default false Does nottestifa new state was already encountered Without this option when IMITATOR 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 consequence 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 will compute twice the states after the state common to the two traces As a consequence 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 check ippta default false Check that every new symbolic state contains an integer point i e a point in the XUP dimension If not raises an exception check point default false In the inverse method checks a
34. odel pi0 PRP Note that a bad location as in Section 4 2 or a property as in Section 4 3 must be defined in the model Parametric Reachability Preservation Cartography An extension of PRP to the cartography named PRPC is also available PRPC synthesizes parameter constraints in which the non reachability of l is uni form PRPC was showed in ALNS15 to be a good alternative to EFsynth espe cially when distributed This algorithm PRPC is called as follows imitator model imi model vO mode cover PRP Again a bad location as in Section 4 2 or a property as in Section 4 3 must be defined in the model 22 Chapter 5 Graphical Output and Translation Again we only give the most useful options For more detailed commands and a complete list of options see Chapter 7 5 1 Trace Set To generate the trace set of a given computation in a graphical form use imitator model imi options output trace set IMITATOR will generate a file model jpg Note that beyond about 1 000 states or 1 000 transitions the dot utility responsible to generate the trace set may crash Using output trace set nodetails makes a more compact representa tion but is also less informative 5 2 Constraints and Cartography To generate the constraint generated by IMITATOR in a 2 dimensional plot us ing the plot utility use imitator model imi options output cart This will generate file model cart
35. of constraints over Var In IMITATOR we will consider constraints belonging to sets such as 5 XU P i e the set of constraints over clocks and parameters or 26 XU PUD ie the set of constraints over clocks parameters and discrete variables 3 1 2 IMITATOR Parametric Timed Automata We can now give a formal definition of IPTA Let e denote the unobservable action Definition 1 IPTA An IMITATOR parametric timed automaton IPTA is a tu ple 4 X L linit D X P L S 5 where Lisa finite set of actions L is a finite set of locations linit L is the initial location D is a set of integer valued variables X is a set of clocks P is a set of parameters e I L gt Z XUPUDJ assigns to every location a constraint over all variables called the invariant ofl e S L X assigns to a every location a list of clocks that are stopped in this location e isa set of edges l g a Xup Dup VU where l l L are the source and destination locations g XUPUD isa constraint over all variables called guard of the transition a X Ue is the action associated with the transition Xup X LT XUPUD is the update function for clocks and Dup D gt ZT D is the update function for discrete variables In the following we explain this definition 14 Guards and invariants Guards and invariants in IMITATOR are linear con straints over all variables For example the
36. ollowed by some manual positioning optimization 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 No lt gt operator hence we use both gt and x when xl gt gamma amp turn lt 1 sync no access 1 do xl 0 goto idlel when xl gt gamma amp turn gt 1 sync no access 1 do xl 0 goto idlel loc accessl while True wait when True sync enter 1 do counter counter 1 goto CSI loc CSI while True wait when True sync exit 1 do counter counter 1 turn IDLE xl 0 goto idlel end procl automaton proc2 synclabs access 2 enter 2 exit 2 no access 2 try 2 update 2 loc idle2 while True wait when turn IDLE sync try 2 do x2 0 goto active2 loc active2 while x2 lt delta wait when True sync update 2 do turn 2 x2 0 goto check2 loc check2 while True wait when x2 gamma amp turn 2 sync access 2 do x2 0 goto access2 No lt gt operator hence we use both gt and x when x2 gt gamma amp turn 2 sync no access 2 do x2 0 goto idle2 when x2 gt gamma amp turn gt 2 sync no access 2 do x2 0 goto idle2 loc access2 while True wait when True sync enter 2 do counter counter 1 goto CS2 loc
37. p gamma gt 0 ok GCG GGG GR GR KR kk Kk Property specification ee ae e ae ae ae EEE SES SSI A AF A A E AF A A IGG GIGI AF A A AF A e fe AF ACC GaGa EEEE property unreachable loc observer obs_violation ee ae e e ae a e EEE SES SRE GI AR AF A FE A DE AF A ICICI AGC IGA aC Ca i ak akc aca ak The end ooo ee ok doe e OO OO KO e ok doe ef e AR Def e ICI E 3 ef e AF GIGI Cg ea e x end kj Header Letus comment this case model by starting with the header First text in comments gives generalities about the model author date description etc The form is not normalized but it could be in the future so it is strongly advised to follow this form Variable declarations The variable declarations starts with keyword var This model contains two clocks x1 is process 1 s clock and x2 is process 2 s clock This model contains two parameters delta is the parametric duration spec ifying how long a process is idle at most whereas gamma is the parametric dura tion specifying the minimum duration between the time a process checks for the availability of the critical section and the time the same process indeed enters the critical section if it is still available Two discrete variables i e global integer valued variables see Section 3 2 are used turn checks which process is attempting to enter the critical section counter records how many processes are in the critical s
38. point distribution ACN15 dynamic Master worker dynamic subdomain decomposition ACN 15 dynamic elimination default false Dynamic elimination of clocks that are known to not used in the future of the current state And13a fromGrML default false Does not use the standard input syntax described here but a GrML input syntax This is used when interfacing IMITATOR with the CosyVerif platform AHHH 13 Note that in that case not all syntactic features of IMITATOR are supported IMK default false Uses a variant of the inverse method that returns a con straint such that no 7tg compatible state is reached it does not guarantee how ever that any good state will be reached see AS13 IMunion default false Uses a variant of the inverse method that returns the union of the constraints associated to the last state of each path see AS13 28 incl default false Consider an inclusion of region instead of the equal ity when performing the Post operation In other terms when encountering a new state IMITATOR checks if the same state same location and same con straint has been encountered before and if so discards this new state How ever when the incl option is activated it suffices that a previous state with the same location and a constraint greater than 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 HYTECH works a
39. put syntax We give below this model using the IMITATOR syntax Note that this model is given in graphical form in Fig 2 1 Gk 9 a e RR SRR RRS ORO ORR OR ROR OOK OR KOK IMITATOR MODEL Fischer s mutual exclusion protocol Description Fischer s mutual exclusion protocol with 2 processes Correctness Not 2 processes together in the critical section location obs violation unreachable Source PAT library of benchmarks Author su Input by Etienne Andre Created 2012 10 08 Last modified 2015 07 20 IMITATOR version 2 7 beta4 CKETTTTTTETTTTTTTTTTTTTTTTTTTTTTTTTTTTITTTTTTTTTTTTTZTTTZTTED var xl procl s clock x2 proc2 s clock clock turn counter discrete delta gamma parameter IDLE 1 constant ee ae e OGG ICICI ICICI Fe A De e AF 3 A A ACC GaGa vCal a ak automaton procl Gk 9 ae e SRR ROSAS ROS ORR RRR OR ROKR ROKK RR kelee synclabs access 1 enter_1 exit 1 no_access_1 try 1 update 1 loc idlel while True wait when turn IDLE sync try 1 do xl 0 goto activel loc activel while xl lt delta wait when True sync update 1 do turn 1 xl 0 goto checkl loc checkl while True wait when xl gt gamma amp turn 1 sync access 1 do xl 0 goto accessl I This TEX representation that makes use of the ATX TikZ library was automatically output by IMITATOR using option PTA2TikZ f
40. raries The OCaml ExtLib library Extended Standard Library for Objective Caml The GNU Multiple Precision Arithmetic Library GMP The Parma Polyhedra Library PPL BHZ08 used to compute operations on polyhedra 6 2 Symbolic States Verification of timed systems and specially parametric timed systems is nec essarily done in a symbolic manner in the sense that the timing information is abstracted by clock constraints However IMITATOR does not perform what is referred to as symbolic model checking in other words the representation of lo cations in IMITATOR is explicit and not symbolic using e g binary decision diagrams In short a symbolic state in IMITAT OR is made of the following elements e the current location index of each IPTA the current value of the integer valued discrete variables aconstraint on XU PU D representing the continuous information In IMITATOR all integers i e the value of the discrete variables and the co efficients used in the constraints are unbounded integers implemented using GMP 25 6 3 Installation This document does not aim at explaining how to install IMITATOR See the installation information available on the website for the most up to date infor mation Binaries and source code packages are available on IMITATOR s Web page IMI15 Several standalone binaries are provided for Linux systems that require no installation 26 Chapter 7 List of Optio
41. set of IPTA A Li Li Uni Di Xi Pi li Si di 1 si lt N for some N N a network of IPTA NIPTA is a tuple D X P 4 1 si lt N Cinit where e X Ui lt ign Zi is the set of all actions e D Uusien Di is the set of all discrete variables e X Ui lt ign Xi is the set of all clocks Pel 1 i N Pi is the set of all parameters Cni LE XUPUD is the initial constraint over D X and P 15 Observe that each set of actions discrete variables clocks and parameters is not disjoint between all IPTA That is actions discrete variables clocks and parameters may be shared between different IPTA If a variable is required to be local to an IPTA then it should just not be used in any other IPTA of the model Different from many tools for parametric timed automata clocks are not necessarily initially equal to 0 this is similar to HYTECH HHWT95 but different from UPPAAL LPY97 The initial value of the clocks is defined by Cinit see Section 3 3 If nothing is defined in Cjnit then their value is supposed to be arbitrary any real value greater or equal to 0 Note that parameters are not assumed positive however the behavior of IMITATOR has not been tested for negative parameters and it is strongly ad vised to constrain them to be positive in Cinit if it is not the case a warning is issued by IMITATOR Finally note that the number of IPTA locations variables and actions that can be defined in a mo
42. some property Specifically IMITATOR implements parametric safety analysis AHV93 JLR15 the inverse method ACEF09 AM15 the behavioral cartography AF10 and parametric reachability preservation ALNS15 Some algorithms can also run distributed on a cluster Numerous analysis options are available IMITATOR is a command line only tool but that can output results in graphical form Furthermore a graphical user interface is available in the CosyVerif platform AHHH 13 IMITATOR was able to verify numerous case studies from the literature and from the industry such as communication protocols hardware asynchronous circuits schedulability problems and various other systems such as coffee ma chines probably the most critical systems from a researcher point of view Nu merous benchmarks are available at IMITATOR Web page IMI15 In this document we present the input syntax we formally define the input model of IMITATOR and we explain how to perform various analyses using the numerous options Keywords formal verification model checking software verification param eter synthesis Chapter 2 A Brief Introduction to the Syntax We first briefly introduce the syntax using a simple example for readers famil iar with parametric timed automata and not interested in subtle details such as the synchronization model A formal and nearly exhaustive definition of IMITATOR parametric timed automata NIPTA can be found in Chap
43. states without this option IMITATOR will not output anything IMITATOR can also output the trace set in a graphical form using option output trace set 4 2 EF Synthesis A main problem in parametric timed automata is to compute the set of parame ter valuations for which some location for instance an error location is reach able The property must be specified as follows at the end of the model after the initial state definition property unreachable loc AUTOMATON LOCATION where AUTOMATON is an automaton name and LOCATION is a location name 19 The algorithm EFsynth implemented in IMITATOR is a basic breadth first procedure close to the one described in AHV93 JLR15 Of course the EF emptiness problem being undecidable AHV93 the analysis is not guaranteed to terminate The standard command is imitator model imi mode EFsynth merge incl The options merge and incl are optional but generally greatly increase the analysis efficiency and the termination The option dynamic elimination can also be used to reduce the state space IMITATOR can also output the trace set in a graphical form option output trace set output the constraint synthesized in a graphical form in two dimensions option output cart or output the result to a text file op tion output result 4 3 Parametric Verification using Properties IMITATOR basically only supports bad state reachability synthesis on the one hand an
44. t be defined IThe name discrete variable comes from HYTECH 16 For variables the definition of the initial value is very permissive in IMITATOR Clocks are not necessarily equal to 0 and parameters are not even necessarily positive Parameters and clocks can be initially bound by any linear constraint over parameters clocks and discrete variables That is we can define initial con straints such as Xi x2 lt 2 p1 00 5 p2 e However discrete variables must be initialized to a constant integer Given a discrete variable i if the definition of the initial state does not contain an equality of the formi followed by a linear term in ZF XUP U D then IMITATOR will assume that i is initially set to 0 and will issue a warning 3 4 Synchronization Model By default all IPTA of an IMITATOR model declare their set of actions The IMITATOR synchronization model is such that all IPTA declaring an action must synchronize together on this action This can be seen as a strong broadcast That is for a transition labeled with action a to be executed all IPTA declaring a must be ready to execute a locally Otherwise this transition cannot be taken yet If an IPTA declares an action a that is never used in this IPTA then action a will never be executed in the entire model 3 5 Constants IMITATOR supports global constants i e a variable the value of which is known once for all The syntax is the following one
45. t each iteration whether the accumulated parameter constraint is restricted to the reference pa rameter valuation Note that this option is not implemented as nicely as it could be and can hence turn very costly 27 completeIM default false Returns a complete result for the inverse method for deterministic PTA i e returns a conjunction of negations of convex param eter constraints The result may result in a large list of such constraints and may hence be complicated to interpret contributors Print the list of contributors and exits depth limit lt limit gt default none Limits the depth of the exploration of the state space In the cartography mode this option gives a limit to each call to the inverse method Setting depth limit guarantees the termination of any execution of IMITATOR but not necessarily the correctness of the algorithms distributed lt mode gt default not distributed Distributed version of the behavioral cartography Various distribution modes are possible no Non distributed mode default static Static domain decomposition ACN15 sequential Master worker scheme with sequential point distribution ACE14 randomXX Master worker scheme with random point distribution eg randon5 or random10 after XX successive unsuccessful attempts where the generated point is already covered the algorithm will switch to an exhaustive sequential iteration ACE14 shuffle Master worker scheme with shuffle
46. ter 3 The complete syntax is given in Chapter 8 Generalities IMITATOR performs parametric verification of models specified using networks of IMITATOR parametric timed automata hereafter NIPTA An IMITATOR parametric timed automaton hereafter IPTA is a variant of para metric automata as introduced in AHV93 IPTA and NIPTA are formalized in Section 3 1 The input syntax of IMITATOR is originally based on the syntax of HYTECH HHWT95 with several improvements Actually all standard HYTECH files describing only PTA and not more general systems like linear hybrid au tomata ACHH93 can be analyzed directly by IMITATOR sometimes with very minor changes Comments are OCaml like comments starting with and ending with As in OCaml comments can be nested The Fischer mutual exclusion protocol We use as a motivating example one timed version of the Fischer mutual exclusion protocol coming from the PAT model checker SLDP09 This version of the protocol is neither the most com plete nor the most simple we just use it here to introduce various aspects of the IMITATOR input syntax Fischer mutual exclusion protocol is a protocol that guarantees the mutual exclusion of several processes here two that want to access a shared resource called the critical section e wo N a 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 44 45 46 In
47. xamples from the hardware literature Jeremy Sproston provided examples from the probabilistic community Bertrand Jeannet has been of great help on the linking with Apron M09 in a previous version of IMITATOR Ulrich K hne made several important improvements to IMITATOR and linked the tool to PPL Daphne Dussaud implemented the graphical output of the behavioral car tography Romain Soulat implemented in part the merging technique AFS13 and brought several case studies Giuseppe Lipari and Sun Youcheng provided examples from the real time systems community and collaborated on several algorithms Camille Coti Sami Evangelista and Nguyen Hoang Gia worked on the distributed version of IMITATOR 42 Chapter 11 Licensing and Credits IMITATOR license IMITATOR is available under the GNU GPL license Contributors Free Software Free as in Freedom The following people contributed to the development of IMITATOR Etienne Andr Camille Coti Daphne Dussaud Sami Evangelista Ulrich K hne Nguyen Hoang Gia Romain Soulat 2008 2014 2010 2014 2010 2011 2014 2010 2013 The following people contributed to the compiling and packaging facilities Corentin Guillevic Sarah Hadbi Fabrice Kordon Alban Linard User Manual 2015 2015 2015 2014 This user manual is available under the Creative Commons CC BY SA license 43 GIO BY SA Graphics Credits IMITATOR s logo comes from Typing mon
48. y decrementing the global variable counter by 1 and setting the global variable turn to its initial value IDLE The second process Process 2 is identical to process 1 except that x1 is re placed with x2 and that the value of turn becomes 2 Theobserver The observer is in charge to check that no more than one process is in critical section at the same time This observer will detect that this situa tion happens if an action enter 1 is followed by an action enter 2 without an action exit 1 in between or symmetrically if an action enter 2 is followed by an action enter 1 without an action exit 2 in between Note that the ob server simply observes the system state and synchronizes on the actions used by proci and proc2 it does not use any clock nor variable A graphical representation of the IPTA observer is given in Fig 2 1b Initial definitions The initial state is defined the part of the file following init This part must contain the initial location of each IPTA For example loc proci idlei states that proc1 is initially in location idlet The initial definition may only may see Section 3 3 give an initial value to the clocks for example requiring them to be equal to some constant typically 0 Here clocks are only bound to be greater or equal to 0 The initial definition should assign a constant value to each discrete vari able here turn is initially equal to IDLE and counter is initially equal to 0 Finally
49. y list name nonempty list name name nonempty list name locations location locations locations loc name while convex predicate stop opt wait opt transitions urgent loc name while convex predicate stop opt wait opt transitions wait opt wait wait e stop opt stop name list Y transitions transition transitions transition when convex predicate update synchronization goto name update synchronization updates syn label updates syn label syn label updates updates do update list update list update nonempty list 35 update nonempty list update update nonempty list update update name linear expression syn label sync lt name gt convex_predicate amp convex_predicate_fol convex predicate fol convex predicate fol linear constraint amp convex predicate linear constraint linear constraint linear expression relop linear expression True False we gt linear_expression p linear term linear expression linear term linear expression linear term linear term rational rational name rational name lt name gt lt name gt C linear term rational integ
Download Pdf Manuals
Related Search