Benchmark

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

Visible to the public Yet another adaptive cruise controller

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

Visible to the public Fischer's protocol

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

Visible to the public Benchmarks in a Standard Form

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

Visible to the public  Quadrotor Attitude Control

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

Visible to the public Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark

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

Visible to the public Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark

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

Visible to the public New Benckmarks

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.

file

Visible to the public neuron.cfg

file

Visible to the public neuron.xml

forum

Visible to the public CNLN Problem Instance: Neuron

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)