The ETC Regulation Control Problem

This example demonstrates the application of CheckMate to verify properties of a hybrid system with ranges of values for the initial state and parameters in the system model. The requirements given for the MoBIES OEP page can be shown to either hold or not hold by simulation studies for particular initial conditions and parameter values. For example, simulations of the CheckMate model of the ETC system in the demo example ETC5D show that the transient response never violates the rise-time specifications, even for cases when the throttle spring constant and equilibrim position deviate from their nominal values by 20%.

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.

sim5d
Figure 1: Simulation of the the model from the ETC5D demo, for a spring constant and spring equilibrium that are both 20% beyond nominal.

The CheckMate Model

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.

simulation
Figure 2.Simulation of the the ETC model from the vertices of the initial condition set - 5D model.
simulation - ZOOM
Figure 3. Simulation of the the ETC model - zoom in the region of interest.

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.

far
far
Figure 4. CheckMate model and the StateFlow diagram included for verification purposes.

The Verification

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.

far
Figure 5. Results of the verification for the ETC. The initial set is the red box on the right, the final set the green diagonal box.

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.

Background on Parametric Verification

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.

step1

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.

step2

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.

step3

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.