A verification benchmark is a model together with a list of properties to be checked on the model.
forum
Submitted by mg on Fri, 12/16/2016 - 7:42am
Here is a model for an adaptive cruise controller. We have 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. Here we have models from 2 to 6 cars.
forum
Submitted by mg on Fri, 12/16/2016 - 7:34am
Here is an implementation of Fischer's protocol for 2 to 6 concurrent components. The components attempt infinitely often to enter the critical section, according to the protocol described e.g. here.
The clocks of the components have drift bounded by intervals. Safe and unsafe versions are available, whose difference cosists of the timeout for entering the critical section.
forum
Submitted by xinchen on Thu, 12/15/2016 - 11:10pm
Dear Organizers,
I would be very grateful if you could provide all benchmarks in a standard form based on which hybrid automata could be obtained easily, since it could not only save a lot of time for the tool authors but also ensure that we are using the same benchmarks.
forum
Submitted by althoff on Thu, 12/15/2016 - 4:20pm
I would also suggest the quadrotor altitude control from ARCH 2015 since it is more high-dimensional than Stanley's example.
Here is the link.
forum
Submitted by mover on Wed, 12/14/2016 - 4:20pm
Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark
The TTEthernet benchmark (http://cps-vo.org/node/26547) seems the only one with a picewise constant dynamic among the ARCH benchmark (please, tell me if there are others).
I tried to run the models (http://cps-vo.org/node/26534) with the provided configuration scripts with SpaceEx.
I have several doubts on the benchmark.
@Sergiy Bogomolov: since you are one of the authors of the models, could you please take a look at the following questions and provide some clarifications?
forum
Submitted by mover on Wed, 12/14/2016 - 4:19pm
Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark
The TTEthernet benchmark (http://cps-vo.org/node/26547) seems the only one with a picewise constant dynamic among the ARCH benchmark (please, tell me if there are others).
I tried to run the models (http://cps-vo.org/node/26534) with the provided configuration scripts with SpaceEx.
I have several doubts on the benchmark.
@Sergiy Bogomolov: since you are one of the authors of the models, could you please take a look at the following questions and provide some clarifications?
forum
Submitted by xinchen on Wed, 12/14/2016 - 12:54pm
Dear All,
I am wondering whether we could propose benchmarks from the papers not in ARCH if we do not have enough examples by Dec 15th.
If so, I would like to suggest the following criteria for a benchmark.
1) It should be originally published in a paper which is NOT from the authors of the tools in our competition.
2) Configurations (initial sets, unsafe sets) for different difficulty levels should be provided. Trivial safety checking tasks should be excluded.
forum
Submitted by stanleybak on Tue, 12/13/2016 - 5:36pm
This is the FitzHugh-Nagumo Neuron Model, proposed in the ARCH paper "Benchmarks for Non-linear Continuous System Safety Verification", by Andrew Sogokon, Taylor T Johnson and Khalil Ghorbal.
It is a 2-d system with the following nonlinear dynamics:
x' = x - x^3 / 3 - y + 7/8
y' = 0.08 * (x + 0.7 - 0.8*y)