source: papers/FDL2012/exp_results.tex @ 84

Last change on this file since 84 was 83, checked in by syed, 13 years ago

/papers/FDL2012/

File size: 8.0 KB
Line 
1We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. There several abstraction-refinement techniques implemented in VIS accessible via \emph{approximate\_model\_check}, \emph{iterative\_model\_check}, \emph{check\_invariant} and \emph{incremental\_ctl\_model\_check} commands. However, among the techniques available, \emph{incremental\_ctl\_model\_check} is the only abstraction-refinement technique that supports CTL formulas and fairness constraints which are necessary in our test platforms. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}.
2
3
4We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes on a CAN bus. Table \ref{StatsVCI_PI} and Table \ref{StatsCAN_Bus} give the size and the statistics concerning the VCI-PI platform and CAN bus platform respectively. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.
5
6
7\begin{table*} [ht]
8\hspace*{17mm}
9\begin{tabular}{clcccc}
10
11\toprule 
12\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
13\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
14\midrule
15\midrule
16               & 1 Master-1 Slave   & 304  & 7207     & 4.711e+3    & 6.36 \\
17 Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
18  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
19               & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >1 day \\
20 \midrule 
21 \midrule
22 Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
23 Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
24 Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
25 for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
26\midrule 
27 Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
28 Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
29 Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
30 for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
31\bottomrule 
32\bottomrule
33\end{tabular}
34 
35\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform}
36\end{table*}
37%\medskip
38
39
40
41\begin{table*} [ht]
42\hspace*{15mm}
43\begin{tabular}{ccccc}
44
45\toprule 
46\textbf{CAN Bus}      & \emph{Number of}       & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
47\textbf{Platform}     &\emph{BDD Variables}    & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
48\midrule
49\midrule
50 Concrete Model                     & 822     & 161730      & 3.7354e+07     & 300.12 \\     
51 \midrule 
52 \midrule
53 Final Abstract Model for $\phi_1$  & 425   & 187   &  1.66005e+12       & 0.03 \\
54\midrule 
55 Final Abstract Model for $\phi_2$  & 425   & 187   &  1.66005e+12       & 0.04 \\
56\bottomrule 
57\bottomrule
58\end{tabular}
59 
60\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
61\end{table*}
62
63
64
65
66\begin{table} [h]
67%\hspace*{-8mm}
68\begin{tabular}{cccc}
69
70\toprule 
71\emph{Global}   &\emph{Verification} & \emph{Refinement}  & \emph{Verif.}  \\
72\emph{Property} & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\ 
73\midrule
74\midrule
75\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
76                 & Prop. Selection   & 1    &    2.2     \\
77 $\phi_1$   & Incremental       & 0    &    6.3        \\
78            & Standard MC       & -    &    6.06     \\
79\midrule
80                 & Prop. Selection   & 0    &     1.0     \\
81 $\phi_2$   & Incremental       & 562  &   200.9         \\
82                 & Standard MC       & -    &    6.13      \\
83\midrule   
84\midrule
85\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
86                 & Prop. Selection   & 1    &    2.0     \\
87 $\phi_1$   & Incremental       & 0    &   20.4        \\
88            & Standard MC       & -    &   37.9     \\
89\midrule
90                 & Prop. Selection   & 0    &    1.0    \\
91 $\phi_2$   & Incremental       & 74   &  786.3        \\
92                 & Standard MC       & -    &   39.4    \\
93\midrule
94\midrule 
95\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\ 
96                 & Prop. Selection   &  1   &    2.1     \\
97 $\phi_1$   & Incremental       &  0   &  261.6      \\
98            & Standard MC       &  -   &  >1 day     \\
99\midrule
100                 & Prop. Selection   &  0   &   1.0    \\
101 $\phi_2$   & Incremental       &  0   &   263.5     \\
102                 & Standard MC       &  -   &   >1 day   \\
103\midrule 
104\midrule
105\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
106                                & Prop. Selection   & 1   &  2.2     \\
107 $\phi_1$   & Incremental       & N/A &  >1 day    \\
108            & Standard MC       & -   &  >1 day   \\
109\midrule
110            & Prop. Selection   & 0   &  1.1\\
111 $\phi_2$   & Incremental       & N/A &  >1 day    \\
112            & Standard MC       & -   &  >1 day\\
113\bottomrule       
114\bottomrule
115
116\end{tabular}
117 
118\caption{\label{TabVCI_PI} Results on the VCI-PI platform }
119\end{table}
120
121%\medskip
122
123
124\begin{table} [h]
125%\hspace*{-8mm}
126\begin{tabular}{lcccc}
127
128\toprule 
129\emph{Global}  & \emph{Verification} & \emph{Refinement} & \emph{Verif.}   \\ 
130\emph{Property}  & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}       \\
131\midrule
132\midrule
133                 & Prop. Selection  &  0          &  1.02     \\
134 $\phi_3$   & Incremental      & N/A            &  >1 day   \\
135                 & Standard MC      & -                         &  2645.4    \\
136\midrule
137                 & Prop. Selection   &  0         &   1.01     \\
138 $\phi_4$   & Incremental       & N/A        &  >1 day    \\
139                 & Standard MC       & -          &   1678.1    \\
140\bottomrule
141
142\end{tabular}
143 
144\caption{\label{TabCANBus} Results on the CAN Bus platform }
145\end{table}
146
147
148
149In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), \emph{incremental\_ctl\_verification} (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
150
151
152In the case of the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)*AF(r_1=1)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow AG((s_2=0)*(t_2=0)))$. We have at our disposal 103 verified component properties and after the selection process, 3 selected component properties were sufficient to verify both global properties.
153
154Globally, we can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding the more connected components, in contrary to the other two methods, our computation time remains stable.
155
156
157
158%\medskip
159
160
Note: See TracBrowser for help on using the repository browser.