Benchmark

A verification benchmark is a model together with a list of properties to be checked on the model.
forum

Visible to the public HPWA problem: spacecraft rendezvous

I have created the first simulation runs of the spacecraft rendezvous. The first figure shows the x-/y-positionand the second one the velocities. The first two figures are for the model rendezvousSX4np and the second set for rendezvousSX4p. The time horizon for the simulation is 200.

file

Visible to the public drivetrain_sx.zip

forum

Visible to the public HPWA Problem: Drivedrain

This benchmark is taken from

M. Althoff and B. H. Krogh. Avoiding geometric intersection operations in reachability analysis of hybrid systems. In Hybrid Systems: Computation and Control, pages 45-54, 2012

The model files were taken from the attachments to

"Rigorous Simulation-Based Analysis of Linear Hybrid Systems", S. Bak, P. Duggirala, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017)

available at http://stanleybak.com/.

file

Visible to the public iss_fixed_zoom.png

file

Visible to the public iss_time_varying.png

file

Visible to the public iss_fixed_short.png

file

Visible to the public iss_fixed_long.png

forum

Visible to the public CAFF Problem Instance: Space Station

The system is a continuous linear time-invariant system x' = Ax + Bu proposed as a benchmark in ARCH 2016 [1]: "International Space Station (ISS). The ISS state-space model presented in this paper is a structural model of component 1R (Russian service module) of the International Space Station. It has 270 state variables with three inputs."

forum

Visible to the public HNLN: Artificial Pancreas

The hybrid automaton of an artificial pancreas is presented as below. The system has 10 variables whose evolutions are governed by the following ODE.

forum

Visible to the public CNLN example (p53 model)

Leenders, Gerald B., and Jack A. Tuszynski. "Stochastic and Deterministic Models of Cellular p53 Regulation." Frontiers in Oncology 3 (2013): 64.

This model is slightly adapted by replacing the term x1^1.8/(547600 + x1^1.8) by x1^2/(547600 + x1^2). But the model still shows oscillation.