The scalable adaptive cruise controller model

Here is a model for an adaptive cruise controller, very similar with the one in HPWC category, http://cps-vo.org/node/31200.

Model Description, copied from http://cps-vo.org/node/31200: There are n vehicles is a queue, each of which senses the speed of the car in front an keeps this speed. The speed sensor have possible distrurbance constrained in an interval.

The intersting point of this model is that it is scalable, you can introduce arbitrary number of cars into the system to increase the size, number of variables and locations, of the model. Therefore, this case is suitable to measure the scalability of the tool.

It cames from the following paper. Jha, S., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. In: 10th International Conference on Hybrid Sys- tems: Computation and Control, pp. 287-300 (2007)

Here we have models from 5 to 15, and even 100, 200, and 500 cars. We also provide a code to generate the model with arbitrary number of cars.