source: papers/FDL2012/exp_results.tex @ 103

Last change on this file since 103 was 101, checked in by syed, 12 years ago

final

File size: 7.9 KB
Line 
1We have conducted preliminary experiments to test and compare the performance
2of our strategy with existing 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\_verification} commands. However, among the available
7techniques, \emph{incremental\_ctl\_verification} 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\footnotesize
17\begin{tabular}{cclcccc}
18
19\toprule 
20\multicolumn{3}{l}{\textbf{Experiment}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
21\multicolumn{3}{l}{\textbf{Platform}}     &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
22\midrule
23\midrule
24                        &               & 1 Master-1 Slave   & 304  & 7207     & 4.711e+3    & 6.36 \\
25                        & Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
26                        &  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
27                        &               & 4 Masters-2 Slaves & 895  & 238990   & 5.708e+15   & 68882.3\footnotemark[1] \\
28\cline{2-7} 
29\cline{2-7}
30                        & Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
31VCI-PI  & Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
32                        & Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
33                        & for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
34\cline{2-7}
35                        & Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
36                        & Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
37                        & Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
38                        & for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
39% \midrule
40 \midrule
41                        &\multicolumn{2}{c}{Concrete Model}                                          & 822     & 161730      & 3.7354e+07     & 300.12 \\     
42\cline{2-7}
43\cline{2-7}
44CAN Bus  &\multicolumn{2}{c}{Final Abstract Model for $\phi_3$}  & 425   & 187   &  1.66005e+12       & 0.03 \\
45\cline{2-7}
46                        &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
47\bottomrule 
48%\bottomrule
49\end{tabular}
50\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform}
51\end{table*}
52
53%\footnotetext[1]{Computed on a calculation server.}
54
55
56\begin{table} [h]
57%\hspace*{-8mm}
58\small
59\addtolength{\tabcolsep}{-1pt}
60\begin{tabular}{ccccc}
61\toprule 
62\emph{Experim.}     &\emph{Global}   &\emph{Verification} & \emph{Refine.}  & \emph{Verif.}  \\
63\emph{Platform}         &\emph{Property} & \emph{Technique}  & \emph{Iter.}  & \emph{Time (s)}      \\ 
64\midrule
65\midrule
66%\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
67                                &                 & Prop. Select.   & 1    &    2.2     \\
68VCI-PI:         & $\phi_1$   & Incremental       & 0    &    6.3        \\
691 Master                &            & Standard MC       & -    &    6.06     \\
70\cline{2-5}
71-                               &                 & Prop. Select.   & 0    &     1.0     \\
721 Slave         & $\phi_2$   & Incremental       & 562  &   200.9         \\
73                                &                 & Standard MC       & -    &    6.13      \\
74\midrule   
75%\midrule
76                                &                 & Prop. Select.   & 1    &    2.0     \\
77VCI-PI:                 & $\phi_1$   & Incremental       & 0    &   20.4        \\
782 Masters       &            & Standard MC       & -    &   37.9     \\
79\cline{2-5}
80-                               &                 & Prop. Select.   & 0    &    1.0    \\
811 Slave         & $\phi_2$   & Incremental       & 74   &  786.3        \\
82                                &                 & Standard MC       & -    &   39.4    \\
83\midrule
84%\midrule 
85
86                                &                 & Prop. Select.   &  1   &    2.1     \\
87VCI-PI:         & $\phi_1$   & Incremental       &  0   &  261.6      \\
884 Masters       &            & Standard MC       &  -   &  >1 day     \\
89\cline{2-5}
90-                  &              & Prop. Select.   &  0   &   1.0    \\
911 Slave         & $\phi_2$   & Incremental       &  0   &   263.5     \\
92                                &                 & Standard MC       &  -   &   >1 day   \\
93\midrule 
94%\midrule
95
96                                &                                & Prop. Select.   & 1          &  2.2     \\
97VCI-PI:     & $\phi_1$   & Incremental       & N/A      &  >1 day    \\
984 Masters       &            & Standard MC       & -    &  >1 day   \\
99\cline{2-5}
100  -                &            & Prop. Select.   & 0           &  1.1\\
1012 Slaves                & $\phi_2$   & Incremental       & N/A  &  >1 day    \\
102                                &            & Standard MC       & -    &  >1 day\\
103\midrule 
104%\midrule
105                &                 & Prop. Select.   &  0     &  1.02     \\
106                                &$\phi_3$    & Incremental       & N/A    &  >1 day   \\
107CAN                     &                 & Standard MC       & -       &  2645.4    \\
108\cline{2-5}
109Bus                     &                 & Prop. Select.   &  0     &   1.01     \\
110                                &$\phi_4$    & Incremental       & N/A    &  >1 day    \\
111                                &                 & Standard MC       & -      &   1678.1    \\   
112
113\bottomrule       
114%\bottomrule
115
116\end{tabular}
117
118\caption{\label{TabVerif} Verification Results  }
119\end{table}
120
121
122In Table \ref{TabVerif}, we compare the execution time and the number of refinement
123between our technique (Prop. Select.), \emph{incremental\_ctl\_verification}
124(Incremental) and the standard model checking (Standard MC) computed using the
125\emph{model\_check} command in VIS (Note: Dynamic variable ordering has been
126enabled with sift method). For the VCI-PI platform, the global property
127$\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger
128version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of
12926 verified components properties to be selected in the VCI-PI platform.
130In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
131
132
133In the case of the CAN bus platform, the global property $\phi_3$ is the type
134$AG(((p'=1)*(q'=1)*AF(r_1=1)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4
135= AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow AG((s_2=0)*(t_2=0)))$. We have at
136our disposal 103 verified component properties and after the selection process
137for the initial abstraction, 3 selected component properties were sufficient
138to verify both global properties without refinement.
139
140Globally, we can see that our technique, for these examples, 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. This is mainly due to the fact that for small number of properties, our abstraction is generated almost instantly and as only pertinent properties are selected, not many refinement iterations are required in order to complete the verification process. It is also important to note that the properties tested are simple and we have in our property selection list the local properties required to satisfy the global property.
141
142
143
144%\medskip
145
146
Note: See TracBrowser for help on using the repository browser.