User's Manual of Flow - Software modeling and verification group
Contents
1. ptp p p p p p pal xir such that n is a positive integer x is a variable and r is a real number The priorities over the operators are shown in Table 2 In addition an unsafe set can be option ally specified after the reachability definition 4 unsafe set 7 prefix 3 2 polynomial constraints F I pi lt cl 2 p2 gt c2 infix 1 p3 in c3 c4 vee Table 2 Priorities of the opera E tors The set is defined by the conjunction of the user given polynomial constraints each of which is of the form p cor p in c1 c2 wherein p is a polynomial over the state variables c c1 c2 are constants and E lt gt After performing the reachability computation FLOw checks the intersection of the flowpipes and the unsafe set If no intersection is detected then the tool reports SAFE otherwise it reports UNKNOWN 2 2 Modeling language for hybrid systems In this section we present the model file of a collision avoidance maneuver of two aircraft at a fixed altitude 3 In the beginning both of the aircraft are in straight flight with a relative heading When the aircraft come too close that is the distance of them is blow a specified value the controller will make an instantaneous heading change of 90 on both of them and then the two aircraft will complete a 7 time semicircular arc flying Afterwards both aircraft make another 90 instantaneous heading change and resume their2. 1 57075 a2 a2 1 57075 s1 c1 63 cl si s2 c2 c2 s2 64 parallelotope aggregation x1 1 y1 1 x2 1 y2 1 65 66 start mode2 67 end mode3 68 guard z 3 1415 69 reset a1 a1 1 57075 a2 a2 1 57075 si c1 70 cl s1 s2 c2 c2 s2 71 parallelotope aggregation the template is auto selected 72 73 init 4y i 15 modei initial mode 76 17 x1 in 0 1 0 1 y1 in 0 1 0 1 c1 in 0 70710 0 70711 78 s1 in 0 70710 0 70711 a1 in 0 785374 0 785376 x2 in 9 9 10 1 79 y2 in 0 1 0 1 c2 in 0 70711 0 70710 s2 in 0 70710 0 70711 80 a2 in 2 35612 2 35613 z in 0 0 81 8 amp 2 8 amp 3 84 8 amp 5 unsafe set there is a collision in a mode 86 4 87 modet ge 89 xl x2 0 90 yi y2 0 91 92 mode2 93 4 94 x1 x2 0 95 yi y2 0 96 97 mode3 98 99 xi x2 100 yi y2 0 101 102 fo The starting position of the first aircraft is the region 0 1 0 1 x 0 1 0 1 in the coordinate map For the second aircraft the initial position is the region 9 9 10 1 x 0 1 0 1 The initial heading angle of the first aircraft is 7 and that of the second aircraft is rr There are at most two jumps in the hybrid automaton so we bound the jump depth by 2 max jumps 2 We set the time horizon 0 15 such that the system will definitely in mode 3 after 15 time units The octagon enclosures of
3. be determined by d linearly independent vectors the set of which is called template We give an example in Figure 5 The two flowpipes can be over approximated by a parallelotope with the template 1 0 7 0 1 7 or the template 1 1 7 1 1 7 It is obvious that the aggregation accuracy plays an important role in the subsequent flowpipe construction work FLOW provides the following options to select a template for a jump T x a template 1 0 7 0 1 7 b template 1 1 1 1 7 Figure 5 Example of flowpipe aggregation e Interval aggregation FLOW computes a box enclosure for the flowpipe union similar to the example shown in Figure 5 a The specification is interval aggregation e General parallelotopic aggregation Users may simply specify parallelotope aggregation then FLow will determine the template based on the mode invariant jump guard flow direction and so on Users are also allowed to provide some preferred vectors for a 3 dimensional example parallelotope aggregation x 1 y 1 z 2 wherein x 1 y 1 denotes the vector 1 1 0 in the state space and z 2 denotes 0 0 2 7 The unspecified state variables will be assigned zero SO users may not need to specify the zero components Since only the directions of vectors are concerned FLOw will normalize the user given vectors and consider them on the highest priority in determining the templates To the best of our knowledge there is no be
4. headings in the very beginning Such a system can be modeled by a 3 mode hybrid system see Figure Pe oe Vi A te seen f ee Sk 2 er x z A K xX X ae N a RK D i z e__ l Fd ee f I I ay ax Fa 4 j Pi a eee A OX S pa Mode 1 Mode 2 Mode 3 Figure 3 Hybrid automaton of the collision avoidance maneuver The state variables are as follows 1 y1 the coordinates of the first aircraft ay the heading angle of the first aircraft 2 y2 the coordinates of the second aircraft Q2 the heading angle of the second aircraft Zi timer for the semicircular arc flying Here a heading angle is the angle between the heading direction and the vector 1 0 7 in the coordinate map The dynamics of 1 Y1 2 Y2 in each mode are t V1 COS Q1 Yi V1 S N Q1 Ly V2 COS Q2 Yo V2 S N ag The angles amp 1 2 only changes at rate 1 in Mode 2 and so is the timer z To make FLOw work on the example we need to equivalently reformalize the dy namics by polynomials To do so four new variables c1 81 c2 S2 are introduced to substitute the trigonometric terms cos a1 sin amp 1 Cos 2 sina2 respectively Then the dynamics in Mode 1 and 3 becomes H U a s amp 0 6 0 a 0 0 t2 V2 C2 Y2 V2 S2 Co 0 2 0 d2 0 the dynamics in Mode 2 is t v G Yi V1 S1 C1 5 1 G a 1 z 1 t2 V2 C2 2 V2 S2 Co S2 2 C2 AQ For the jump from Mode 1 to Mode 2 t
5. respectively For the systems with more than 3 variables QR preconditioning is not suggested to use e Plot setting In order to view the reachability results intuitively FLOw over approximates a 2D projection of the flowpipes by two classes of ge ometric objects intervals boxes and octagons The image file can be generated by Gnuplot To view the interval enclosures of the flowpipes in an x y plane users may specify visualize interval x y To provide a more accurate visualization FLOW may generate a grid paving for the flowpipes The accuracy is determined by the grid number which can be specified by users For example users may use the plot setting visualize grid 10 x y to tell FLOw to split the domain of a TM flowpipe evenly into 10 parts in each dimension totally 10 grids wherein n is the number of the vari ables and compute the images of the grids under the flowpipe mapping by interval arithmetic The three visualizations of the Van der Pol oscillator example is presented in Figure 2 e TM orders the orders of the TM arithmetic Theoretically FLOw may always achieve a better accuracy with higher TM orders as long as proper remainder estimations A fixed order for all state variables can be specified like fixed orders 5 or the user may like to try uniform adaptive orders adaptive orders min 3 max 6 It is quite common that a system may have several variables change at very different rates In that case FLOw allo
6. User s Manual of FLOW May 29 2013 1 Overview The reachability analysis of hybrid systems is a difficult task since the reachabil ity problem on hybrid systems is not decidable even the variable derivatives are all constant The tool FLOw computes Taylor Model TM flowpipes for a given hybrid system Each flowpipe is an over approximation of the reachable set in a small time interval time step and the union of them then over approximates the reachable set in bounded time horizon and jump depth FLow deals with a subclass of general hybrid systems such that i the continuous dynamics are given by polynomial Ordinary Differential Equations ODEs ii a mode invariant or jump guard is defined by a conjunction of polynomial constraints and iii a jump reset is a polynomial mapping The high level structure of FLOW is presented in Figure 1 The tool uses TM based methods including a integrating ODEs b computing TM guard and TM invariant intersections c aggregating finitely many TMs to compute a set of TM flowpipes which over approximate the reachable set of the given hybrid system The tool accepts the following input files i a model file which specifies the reachability task on a continuous or hybrid system ii a TM flowpipe file which contains the state space definition and TM flow pipes For a model file FLow performs the TM flowpipe construction and generates a plotting file as long as a TM flowpipe file whi
7. ch can be reused by FLOow or other tools If there is an unsafe set specified the tool also returns the checking results For a TM flowpipe file FLow calls the TM analyzer module and generates a plotting file Similarly a safety checking result may also be returned if an unsafe set is specified It is easy to use FLOW Users may execute flowstar lt reach model to let the tool work on a reachability task specified in reach model If the computation is successful FLOw terminates with a plotting file ends with plt and a TM flowpipe file ends with flow which are located in the sub directory outputs The software Gnuplot is required to visualize a plotting file flowpipes plt In the tool directory users may simply execute gnuplot outputs flowpipes plt and then an eps file will be produced in the subdirectory images Users may change the plot setting or the unsafe set specification in the flowpipe file and TM file Model file TM parser Model parser arithmetic Image Computation TM integrator Domain contraction Range TM analyzer over approx ete ee ee a aa Plotting file Result TM file Figure 1 Structure of FLow let FLow do the new analysis job on the original flowpipes flowstar lt outputs flowpipes flow a new plotting file will be generated in images FLow has a simple installation After the libraries and tools listed
8. he guard is 11 2 y1 y2 lt D and the reset mapping is E beat Pe ogee a Ps sa T E Q1 Q1 gt Qs Q2 gt Cy 81 51 C1 Cy S2 S2 C2 T 2 2 For the jump from Mode 2 to Mode 3 the guard is z 7 and the reset mapping is same as the above one Our model file is shown as below wherein we choose v v l and D 2 1 hybrid system state var xi y1 ci si al x2 y2 c2 s2 a2 z 3 4 5 settings 6 7 8 fixed steps 0 02 time 15 9 remainder estimation 1e 6 10 identity precondition 11 visualize interval x1 y1 12 adaptive orders min 2 max 5 13 output aircraft 14 max jumps 2 the bound on the jump depth 15 print on 16 TF 18 modes 19 4 20 mode1 21 22 ode 23 24 xl c1 yl s1 cl 0 si 0 al 0 x2 c2 25 y2 s2 c2 0 s2 0 a 0 z 0 26 27 inv 28 29 x1 x2 2 yl y2 2 gt 4 30 31 32 mode2 33 34 ode 35 36 xl c1 yl s1 cl s1 si c1 al 1 x c2 37 y2 s2 c2 s2 s2 c2 a 1 2 1 38 39 inv 40 41 z lt 3 1415 42 43 44 mode3 45 46 ode 47 48 xl c1 yl s1 cl 0 si 0 ai 0 x c2 49 y2 s2 c2 0 s2 0 a 0 z 0 50 51 inv no invariant 52 53 54 55 56 57 jumps 58 6 59 start mode1 60 end mode2 61 guard x1 x2 2 y1 y2 2 4 62 reset al al
9. in Table 1 properly installed users only need to type make to compile the source code and an executable file flowstar will be generated Names Weblinks GMP Library ttp gmplib org GNU MPFR Library ttp www mpfr org GNU Scientific Library ttp www gnu org software gs1 GNU Linear Programming Kit ttp www gnu org software glpk Bison GNU parser generator flex The Fast Lexical Analyzer Gnuplot g y E 5 ttp www gnu org software bison http flex sourceforge net ttp www gnuplot info Table 1 Libraries and tools needed by FLow The technical details of FLOWw are described in I 2 2 Model specifications We introduce the modeling language in FLOW by two examples 2 1 Modeling language for continuous systems A Van der Pol oscillator can be described by the following 2 dimensional ODE g w Yo y ray We use FLOW to perform a flowpipe construction from the initial set x 1 25 1 55 y 2 25 2 35 with the time horizon 0 7 The content of the modeling file is shown as below 26 continuous system state var x y declare the state variables settings the reachability setting fixed steps 0 02 time step size time 7 time horizon 1e 5 1e 5 in each dimension QR precondition the preconditioning technique visualize octagon x y plot the octagon enclosure of the flowpipes adaptive orders m
10. in x 4 y 4 max x 6 y 6 TM orders remainder estimation 1e 5 HHH H H output vanderpol name for the output files print on display the computation steps init specify the initial set x in 1 25 1 55 y in 2 25 2 35 ode specify the ODE x y y y Xx x 2 y The explanation of the parameters are as follows e Time step size the size of TM integration steps A fixed step size 0 02 can be specified by fixed steps 0 02 or a user may want FLOW to perform adaptive step sizes range from 0 01 to 0 05 adaptive steps min 0 01 max 0 05 e Time horizon A time horizon 0 T can be specified by time T e Remainder estimation the remainder estimation interval used in TM in tegration Users may simply write for example remainder estimation 1e 5 to tell FLow to use 10 10 as the estimation interval in all di mensions Or more specifically apply different estimations over the di mensions For example the following specification tells FLOW to apply 0 002 0 002 to the dimension x and 0 1 0 1 to the dimension y remainder estimation x 2e 3 2e 3 y 0 1 0 1 In adaptive flowpipe construction the wrapping effect can be controlled by using a set of small estimations e Preconditioning technique FLOw provides two preconditioning tech niques to control the wrapping effect in TM integration They can be specified by QR precondition and identity precondition
11. st approach to choose templates Then more heuristics will be added in the future More benchmarks are described on the homepage of FLow please visit http ccis colorado edu research cyberphysical taylormodels References 1 X Chen E brah m and S Sankaranarayanan Taylor model flowpipe construction for non linear hybrid systems In Proc of the 33rd IEEE Real Time Systems Symposium RTSS 12 pages 183 192 IEEE 2012 10 2 X Chen E brah m and S Sankaranarayanan Flow An analyzer for non linear hybrid systems In Proc of the 25th International Conference on Computer Aided Verification CAV 18 LNCS Springer 2013 3 I Mitchell and C Tomlin Level set methods for computation in hybrid systems In Proc of the 8rd International Workshop on Hybrid Systems Computation and Control HSCC 00 volume 1790 of LNCS pages 310 323 Springer 2000 11
12. the two aircraft trajectories are presented in Figure 4 no collision is detected by FLow In a hybrid model file the discrete modes and jumps are declared in modes and jumps respectively The specification of a mode is of a First aircraft b Second aircraft Figure 4 Collision avoidance maneuver the following structure name user defined name of the mode ode polynomial ODE of the mode inv polynomial constraints A jump from mode m1 to mode m2 is defined by start ml end m2 guard polynomial constraints reset polynomial reset mapping with uncertainties aggregation setting FLOw accepts polynomial reset mappings of the form x p wherein x is a state variable and p is a polynomial over the state variables Additionally users may also include an interval uncertainty that is x p a b An unspecified variable will be assigned an identity mapping that is x x To relieve the computation burden it is always necessary to aggregate the flowpipes after a jump Since TMs are not closed under union aggregating a set of TMs is not an easy job FLOw provides the following schemes to compute a parallelotopic aggregation which can be efficiently transformed into an order 1 TM with zero remainder interval The key part of the parallelotopic aggregation is the template selection For a d dimensional parallelotope its orientation can
13. ws users to specify different orders or order ranges over the state variables For example fixed orders x 3 y 4 and adaptive orders min x 2 y 3 max x 5 y 4 e Output specification After a successful computation FLOW generates two files name plt and name flow in the output directory such that name can be specified in the model file by output name e Print out The display of the computation steps can be turned on or off by specifying print on or print off respectively With proper adaptive parameters users may obtain a good efficiency with very little loss of accuracy The initial set of a continuous system can be an interval or a TM An interval initial set is given by specifying each variable an interval for example x in 1 2 y in 1 1 The definition of a TM initial set consists of three parts 1 TM variable declaration 2 the TM polynomial and remainder 3 the TM domain An example of 2 state variables x y is given as below tm var x0 x1 x2 x 1 x172 x2 0 0 y x0 3 x1 0 0 xO in 0 2 0 2 x1 in 0 2 0 2 x2 in 0 1 0 1 a intervals b octagons c grids Figure 2 Van der Pol oscillator Currently FLOW only accepts polynomial ODEs For a state variable x its ODE can be specified by x p such that p is a polynomial over the state variables The syntax of polynomials in FLOW is given as below p
Download Pdf Manuals
Related Search