October 16, 2018

HSCC 2019 Benchmarks

Formal Verification of Non-fragile Settling-Time and Overshoot Requirements for Digital State-Feedback Control Systems: Benchmarks Results.

 

Experimental Setup:
The experiments were executed in a computer with the following hardware configurations: Intel Core i7-2600 3.40 GHz processor, 32 GB of RAM, and Linux Mint 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:

We used 16 different benchmarks and we provide information about state-space matrices A, B, and C, in Jordan-form-like, controller matrix K, required settling-time t_{\mathrm{sr}}, and required overshoot percentage PO_{\mathrm{r}}. All systems in Table below present state-space matrix D=[0] and were chosen because they tackle different scenarios regarding eigenvalues of A. There are systems of 2\textsuperscript{nd}, 3\textsuperscript{rd}, 4\textsuperscript{th} and 5\textsuperscript{th} order, with the same, different, real, and complex eigenvalues.

There are 16 experiments in open-loop configuration, 16 in closed-loop without FWL effects, and 48 in closed-loop with FWL effects, for 8, 16, and 32 bits, which amounts to $80$ verification tasks for each property (settling-time and overshoot).

Benchmarks:
Test Case Id A B C K t_{sr} PO_r
1 \begin{bmatrix} -0.5 & 1.0 \\ 0.0 & -0.5 \end{bmatrix} \begin{bmatrix} 0.0 \\ 2.5 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 \end{bmatrix} \begin{bmatrix} 0.3641 & -0.7161 \end{bmatrix} 2.5 5
2 \begin{bmatrix} -0.5 & 1.0 & 0.0 \\ 0.0 & -0.5 & 1.0 \\ 0.0 & 0.0 & -0.5 \end{bmatrix} \begin{bmatrix} -0.4 \\ 2.5 \\ -0.8 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 \end{bmatrix} \begin{bmatrix} 1.0706 \\ -0.0277 \\ 2.8996 \end{bmatrix}^T 3.5 5
3 \begin{bmatrix} -0.5 & 1.0 & 0.0 & 0.0 \\ 0.0 & -0.5 & 1.0 & 0.0 \\ 0.0 & 0.0 & -0.5 & 1.0 \\ 0.0 & 0.0 & 0.0 & -0.5 \end{bmatrix} \begin{bmatrix} 1.0 \\ 2.5 \\ 1.0 \\ 1.0 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 1.2 & 0.0 \end{bmatrix} \begin{bmatrix} 0.444 \\ -2.6941 \\ 5.7609 \\ -2.8354 \end{bmatrix}^T 4.5 30
4 \begin{bmatrix} -0.5 & 1.0 & 0.0 & 0.0 & 0.0 \\ 0.0 & -0.5 & 1.0 & 0.0 & 0.0 \\ 0.0 & 0.0 & -0.5 & 1.0 & 0.0 \\ 0.0 & 0.0 & 0.0 & -0.5 & 1.0 \\ 0.0 & 0.0 & 0.0 & 0.0 & -0.5 \end{bmatrix} \begin{bmatrix} -0.4 \\ -0.6 \\ 5.5 \\ 1.0 \\ -0.3 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.5 & 1.2 & 0.0 \end{bmatrix} \begin{bmatrix} 0.5811 \\ -2.5168 \\ 15.458 \\ -14.5328 \\ 251.9519 \end{bmatrix}^T 5.5 20
5 \begin{bmatrix} -0.5 & 0.4 \\ -0.4 & -0.5 \end{bmatrix} \begin{bmatrix} 0.0 \\ 2.5 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 \end{bmatrix} \begin{bmatrix} 0.8725 & -0.7848 \end{bmatrix} 3.0 5
6 \begin{bmatrix} -0.5 & 0.4 & 1.0 & 0.0 \\ -0.4 & -0.5 & 0.0 & 1.0 \\ 0.0 & 0.0 & -0.5 & 0.4 \\ 0.0 & 0.0 & -0.4 & -0.5 \end{bmatrix} \begin{bmatrix} 0.0 \\ 0.0 \\ 2.5 \\ 1.6 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 & 2.0 \end{bmatrix} \begin{bmatrix} -0.3248 \\ 0.804 \\ 0.694 \\ -3.2113 \end{bmatrix}^T 5.0 30
7 \begin{bmatrix} -0.5 & 0.4 & 0.0 & 0.0 \\ -0.4 & -0.5 & 0.0 & 0.0 \\ 0.0 & 0.0 & -0.8 & 0.4 \\ 0.0 & 0.0 & -0.4 & -0.8 \end{bmatrix} \begin{bmatrix} -0.4 \\ -0.6 \\ 2.5 \\ 1.6 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 & 2.0 \end{bmatrix} \begin{bmatrix} 14.8068 \\ -5.2354 \\ 4.9214 \\ -8.8323 \end{bmatrix}^T 10.0 4
8 \begin{bmatrix} -0.2 & 0.0 \\ 0.0 & -0.3 \end{bmatrix} \begin{bmatrix} -0.6 \\ 2.5 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 \end{bmatrix} \begin{bmatrix} -2.5516 & -0.873 \end{bmatrix} 1.5 8
9 \begin{bmatrix} -0.2 & 0.0 & 0.0 \\ 0.0 & -0.3 & 0.0 \\ 0.0 & 0.0 & -0.7 \end{bmatrix} \begin{bmatrix} -0.8 \\ -0.7 \\ -0.5 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 \end{bmatrix} \begin{bmatrix} 3.5127 \\ -8.0225 \\ 9.4041 \end{bmatrix} ^ T 2.0 8
10 \begin{bmatrix} -0.2 & 0.0 & 0.0 & 0.0 \\ 0.0 & -0.3 & 0.0 & 0.0 \\ 0.0 & 0.0 & -0.7 & 0.0 \\ 0.0 & 0.0 & 0.0 & -0.9 \end{bmatrix} \begin{bmatrix} -0.4 \\ 2.5 \\ 1.0 \\ -0.7 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 1.2 & 0.0 \end{bmatrix} \begin{bmatrix} -8.6418 \\ -3.8839 \\ 37.21 \\ 49.6053 \end{bmatrix}^ T 5.0 30
11 \begin{bmatrix} -0.2 & 0.0 & 0.0 & 0.0 & 0.0 \\ 0.0 & -0.3 & 0.0 & 0.0 & 0.0 \\ 0.0 & 0.0 & -0.7 & 0.0 & 0.0 \\ 0.0 & 0.0 & 0.0 & -0.9 & 0.0 \\ 0.0 & 0.0 & 0.0 & 0.0 & -0.5 \end{bmatrix} \begin{bmatrix} -0.5 \\ -0.2 \\ 2.5 \\ 2.0 \\ -0.8 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.5 & 1.2 & 0.0 \end{bmatrix} \begin{bmatrix} 34.4436 \\ -382.0806 \\ 143.6879 \\ -91.9969 \\ 299.8048 \end{bmatrix}^ T 10.0 18
12 \begin{bmatrix} 4.5 & 1.0 \\ 0.0 & 4.5 \end{bmatrix} \begin{bmatrix} 0.0 \\ 2.5 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 \end{bmatrix} \begin{bmatrix} 5.5182 & 2.9698 \end{bmatrix} 8.0 10
13 \begin{bmatrix} 1.5 & 1.0 & 0.0 \\ 0.0 & 1.5 & 1.0 \\ 0.0 & 0.0 & 1.5 \end{bmatrix} \begin{bmatrix} -0.4 \\ 2.5 \\ -0.8 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 \end{bmatrix} \begin{bmatrix} -0.7351 \\ -5.0045 \\ -18.5371 \end{bmatrix} ^ T 10.0 9
14 \begin{bmatrix} -0.5 & 0.4 & 0.0 & 0.0 \\ -0.4 & -0.5 & 0.0 & 0.0 \\ 0.0 & 0.0 & -0.8 & 0.4 \\ 0.0 & 0.0 & -0.4 & -0.8 \end{bmatrix} \begin{bmatrix} -0.4 \\ -0.6 \\ -0.4 \\ -0.6 \end{bmatrix} \begin{bmatrix} 0.0 & 2.6 & 0.0 & 2.0 \end{bmatrix} \begin{bmatrix} 12.348 \\ -5.7826 \\ 3.9751 \\ -8.0988 \end{bmatrix} ^ T 10.0 2
15 \begin{bmatrix} -0.6386 & 0.4151 \\ -0.0098 & 0.8266 \end{bmatrix} \begin{bmatrix} 0.2442 \\ 1.0745 \end{bmatrix} \begin{bmatrix} 0.1807 & 0.2076 \end{bmatrix} \begin{bmatrix} 21.8774 \\ -6.1877 \end{bmatrix} ^ T \end{bmatrix} 6.5 5
16 \begin{bmatrix} -1.0003 & -0.0002 & 0.0 \\ -8.0007 & -1.0003 & 0.0001 \\ 0.0 & 0.0 & -0.9216 \end{bmatrix} \begin{bmatrix} 0.0008 \\ 0.0016 \\ 1.9608 \end{bmatrix} \begin{bmatrix} -0.00016 & -0.0000831 & 0.000016 \end{bmatrix} \begin{bmatrix} -3911249 \\ -910.6 \\ 1593.2 \end{bmatrix} ^ T 10.5 8

Verification Results:

Benchmark ID open-loop closed-loop closed-loop-fwl  t_{sr}  PO_r
FWL format
ST OV ST OV ST OV ST OV ST OV
<4,4> <8,8> <16,16>
DM1 F F S S S S S S S S 2.5 5
DM2 F F S S F F S S S S 3.5 5
DM3 F F S S S S F S S S 4.5 30
DM4 F F S S F F F S S S 5.5 20
DM5 F F S S S S S S S S 3.0 5
DM6 F F S S F F S S S S 5.0 30
DM7 F F S S F F F F S S 10.0 4
DM8 F F S S F F F S S S 1.5 8
DM9 F F S S S S S S S S 2.0 8
DM10 F F S S F S S S S S 5.0 30
DM11 F F S S F F F F S S 10.0 18
DM12 F F S S F F S S S S 8.0 10
DM13 F F S S F F F S S S 10.0 9
DM14 F F S S S S F F S S 10.0 2
DM15 F F S S S S S S S S 6.5 5
DM16 F F S S F F F F S S 10.5 8
S = Success and F = Fail. ST = settling-time verification and OS=overshoot verification

Verification Result graphs:

Benchmark ID open-loop closed-loop closed-loop-fwl  t_{sr}  PO_r
FWL format
ST OV ST OV ST OV ST OV ST OV
<4,4> <8,8> <16,16>
DM1 2.5 5
DM2 3.5 5
DM3 4.5 30
DM4 5.5 20
DM5 3 5
DM6 5 30
DM7 10 4
DM8 1.5 8
DM9 2 8
DM10 5 30
DM11 10 18
DM12 8 10
DM13 10 9
DM14 10 2
DM15 6.5 5
DM16 10.5 8