A verification benchmark is a model together with a list of properties to be checked on the model.
forum
Submitted by schillic on Wed, 01/18/2017 - 6:59am
Prelude:
I know this is very late; I wanted to see what format other people use in this category - which did not work so well :D
So now I simply present a piecewise-linear problem in our tool-specific format.
I could try to convert to other formats if somebody prefers.
General problem description:
See here: http://dx.doi.org/10.1093/bioinformatics/btm362
forum
Submitted by njubulei on Sat, 01/14/2017 - 1:40am
The well known navigation (NAV) example from [1] models the motion of a point robot in a n-dimensional cube. The cube is partitioned into m^n rectangular regions and each such region is associated with a vector field described by the flow equations. It is extended in [2] to a scalable n- dimensional HPWC model to increase the complexity of the model.
In the attached files, we present a script to generate arbitatry large NAV models in HPWC style and we also provide some instances generated automatically.
forum
Submitted by njubulei on Tue, 12/20/2016 - 12:39am
Here is a model for an adaptive cruise controller, very similar with the one in HPWC category, http://cps-vo.org/node/31200.
Model Description, copied from http://cps-vo.org/node/31200: There are 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.
forum
Submitted by mover on Sun, 12/18/2016 - 9:51pm
We propose the following benchmarks for hybrid automata with piecewise constant dynamics.
The benchmarks we are proposing are:
- A distributed controller for a robot
- A simple system that controls a nuclear reactor
- A piecewise consant version of the navigation benchmark
The benchmark are taken and adapted from the existing literature, and are quickly described in the paper http://www.sergiomover.eu/paper/tacas15.pdf
They can already be downloaded from the link in the paper.
forum
Submitted by immler on Sun, 12/18/2016 - 9:42am
I have seen the van der Pol system in many papers, so probably most tools/tool authors have this example at their disposal:
x' = y
y' = (1 - x^2)*y - x
Is this interesting for the competition?