Automated test-case generator for CPS model checkers

Cyber-Physical Systems (CPS) are integrations of computation and physical processes. The embedded computers and networks monitor and control the physical processes, usually with feedback loops where physical processes affect computations and vice versa.
A CPS (Cyber-Physical-Systems) model checker is a software which can analyze mathematical models of CPS for property verification.Model-checkers are themselves software which needs to be sufficiently tested.
Creating an automated test-case generator for CPS model-checkers. The generator should attempt to create test-cases which can make existing model-checkers to fail.
The following is an example of a hybrid system or CPS :

Xᵥ denotes the volume of the tank, Ws denotes the input water supply rate and Wd the output water demand rate.

System is in Healthy state while 0 < Xᵥ < Vmax , where Vmax is tank’s maximum volume.

System is in Drained state if Xᵥ <= 0.

System is in Overflow state if Xᵥ > Vmax.

Why automated test-case generator is required?

Manually generating many random models can be a very tedious process. There are not many random models from existing literature. The generated xml models can be test-cases for model checkers to check if they parse models that satisfy the given properties correctly. Model checkers should be able to run correctly and should not crash for different types of models which may have missing invariants, missing guards and also multiple edges between location.