In this example we demonstrate verification of the requirement that the throttle angle should not exceed a 5% band around the steady state value of the reference signal after the transient phase of a step response. Simulations such as the one shown in Figure 1 demonstrate that this property is satisfied for a finite-time horizon for the nominal values of the system parameters. The objective here is to show that the specification is satisfied for a range of possible values for the throttle spring constant and equilibrim position. Our approach is to show that, starting from a range of initial states corresponding to the end of the transient phase of the system step reponse, the sliding mode defined in ETC5d demo is reached.
The structure of this model is the same as the model described in the other ETC demo. Futher infomation may be found in this powerpoint presentation.
In this model, we assume that the reference signal has reached its steady state value, and can therefore omit the reference signal filter. Consequently, the CheckMate model has only two state variables, the throttle angle α and the angular velocity ω. The sliding surface, which is defined by s=λ(α-uf) + (ω-u'f ), becomes s=λ(α-αdes) + ω. Similarly, other occurrences of the filter in the etc5d model are replaced. All other hyperplanes and thresholds in the higher dimensional ETC model were already expressed in α and ω only.
Analyzing the system dynamics and the trajectories from the initial conditions, it is possible to identify a region where all the trajectories pass through. By enlarging this region we have a conservative approximation for the reachable region, starting at the initial set. The enlarged reached region is called outer box. The rationale is that the set should, for example, be reached by all trajectories from the initial after a step change to the desired angle. By using the outer box as the initial set for the verification procedure, one can focus on the behavior that is close to the region where the system can potentially violate the requirements (α > 1.05αdes). Figure 2 shows the trajectories for the vertices of the initial set, for the full-dimensional case, where all of them cross the outer box. Figure 3 shows the crossing in detail.
Once the trajectories enter the region between the sliding surfaces, a region called middle box, it is necessary to show that all the trajectories starting in the middle box go to the steady state, without violating the requirements. This investigation can be done by verification or by observing that the vector field inside the middle box points towards the steady state region, which combined with the robustness of the sliding mode behavior is sufficient to guarantee that all trajectories go eventually to the steady state. The middle box region will be used as the termination criterion for the verification.
In addition to the thresholds for the sliding surface and coulomb friction we define the middle box neighborhood as another region. The objective of this region is to show that if the system leaves a pre-defined initial condition set it will enter the middle box
We add to the file setup2_reg.m
the definition of
the outer box and middle box. They are defined as
follows:
C_outer = [1 0;-1 0;0 1;0 -1]; d_outer = [alpha_des*1.04;-alpha_des*1.003;-0.1;0.2]]; assignin('base','etc_ICS',linearcon([],[],C_outer,d_outer));
C_middle = [-60 -1]; d_middle = -94.0883; assignin('base','middle',linearcon([],[],C_middle,d_middle));
Note that the outer box will be defined as the initial
set. The middle box will be represented only by one face of the
sliding surface, since the dynamics crosses this face first. The
simplified CheckMate model will have only one SFM block,
called state. In this model, the discrete states model the
transitions for the coulomb friction (called left, neither and
right) and there is a final state called reach, if the trajectory
reaches the middle box. There is no need to specify an ACTL
formula; CheckMate will generate the necessary property by
itself. Recall from the other demo's that we name a location
reach
if each trajectory has to eventually reach the
location. Figure 4 shows the part that was
included to verify the property.
Figure 5 shows the flowpipe segments that were computed during the verification. The red box is the initial set, the green box is the neighborhood of the sliding surface that has to be reached.
The verification shows that the state do always reach the sliding surface. While running the verification one might encounter the following warning:
Warning: Optimization did not improve the results of the convex hull approximation during reachability analysis.This warning tells the user that the optimization in step 3 did not yield a better result than the convex hull approximation of the simulated points and vertices, for a particular face (step 2). In this case the optimization was not able to improve the result. In all other cases, however, simulation did not provide a conservative approximation, and using optimization did improve the result.
Finally, since the verification works out as planned, you might see the following output:
Parsing specification 1: (AG ~out_of_bound)&(AF state == reach) Compiling list of atomic propositions. * out_of_bound * state_in_reach Making refinement decision. System enters the state "reach" in all cases. total verification time is 194.92 seconds. >>We can therefore conclude that the system did not leave the analysis region, and that the system reaches the sliding surface in all cases.
CheckMate allows the user to specify uncertainty ranges on parameters for the continuous dynamics. In this ETC demo we have selected the spring constant and the spring equilibrium as uncertain parameters. We assume that both may deviate with 20% from their nominal values. Both parameters have an influence on how the system behaves close to the steady state.
Parameters are incorporated into the verification precedure during the computation of the flowpipe approximations. The flowpipe approximation starts from an initial set of states (a polyhedron) in the continuous state space. As a first step, each vertex of the initial set is simulated up to a predefined time Δt. In the parametric case, this simulation is performed for all vertices of the polyhedron that defines the set of possible parameter values, as well as for the vertices of the initial state set. This is illustrated in the figure below, where the polyhedron represents the initial set of states and the points represent the results of simulating the system for the vertices in both the state set and the parameter set.
The next step is to determine the convex hull of the simulation points and the vertices of the initial state set, as illustrated in the following figure. This step is mainly done to obtain the normals on the faces. These directions are used get an over-approximation of the reachable set.
The third and last step, illustrated below, is to push the faces in the direction of its normal, such that the face will become a tangent plane of the reachable set. The flowpipe approximation uses an optimization routine to do so.
The optimization, given a non-parametric system, is performed over all initial states and all times within the interval t and t+Δt. To obtain the flowpipe for a parametric model one has to optimize over the parameter range, too. This means for the ETC example in this demo, that the optimization problems are 5-dimensional, two dimensions for the states, two for the parameters and one time dimension.