Verifying Fragility in Digital Systems with Uncertainties using DSVerifier v2.0

Experimental Setup:
The experiments were executed in a computer with the following hardware configurations: Intel Core i7-2600 3.40 GHz processor, 24 GB of RAM, and Ubuntu 64-bits OS. The experiments used the Linux times command to measure CPU time used for each benchmark. The runtime was limited to one hour (i.e., 3600s).

Benchmarks Description:

IEEE Transaction on Computers Benchmarks: We extracted 4 digital systems (controller and plant) from Keel, L.H. and Bhattacharyya, S.P. 1997. Robust, fragile, or optimal? IEEE Trans. Automat. Control, 42, 1098–1105. All digital systems are designed in transfer-function format, and the discretized plant and controller are published by Bessa, I. V. et al. Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty. In IEEE Transactions on Computers, v.66(3), pp. 545-552, 2017.

ACM International Conference on Hybrid Systems: Computation and Control (HSCC) Benchmarks:
The first set of benchmarks uses the discrete model of a cruise control system for a car, and accounts for rolling friction, aerodynamic drag, and the gravitational disturbance force.
The second set of benchmarks considers the discrete model of a simple spring-mass damper plant.
A third set of benchmarks uses the discrete model for satellite attitude dynamics, which require attitude control for orientation of antennas and sensors w.r.t. Earth.
The fourth and fifth set of benchmarks describe the discrete model of a DC servo motor velocity dynamics.
The sixth set of benchmarks contains a well-studied discrete non-minimal phase model. Non-minimal phase models cause additional difficulties for the design of stable controllers.
The seventh set of benchmarks describes the discrete model for the Helicopter Longitudinal Motion, which provides the longitudinal motion dynamics of a helicopter.
The eighth set of benchmarks contains the discrete model for the known Inverted Pendulum, which describes a pendulum dynamics with its center of mass above its pivot point.
The ninth set of benchmarks contains the Magnetic Suspension discrete model, which describes the dynamics of a mass that levitates with support only of a magnetic field.
The last set of benchmarks contains the Computer Tape Driver discrete model, which describes a system to read and write data on a storage device.

Results: https://docs.google.com/spreadsheets/d/e/2PACX-1vRQDfOY26IHw4gxQFDaRbWVYm-bN4hGOo8d6VZCWiVjSG_nj7qGa6CyDm4phgL97WZNmeXvH-hodhNP/pubhtml#

实验设置：
实验在配备以下硬件配置的计算机上执行：Intel Core i7-2600 3.40 GHz 处理器，24 GB 内存，以及 Ubuntu 64 位操作系统。实验使用 Linux 中的 times 命令来测量每个基准测试所使用的 CPU 时间。运行时间限制为一小时（即 3600 秒）。
基准测试描述：
《IEEE 计算机学报》基准测试：从 Keel, L.H. 和 Bhattacharyya, S.P. 1997 年发表的《稳健、脆弱或最优？IEEE 自动控制学报，42，1098–1105》中提取了 4 个数字系统（控制器和植物）。所有数字系统均设计为传递函数格式，而离散化的植物和控制器由 Bessa, I. V. 等人在《IEEE 计算机学报，v.66(3)，pp. 545-552，2017》中发布。
ACM 国际混合系统计算与控制会议（HSCC）基准测试：
第一组基准测试采用汽车的巡航控制系统的离散模型，并考虑了滚动摩擦、空气动力学阻力和重力扰动力。
第二组基准测试考虑了一个简单弹簧-质量阻尼器的离散模型。
第三组基准测试使用了卫星姿态动力学的离散模型，该模型需要姿态控制以实现天线和传感器相对于地球的定向。
第四和第五组基准测试描述了直流伺服电机速度动力学的离散模型。
第六组基准测试包含了一个经过深入研究的不最小相位移模型。不最小相位移模型为稳定控制器的设计带来了额外的困难。
第七组基准测试描述了直升机纵向运动的离散模型，它提供了直升机的纵向运动动力学。
第八组基准测试包含了已知的倒立摆的离散模型，它描述了一个质心位于支点之上摆的运动动力学。
第九组基准测试包含了磁悬浮的离散模型，它描述了一个仅由磁场支持的悬浮质量动力学。
最后一组基准测试包含了计算机磁带驱动器的离散模型，它描述了一个在存储设备上读写数据的系统。
结果：[结果链接]https://docs.google.com/spreadsheets/d/e/2PACX-1vRQDfOY26IHw4gxQFDaRbWVYm-bN4hGOo8d6VZCWiVjSG_nj7qGa6CyDm4phgL97WZNmeXvH-hodhNP/pubhtml#]