User's Manual of Flow v1.2.0 - Software modeling and verification
Contents
1. 2 X Chen E brah m and S Sankaranarayanan Taylor model flowpipe construction for non linear hybrid systems In Proc of the 38rd IEEE Real Time Systems Symposium RTSS 12 pages 183 192 IEEE 2012 3 X Chen E brah m and S Sankaranarayanan Flow An analyzer for non linear hybrid sys tems In Proc of the 25th International Conference on Computer Aided Verification CAV 18 LNCS Springer 2013 4 Matthias Althoff Reachability Analysis and its Application to the Safety Assessment of Au tonomous Cars PhD thesis Technischen Universitat M nchen 2010 5 K Makino and M Berz Suppression of the wrapping effect by taylor model based verified integrators Long term stabilization by preconditioning International Journal of Differential Equations and Applications 10 4 353 384 2005 6 I Mitchell and C Tomlin Level set methods for computation in hybrid systems In Proc of the 3rd International Workshop on Hybrid Systems Computation and Control HSCC 00 volume 1790 of LNCS pages 310 323 Springer 20002. 2 cos alpha1 cos alpha2 0 yt y2 y1 mode2 nonpoly ode x1 x2 z inv z lt 3 1415 cos alpha1 cos alpha2 yl y2 1 mode3 nonpoly ode x1 x2 z inv cos alpha1 cos alpha2 0 yl y2 jumps mode1 gt mode2 guard x1 x2 72 yl reset alpha1 alphai parallelotope aggregation mode2 gt mode3 guard z 3 1415 reset alphai alphai parallelotope aggregation init 1 model bound of the jump depth sin alphal alphal 0 sin alpha2 alpha2 0 y2 2 gt 4 sin alphal alphai 1 sin alpha2 alpha2 1 sin alphai alphai 0 sin alpha2 alpha2 0 y2 2 4 1 57075 alpha2 alpha2 1 57075 x1 1 y1 1 x2 1 y2 1 1 57075 h alpha2 alpha2 1 57075 72 1 73 x1 in 0 1 0 1 yi in 0 1 0 1 alphai in 0 785374 0 785376 74 x2 in 9 9 10 1 y2 in 0 1 0 1 alpha2 in 2 35612 2 35613 75 z in 0 0 76 i qu oF 78 Y 79 80 unsafe set 81 t1 82 model x1 x2 lt 0 2 xi x2 gt 0 2 yl y2 lt 0 2 y1 y2 gt 0 2 83 mode2 x1 x2 lt 0 2 x1 x2 gt 0 2 y1 y2 lt 0 2 yl y2 gt 0 2 84 mode3 x1 x2 lt 0 2 x1 x2 gt 0 2 y1 y2 lt 0 2 yl y2 gt 0 2 85 The reachability task considers all the possible initial positions in the region 0 1 0 1 x 0 1 0 1 for the firs
3. empty then the tool reports SAFE otherwise it reports UNKNOWN and dumps the potential unsafe flowpipes in a counterexample file the format of which will be described in Section 5 For the sake of efficiency the tool uses naive interval arithmetic to check the safety Therefore it is better to give linear constraints in a reachability problem 4 Modeling language for hybrid reachability problems We introduce the modeling language for hybrid reachability problems by a concrete exam ple The model of a collision avoidance maneuver of two aircraft at a fixed altitude is given in 6 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 their headings in the very beginning Such a system can be modeled by a 3 mode hybrid system see Figure 3 The state variables are listed as below 21 91 the coordinates of the first aircraft 01 the heading angle of the first aircraft 2 Y2 the coordinates of the second aircraft 03 the heading angle of the second aircraft Z3 timer for the semicircular arc flying A heading angle is the angle between the heading direction and the vector 1 0 7 i
4. 1 Libraries and tools used by FLOW 5 5 5 5 2 A Quick Start We start the usage of FLOW by a simple example given in 4 A Van der Pol oscillator can be modeled by the following ODE iy y y u a y We want to compute the TM flowpipes from the initial condition z 1 25 1 55 y 2 25 2 35 in the bounded time horizon 0 7 Such a continuous reachability task can be described by the following model file 1 file vanderpol model 2 3 continuous reachability 4 t1 5 State var x y declare the state variables 6 7 setting the reachability setting 8 t 9 fixed steps 0 02 time step size 10 time 7 time horizon 11 remainder estimation 1e 5 1e 5 1e 5 in each dimension 12 QR precondition the preconditioning technique 13 gnuplot octagon x y plotting file is in Gnuplot format 14 adaptive orders min x 4 y 4 max x 6 y 6 TM orders 15 cutoff 1e 15 cutoff threshold 16 precision 53 precision in the computation 17 output vanderpol name for the output files 18 print on display the computation steps g 20 21 poly ode 1 use the integration scheme Poly ODE 1 22 1 23 X y 24 y y x x2x y 25 26 27 init specify the initial set 28 1 29 x in 1 25 1 55 30 y in 2 25 2 35 31 Y 32 To make FLow work on the reachability task we may simply execute flowstar lt vanderpol model After a while two fi
5. the form of 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 a reset mapping may also be of the form x p a b An unspecified variable will be associated with an identity mapping that is x x The flowpipe guard intersection of a jump is usually a non convex or even a set of disjoint fragments To avoid dealing with each of them in the consequent computation we over approximate or aggregate the intersection sets by an order 1 TM with zero remainder interval which can be viewed as an parallelotope It is not hard to compute the transformations between the TM and parallelotope representations however to determine a proper orientation for the aggregation set is not easy For a d dimensional parallelotope its orientation can be determined by d linearly inde pendent vectorq 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 template plays an important role in the aggregation accuracy In FLOW we provide the following options to select a template for aggregating the flowpipe guard intersections for a jump zr HH a template 1 0 7 0 1 7 b template 1 1 7 1 1 7Y Fig 5 Example of flowpipe aggregation Interval aggregation FL
6. OW computes a box enclosure for the flowpipe union similar to the example shown in Figure The specification is interval aggregation They are also the linear independent facet normals of the parallelotope General parallelotopic aggregation Users may simply specify parallelotope aggregation to tell FLow to automatically determine the template based on the invariants guard flow directions and so on It is also allowed to give some vectors which will be definitely selected by the tool For a 3 dimensional example the following specification parallelotope aggregation x 1 y 1 z 2 tells the tool to choose 1 1 0 and 0 0 2 7 in determining the template the remaining ones will still be selected automatically Since the vector lengths make no sense in the template FLOw always normalizes the vectors to the length 1 To the best of our knowledge there is no approach to find the best template for an aggre gation job Hence we will add more heuristics into FLOW in the future 5 Formats of the output files 5 1 TM files For a continuous reachability problem the TM file generated by FLow is of the following format state var x y state variable declaration gnuplot octagon x y plot setting unsafe set bee defined by polynomial constraints output model output name continuous flowpipes tm var x0 yO declare the variables used in TMs 22 TM flowpipes A TM flowpipe is represen
7. The tool FLow also provides the possibility to dump all potential unsafe flowpipes Since the TM flowpipes are over approximations of the exact reachable set segments we are not able to prove the unsafety by detecting a nonempty intersection between the TM flowpipes and the unsafe set However we may dump those potential unsafe T M flowpipes and they can be used in further analysis work For a continuous reachability problem the unsafe TM flowpipes are dumped into a counterexample file of the following form 1 starting time t starting time of the flowpipe 1 TM flowpipe Y For a hybrid reachability problem the counterexample file is as follows mk mode name 1 starting time t local starting time of the flowpipe 1 rS TM flowpipe Y computation path the computation path leads to the unsafe flowpipes mi ni ai bi gt m2 m2 a2 b2 gt gt mk Since we compute over approximations the counterexamples generated might be superflu ous 6 More case studies We collected a considerable number of continuous and hybrid system benchmarks in the case study homepage of FLOow It can be found as below http systems cs colorado edu research cyberphysical taylormodels casestudies References 1 R Alur C Courcoubetis N Halbwachs T A Henzinger P H Ho X Nicollin A Olivero J Sifakis and S Yovine The algorithmic analysis of hybrid systems Theor Comput Sci 138 1 3 34 1995
8. User s Manual of Flow v1 2 0 Xin Chen RW TH Aachen University Germany xin chen cs rwth aachen de November 20 2013 1 Introduction Hybrid systems are dynamical systems which exhibit both continuous flow and discrete jumps They are natural modeling formalism for the systems composed of a discrete con troller interacting with a physical environment Since hybrid systems often appear in safety critical situations it is non trivial to study their behavior A typical way to do that is to explore the reachable state space of a hybrid system which is called reachability analysis Unfortunately such a job can not be done algorithmically since the reachability problem on hybrid systems is undecidable I The tool FLow tries to compute an over approximation for a bounded reachable set of a hybrid system A reachable set w r t a bounded time hori zon 0 T and a maximum jump depth k is called bounded it consists of the states each of which can be reached at some time t 0 T via at most k jumps from an initial state of the system The over approximation set computed by FLOW is a finite group of Taylor Model TM flowpipes Each flowpipe over approximates the exact reachable set in a small time interval The hybrid system models considered by FLow are described as follows The continuous dynamics in a mode should be defined by a non linear Ordinary Differential Equation ODE A mode invariant or a jump guard should be defined by poly
9. e 5 y 0 1 0 1 2 y be 4 5e 4 x C1e 3 1e 3 over the domain x y 1 1 will be simplified to 0 5 0 5 x 0 1 0 1 x y 1 51e 3 1 51e 3 if the terms within 1e 3 1e 3J are considered small Such a threshold can be specified by cutoff and then a term which is contained in amp amp will be moved to the remainder Precision the precision of the floating point numbers in the MPFR library Output name the name of the output files If output model is specified then the Gnuplot and MATLAB plotting files will be named by model plt and model m respectively the TM file will be of the name model f1ow Print out The display of the computation steps can be turned on or off by specifying print on or print off respectively Additionally an unsafe set can be optionally given after the reachability problem such as unsafe set 1 polynomial constraints pi lt ci p2 gt c2 p3 in c3 c4 The set should be defined by finitely many polynomial constraints That is the set is com posed by the states that satisfy all of the constraints A polynomial constraint should be given as the form p c or p in c1 c2 wherein p is a polynomial over the state vari ables c c1 c2 are constants and E lt gt After the flowpipe construction FLOW checks the emptiness of the intersection between the flowpipes and the unsafe set If it is
10. erval x y or matlab interval x y for the Gnuplot output or MATLAB output respectively For octagon visualization users may just replace the term interval by octagon in the above specification Besides FLOW also provides more accurate visualizations which is based on grid pavings over TM flowpipes For example users may use the plot setting gnuplot grid 10 x y to tell FLow to divide a TM flowpipe into 10 parts wherein n is the number of the state variables by splitting the original domain uniformly into 10 grids in each dimension Then the plotting is based on the interval enclosures of the subdivisions TM orders The orders of the TMs in flowpipe construction Theoretically FLOW may always achieve a better accuracy with higher T M orders A fixed order 5 in all dimensions can be specified as fixed orders 5 or the user may want to apply a uniform adaptive order ranges from 3 to 6 adaptive orders min 3 max 6 It is quite common that a system may have several variables which change at very different rates For such systems FLow allows users to specify different fixed or adaptive orders over the state dimensions For example fixed orders x 3 y 4 or adaptive orders min x 2 y 3 max x 5 y 4 Cutoff threshold In order to improve the performance FLOW simplifies a TM by sweeping the small terms in the polynomial part into the remainder interval For example the TM 0 5 0 5 1e 5 l
11. les vanderpol plt and vanderpol flow are generated in the subdirec tory outputs To visualize the flowpipes users may use Gnuplot gnuplot lt outputs vanderpol plt and then an eps file will be produced in the subdirectory images If the plotting file is speci fied as a MATLAB file then a m file is generated in outputs and it can be directly executed in the MATLAB environment In Figure 2 we present the three kinds of visualizations of the same TM flowpipes produced by FLOW a intervals b octagons c grids Fig 2 Different visualizations of the flowpipes 3 Modeling language for continuous reachability problems We give a detailed introduction for the modeling language of continuous reachability prob lems in FLow To describe a continuous reachability task we should first define the initial value problem and then specify the parameters which are used in the reachability compu tation An initial value problem is defined in the following form in FLOW initial set The option poly ode 1 tells the tool to use the integration scheme Poly ODE 1 and it can be replaced by one of the other two i e poly ode 2 and nonpoly ode A d dimensional ODE can be given by d equations of the form x y such that x is a state variable and y can be a polynomial in the first two integration schemes or a non polynomial expression in the last integration scheme over the state variables If y is a po
12. lynomial then it should be defined according to the following syntax Q otvolo olo nwvoel veltoivninx r wherein n is a positive integer x is a variable and r is a real number The priorities of the operators are given in Table 2 If v is a non polynomial expression then the corresponding syntax is given as follows Q otolo wvlinvoe nwvoi oltoivgnilixi ir sin y cos y exp y ve ve sqrt y in which sin cos are the trigonometric functions sine and cosine respectively exp is the exponential function is the division operator and sqrt denotes the square root FLOW also allows users to specify time varying disturbances which are bounded by intervals in ODEs For example x 1 0 5 x y x73 0 01 0 01 The initial set can be an interval or a TM An interval initial set is given by specifying each variable a single interval for example x in 1 2 y an 1 1 The definition of a TM initial set consists of three parts 1 TM variable declaration 2 the TM and 3 the TM domain An example is given as below tm var xO x1 x2 x 1 x1 2 x2 0 02 0 01 y x0 3 x1 0 0 1 x0 in 0 2 0 2 xi in 0 2 0 2 x2 in 0 1 0 1 wherein x y are the state variables operators priorities P 4 prefix 3 The parameters in the reachability setting 2 are explained as below 1 infix 1 Time step size The size of TM integration Table 2 Priorities of the operato
13. module TM integrator we provide three different schemes for the integration of non linear ODEs The functionalities of them are listed as follows Poly ODE 1 prefers low degree polynomial ODEs Poly ODE 2 prefers high degree polynomial ODEs Nonpoly ODE prefers non polynomial ODEs TM file Model file Image Computation TM integrator Poly Poly Nonpoly ODE 1 J ODE 2 ODE Domain contraction Range over approx TM analyzer Plotting file Result TM file Fig 1 Structure of FLow Although the low degree polynomial ODEs are also supported by the last scheme they can be handled more efficiently by the first scheme Our tool has a simple installation After that the libraries and tools listed in Table I are properly installed users only need to type make to compile the source code and then an executable file flowstar is generated Most of the technical details of FLOW are described in BIB Please visit the following web page to fetch the current version of the tool http ccis colorado edu research cyberphysical taylormodels Names GMP Library GNU MPFR Library GNU Scientific Library GNU Linear Programming Kit Bison GNU parser generator flex The Fast Lexical Analyzer Gnuplot Weblinks http gmplib org ttp www gnu org software gsl ttp www gnu org software glpk http www gnu org software bison http flex sourceforge net ttp www gnuplot info Table
14. n the coordinate map N M A s pice c gi s e f LN ud x a i x x EE kw 4 Vs A K D Eo s 7 S e 3 I dr ou gf S f 1 eb PONAT MB z 1 Fi z A UM Na A XK s jr Mode 1 Mode 2 Mode 3 Fig 3 Hybrid automaton of the collision avoidance maneuver The continuous dynamics in each mode are of the form Ly U1 COSQ1 y v1 Sino 12 U2 COS Q2 Y2 U2 sin a2 The angles o1 o only changes in Mode 2 and so is the timer z For the jump from Mode 1 to Mode 2 the guard is given by the constraint x x2 y1 y2 D and the reset mapping is Y 24g T 2 Q3 Ag 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 simply choose v v2 1 and D 2 1 ay Q1 hybrid reachability state var x1 yl alpha1 x2 y2 alpha2 z 1 2 3 4 5 setting 6 Y 8 9 fixed steps 0 02 time 15 remainder estimation 1e 6 10 identity precondition 11 gnuplot octagon x1 y1 12 adaptive orders min 2 max 5 13 cutoff 1e 12 14 precision 53 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 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 7 output aircraft max jumps 2 print on modes 1 model nonpoly ode 1 x1 x2 z inv x1 x2
15. nomial constraints A jump reset should be defined by a polynomial mapping The initial set of a hybrid system can be given by an interval or a TM We present a birdview of the tool in Figure 1 FLOw accepts two classes of input files A model file describes a bounded reachability problem on a hybrid or continuous system The tool tries to compute an over approximation for the bounded reachable set A TM file includes a state space definition as well as finitely many TM flowpipes The tool reads those specifications and generates a plotting file for the flowpipes In both of the cases an unsafe set can be specified and FLow will conservatively check the emptiness of the intersection between flowpipes and the unsafe set The output of FLOW consists of the following files A plotting file which provides a 2D visualization of the flowpipes The format of the plotting file can be determined by users it can be a Gnuplot file or a MATLAB file A T M file which describes the state space of the system and contains all computed TM flowpipes The file can be reused by FLOW or the content may also be extracted and analyzed by other tools If an unsafe set is given and the tool detected some unsafe flowpipes then a counterexample file is generated The file includes all potential unsafe flowpipes as well as the discrete computation paths which lead to them The two main components of FLow are the TM integrator and the image computation module In the
16. rs steps A fixed step size 0 02 can be specified by fixed steps 0 02 To apply an adaptive step size ranges from 0 01 to 0 05 users may write adaptive steps min 0 01 max 0 05 Time horizon A time horizon 0 T is given by time T Remainder estimation The remainder estimation interval used in TM integration Users may simply write for example remainder estimation 1e 5 to tell FLow to use le 5 le 5 as the estimation interval in all dimensions It is also possible to specify different remainder estimations over the dimensions For example the following setting tells FLOw to apply 2e 3 2e 3 to the x dimension and 0 1 0 1 to the y dimension remainder estimation x 2e 3 2e 3 y 0 1 0 1 Small estimations help in control the wrapping effect in flowpipe construction Preconditioning technique FLOW provides two preconditioning techniques to control the wrapping effect Users may specify QR precondition to use the QR preconditioning technique or use identity precondition to apply the identity preconditioning technique For the systems with more than 3 variables QR preconditioning technique is not suggested to use More details can be found in 5 Plot settings It is difficult to plot even a 2D projection of a TM Given two state variables x y FLOW plots the interval box or octagon over approximations of the flowpipes in the x y plane To generate an interval visualization users may specify gnuplot int
17. t aircraft and the initial positions in the region 9 9 10 1 x 0 1 0 1 for the second aircraft The initial heading angle of the first aircraft is 7 and that of the second aircraft is 2m There are at most two jumps in the hybrid automaton so we bound the jump depth by 2 We set the time horizon 0 15 such that the two jumps will definitely be executed in 15 time units The octagon enclosures of the two aircraft trajectories are presented in Figure FLOW verifies that the two aircraft never got too close to each other o 2 6 s 10 12 E o 2 6 s 10 12 a First aircraft b Second aircraft Fig 4 Collision avoidance maneuver Similar to the modeling file of a continuous reachability problem the description of a hybrid reachability problem is also composed by two parts i e the setting for reachability computation and the initial value problem on a hybrid system The locations modes and jumps of a hybrid system are declared in modes and jumps respectively A mode is defined by the form name name of the mode poly ode 1 can also be poly ode 2 or nonpoly ode 1 ODE in the mode inv polynomial constraints and a jump from mode m1 to mode m2 is defined by the form mi gt m2 guard polynomial constraints Y reset 1 polynomial reset mapping with uncertainties aggregation setting FLOW accepts polynomial reset mappings given in
18. ted as x p a b TM in every dimension local_t in 0 r domain of the TM x0 in c d h wherein local t is the local time variable of the TM It ranges in a time step interval Notice that the TM variables are automatically named by the tool thereby their names have nothing to do with the state variable names For a hybrid reachability problem the generated T M file is of the following form The flowpipes are kept according to the mode sequences visited in the computation state var X y state variable declaration modei specify the mode invariants computation paths computation paths of modes 1 mi ni ai bi gt m2 n2 a2 b2 gt gt mk gnuplot octagon x y plot setting output model output name unsafe set 1 hybrid flowpipes modei 1 tm var x0 yO declare the variables used in TMs idee TM flowpipes ia other modes in the computation tree F The computation paths of modes are also dumped As an example the path mi ni a1 b1 gt m2 n2 a2 b2 gt gt mk denotes a mode sequence from m1 to mk in the reachability computation A segment mi n a b gt mj means that there is a jump which is numbered by n from the mode mi to the mode mj such that the execution time is included by the interval a b For a hybrid system the jumps are numbered by 1 2 in the order of their declarations 5 2 Counterexample files
Download Pdf Manuals
Related Search