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

Published: 16 Mar 2019 | Version 1 | DOI: 10.17632/83w8k935fd.1

Description of this data

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.


Experiment data files

Steps to reproduce


(1) You need to install the Eigen library (e.g., eigen3, eigen3-static, and eigen3-devel depending on your distribution).

(2) Make sure that you have installed GCC version 5.4 (or higher).

(3) Execute the following commands in a shell terminal:

sudo apt-get install build-essential libc6-dev-i386 libeigen3-dev libboost-dev -y


(1) Download the data file "", and unzip in some directory in your computer.

(2) After the extraction of the file "", perform the following command in a shell terminal:


(3) Then, DSVerifier 2.0 will be installed on your computer, and the experiments will start automatically.

Please, visit in case of any doubts.

Related links

Latest version

  • Version 1


    Published: 2019-03-16

    DOI: 10.17632/83w8k935fd.1

    Cite this dataset

    Chaves, Lennon; Bessa, Iury; Ismail, Hussama; Cordeiro, Lucas; Lima Filho, Eddie (2019), “Verifying Fragility in Digital Systems with Uncertainties using DSVerifier v2.0”, Mendeley Data, v1


Views: 31
Downloads: 4


The University of Manchester, Universidade Federal do Amazonas


Computer Science, Software Engineering, Control Systems, Embedded System, Model Checking, Formal Verification


CC BY 4.0 Learn more

The files associated with this dataset are licensed under a Creative Commons Attribution 4.0 International licence.

What does this mean?
You can share, copy and modify this dataset so long as you give appropriate credit, provide a link to the CC BY license, and indicate if changes were made, but you may not do so in a way that suggests the rights holder has endorsed you or your use of the dataset. Note that further permission may be required for any content within the dataset that is identified as belonging to a third party.