Benchmark

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

Visible to the public 2020 Benchmark Proposal: VerticalCAS by Elena Botoeva

The scenario involves two aircraft, the ownship and the intruder, where
the ownship is equipped with a collision avoidance system referred to as
VerticalCAS (Julian and Kochenderfer 2019,
https://arxiv.org/abs/1903.00520). The intruder is assumed to follow a
constant horizontal trajectory. VerticalCAS once every second issues
vertical climbrate advisories to the ownship pilot to avoid a near
mid-air collision (NMAC), a region where the ownship and intruder are
separated by less than 100ft vertically and 500ft horizontally, where

file

Visible to the public embrake_deterministic.cfg

file

Visible to the public embrake_constant_nondeterministic.png

file

Visible to the public embrake_constant_deterministic.png

file

Visible to the public embrake_nondeterministic.cfg

file

Visible to the public embrake.xml

forum

Visible to the public HPWA problem: electro-mechanical brake

This is a linear hybrid model of an electro-mechanical brake from [1]. The model files used in that reference are available at [2].


# Short description:

forum

Visible to the public CAFF Problem Instance: Heat3D

The Heat3D benchmark is a spatially discretized version of the heat equation partial differential equation (PDE) in three dimensions. One way to analyze PDEs is to discretize space in a mesh resulting in a system of ordinary differential equations (ODEs), where each variable in the system is a mesh point. Depending on the granularity of discretization, you can adjust the number of variables in the ODE system. This system has no switching or inputs, and serves to evaluate one aspect of scalability, namely the number of system dimensions.

forum

Visible to the public CAFF Problem Instance: Heat3D

The Heat3D benchmark is a spatially discretized version of the heat equation partial differential equation (PDE) in three dimensions. One way to analyze PDEs is to discretize space in a mesh resulting in a system of ordinary differential equations (ODEs), where each variable in the system is a mesh point. Depending on the granularity of discretization, you can adjust the number of variables in the ODE system. This system has no switching or inputs, and serves to evaluate one aspect of scalability, namely the number of system dimensions.

forum

Visible to the public CAFF Problem Instance: Heat3D

The Heat3D benchmark is a spatially discretized version of the heat equation partial differential equation (PDE) in three dimensions. One way to analyze PDEs is to discretize space in a mesh resulting in a system of ordinary differential equations (ODEs), where each variable in the system is a mesh point. Depending on the granularity of discretization, you can adjust the number of variables in the ODE system. This system has no switching or inputs, and serves to evaluate one aspect of scalability, namely the number of system dimensions.