source: papers/FDL2012/exp_results.tex @ 91

Last change on this file since 91 was 89, checked in by cecile, 13 years ago

corrections typos and co
File size: 7.4 KB
Line 
1We have conducted preliminary experiments to test and compare the performance
2of our strategy with existing abstraction-refinement techniques available in
3VIS. There are several abstraction-refinement techniques implemented in VIS
4accessible via \emph{approximate\_model\_check},
5\emph{iterative\_model\_check}, \emph{check\_invariant} and
6\emph{incremental\_ctl\_model\_check} commands. However, among the available
7techniques, \emph{incremental\_ctl\_model\_check} is the only one 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}.
8
9
10We 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{StatsPlatform} gives the size and the statistics concerning the VCI-PI platform and CAN bus platform verified. 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.
11
12
13\begin{table*} [ht]
14\hspace*{15mm}
15\small
16\begin{tabular}{cclcccc}
17
18\toprule 
19\multicolumn{3}{l}{\textbf{Experiment}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
20\multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
21\midrule
22\midrule
23                        &               & 1 Master-1 Slave   & 304  & 7207     & 4.711e+3    & 6.36 \\
24                        & Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
25                        &  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
26                        &                & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >1 day \\
27\cline{2-7} 
28\cline{2-7}
29                        & Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
30VCI-PI  & Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
31                        & Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
32                        & for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
33\cline{2-7}
34                        & Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
35                        & Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
36                        & Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
37                        & for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
38 \midrule 
39 \midrule
40                        &\multicolumn{2}{c}{Concrete Model}                                      & 822     & 161730      & 3.7354e+07     & 300.12 \\     
41\cline{2-7}
42\cline{2-7}
43CAN Bus  &\multicolumn{2}{c}{Final Abstract Model for $\phi_3$}  & 425   & 187   &  1.66005e+12       & 0.03 \\
44\cline{2-7}
45                        &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
46\bottomrule 
47\bottomrule
48\end{tabular}
49
50\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform}
51\end{table*}
52
53
54
55\begin{table} [h]
56%\hspace*{-8mm}
57\small
58\addtolength{\tabcolsep}{-1pt}
59\begin{tabular}{ccccc}
60\toprule 
61\emph{Experim.}     &\emph{Global}   &\emph{Verification} & \emph{Refine.}  & \emph{Verif.}  \\
62\emph{Platform}         &\emph{Property} & \emph{Technique}  & \emph{Iter.}  & \emph{Time (s)}      \\ 
63\midrule
64\midrule
65%\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
66                                &                 & Prop. Select.   & 1    &    2.2     \\
67VCI-PI:         & $\phi_1$   & Incremental       & 0    &    6.3        \\
681 Master                &            & Standard MC       & -    &    6.06     \\
69\cline{2-5}
70-                               &                 & Prop. Select.   & 0    &     1.0     \\
711 Slave         & $\phi_2$   & Incremental       & 562  &   200.9         \\
72                                &                 & Standard MC       & -    &    6.13      \\
73\midrule   
74\midrule
75                                &                 & Prop. Select.   & 1    &    2.0     \\
76VCI-PI:                 & $\phi_1$   & Incremental       & 0    &   20.4        \\
772 Masters       &            & Standard MC       & -    &   37.9     \\
78\cline{2-5}
79-                               &                 & Prop. Select.   & 0    &    1.0    \\
801 Slave         & $\phi_2$   & Incremental       & 74   &  786.3        \\
81                                &                 & Standard MC       & -    &   39.4    \\
82\midrule
83\midrule 
84
85                                &                 & Prop. Select.   &  1   &    2.1     \\
86VCI-PI:         & $\phi_1$   & Incremental       &  0   &  261.6      \\
874 Masters       &            & Standard MC       &  -   &  >1 day     \\
88\cline{2-5}
89-                  &              & Prop. Select.   &  0   &   1.0    \\
901 Slave         & $\phi_2$   & Incremental       &  0   &   263.5     \\
91                                &                 & Standard MC       &  -   &   >1 day   \\
92\midrule 
93\midrule
94
95                                &                                & Prop. Select.   & 1          &  2.2     \\
96VCI-PI:     & $\phi_1$   & Incremental       & N/A      &  >1 day    \\
974 Masters       &            & Standard MC       & -    &  >1 day   \\
98\cline{2-5}
99  -                &            & Prop. Select.   & 0           &  1.1\\
1002 Slaves                & $\phi_2$   & Incremental       & N/A  &  >1 day    \\
101                                &            & Standard MC       & -    &  >1 day\\
102\midrule 
103\midrule
104                &                 & Prop. Select.   &  0     &  1.02     \\
105                                &$\phi_3$    & Incremental       & N/A    &  >1 day   \\
106CAN                     &                 & Standard MC       & -       &  2645.4    \\
107\cline{2-5}
108Bus                     &                 & Prop. Select.   &  0     &   1.01     \\
109                                &$\phi_4$    & Incremental       & N/A    &  >1 day    \\
110                                &                 & Standard MC       & -      &   1678.1    \\   
111
112\bottomrule       
113\bottomrule
114
115\end{tabular}
116
117\caption{\label{TabVerif} Verification Results  }
118\end{table}
119
120
121
122
123In Table \ref{TabVerif}, we compare the execution time and the number of refinment
124between our technique (Prop. Select.), \emph{incremental\_ctl\_verification}
125(Incremental) and the standard model checking (Standard MC) computed using the
126\emph{model\_check} command in VIS (Note: Dynamic variable ordering has been
127enabled with sift method). For the VCI-PI platform, the global property
128$\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger
129version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of
13027 verifed components properties to be selected in VCI-PI plateform.
131In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
132
133
134In the case of the CAN bus platform, the global property $\phi_3$ is the type
135$AG(((p'=1)*(q'=1)*AF(r_1=1)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4
136= AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow AG((s_2=0)*(t_2=0)))$. We have at
137our disposal 103 verified component properties and after the selection process
138for the initial abstraction, 3 selected component properties were sufficient
139to verify both global properties without refinement.
140
141Globally, 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  more connected components, in contrary to the other two methods, our computation time remains stable.
142
143
144
145%\medskip
146
147
Note: See TracBrowser for help on using the repository browser.