A verification benchmark is a model together with a list of properties to be checked on the model.
forum
Submitted by ttj on Tue, 05/12/2020 - 8:56am
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
forum
Submitted by schillic on Sun, 04/26/2020 - 1:20pm
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
Submitted by stanleybak on Wed, 04/22/2020 - 10:44am
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
Submitted by stanleybak on Wed, 04/22/2020 - 10:44am
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
Submitted by stanleybak on Wed, 04/22/2020 - 10:44am
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.