Classification

# of variables	# of modes	# of jumps
3	6	11

Type	Continuous dynamics	Guards & Invariants	Resets
hybrid	linear polynomial	hyperplane & half-space	constant

Download

Flow*	cruise_control1.zip
SpaceEx	cruise_control.zip

Model description

This cruise control benchmark was already used in [1] for testing the decompositional stability verification approach. We suggest it here as a benchmark for testing verification tools. It has in particular a service and emergency brakes. The proposed hybrid model takes in addition the braking behavior of the engine under consideration. A detailed description can be found on pages 128, 129 and 130 of [1].

• is the difference between the actual and the desired velocity.
• is the time.
• is an auxiliary variable.

The hybrid automaton of the benchmark:

Reachability settings

As an inital set we use:

• 
• 
• 

The initial location is and the time horizon .
The bad states are the set of states where .

Alternative initial settings:

• or
• 
• 

Results

References

[1] J. Oehlerking. Decomposition of Stability Proofs for Hybrid Systems, Dissertation zur Erlangung eines Dr.-Ing., Universität Oldenburg, 2011.