A verification benchmark is a model together with a list of properties to be checked on the model.
forum
Submitted by althoff on Fri, 04/20/2018 - 9:00am
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.
forum
Submitted by frehse on Wed, 04/18/2018 - 11:27am
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/.
forum
Submitted by stanleybak on Mon, 03/26/2018 - 9:47am
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
Submitted by xinchen on Wed, 02/15/2017 - 5:51pm
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
Submitted by xinchen on Tue, 02/14/2017 - 3:50pm
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.