HPWA problem: electro-mechanical brake

This is a linear hybrid model of an electro-mechanical brake from [1]. The model files used in that reference are available at [2].


# Short description:

Figure 2(a) in [1] shows a sketch of the brake. State variable x is the position of the brake, which moves toward the brake disc. The position is influenced by the motor current I. The original model is purely continuous but nonlinear. We consider a linearized hybrid version using time discretization, given in Figure 4. There is a single location with a self-loop. Apart from x and I there are three other state variables: t (a clock) and two discretization variables x_e and x_c. The transition is time triggered. In Figure 4 the transitions happen at deterministic time points (multiples of T_sample). The discretization variables are updated with every jump.


# Scenarios:

As a baseline we consider the setting described in Section 4.2 for Flow*. The suggestion is to consider four different scenarios based on parameter variation and switching policy (combinations 1A, 1B, 2A, 2B).

1) Fixed parameter values
The matrix coefficient for the I-I entry (entry (1,1) if I is the first state variable) is -1/L*(R+K2/d_rot) (as given in the paper).

2) Varying parameter value (this is the setting in the paper)
The matrix coefficient for the I-I entry is constant but initially uncertain (chosen from the interval [-507, -501]) (as suggested in the paper). This can be modeled in two ways:
- as an uncertain parameter (this is what we do in JuliaReach)
- with a new state variable that stays constant (but this encoding results in a nonlinear model)

A) Deterministic switching
The transition is taken at deterministic times (as described above and in Figure 4).

B) Nondeterministic switching
The transition is taken at nondeterministic times from an interval [T_sample - 10^{-8}, T_sample + 10^{-7}] (note that there is a typo in the paper).

I attached SpaceEx models and plots for the scenarios 1A and 1B. I suppose that scenarios 2A and 2B are not supported in every tool, so we might also exclude them (JuliaReach supports them and I believe at least CORA should as well). I hope the modification for scenario 2 is simple enough to not require a formal model.


# Properties:

The two properties in the paper probably do not hold for the linearized model. Here are some other proposals for properties. In all cases we fix the parameter x_0 = 0.05.

i) Verify that x < x_0 for a time horizon (depending on the scenario; we can verify it for the full time horizon in scenario 1A).
ii) Report the largest time horizon for which x < x_0 is verified.


# General comments:

The model looks innocent but requires to do 1,001 discrete jumps. The Flow* analysis of scenario 2 took 12 hours back in 2015, probably because there was no special handling of time. If you exploit the information that the transitions are purely time-triggered, you can avoid expensive intersection operations. I am not sure if SpaceEx is doing that but the analysis of the attached models (only scenario 1!) took 6-7 minutes.


# References:

[1] Strathmann, Oehlerking. Verifying properties of an electro-mechanical braking system. ARCH. 2015.
URL: https://easychair.org/publications/paper/1ff2

[2] https://cps-vo.org/node/20289