Changeset 71 for papers/FDL2012


Ignore:
Timestamp:
Mar 22, 2012, 7:15:07 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

File:
1 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/exp_results.tex

    r66 r71  
    11We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our abstraction representation requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}.
    2 
    32
    43We 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 and a CAN bus. The results have been obtained on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.
    54
    65
    7 \medskip
     6\begin{table*} [ht]
     7\hspace*{10mm}
     8\begin{tabular}{clccccc}
     9
     10\toprule
     11\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
     12\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
     13\midrule
     14\midrule
     15               & 1 Master-1 Slave   & 308 & 599 & 33 442   & 3.64116e+06 & 41.49 \\
     16 Concrete      & 2 Masters-1 Slave  & 439 & 186 & 75 210   & 73282       & 14.36 \\
     17  Model        & 4 Masters-1 Slave  & 709 & 408 & 156 657  & 2.15076e+07 & 414.38 \\
     18               & 4 Masters-2 Slaves & 883 & 597 & 217 797  & 3.22215e+10 & 4064.09 \\
     19 \midrule
     20 \midrule
     21 Final         & 1 Master-1 Slave   & 197 & 2   &  76   &  5.03316e+07  & 0.01 \\
     22 Abstract      & 2 Masters-1 Slave  & 301 & 2   &  99   &  4.12317e+11  & 0.02 \\
     23 Model         & 4 Masters-1 Slave  & 501 & 2   & 147   &  3.45876e+18  & 0.03\\
     24 for $\phi_1$  & 4 Masters-2 Slaves & xx  & 2   & xxx   &  xxx          & xxxx \\
     25\midrule
     26 Final         & 1 Master-1 Slave   & 194 & 1   & 50    &  2.62144e+07  & 0 \\
     27 Abstract      & 2 Masters-1 Slave  & 298 & 1   & 73    &  2.14748e+11  & 0.01 \\
     28 Model         & 4 Masters-1 Slave  & 498 & 1   & 121   &  1.80144e+18  & 0.02 \\
     29 for $\phi_2$  & 4 Masters-2 Slaves & xxx & x   & xxx   &  xxx          & xxx \\
     30\bottomrule 
     31\bottomrule
     32\end{tabular}
     33 
     34\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform}
     35\end{table*}
     36%\medskip
     37
     38
     39\begin{table*} [ht]
     40\hspace*{12mm}
     41\begin{tabular}{cccccc}
     42
     43\toprule
     44\textbf{CAN Bus}      & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
     45\textbf{Platform}     &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
     46\midrule
     47\midrule
     48 Concrete Model   & 838     & 182     & 212550    & 2.87296e+08      & 167.9 \\     
     49 \midrule
     50 \midrule
     51 Final Abstract Model for $\phi_1$  & xx  & 2   & xxx   &  xxx       & xxxx \\
     52\midrule
     53 Final Abstract Model for $\phi_2$  & xx  & 2   & xxx   &  xxx       & xxxx \\
     54\bottomrule 
     55\bottomrule
     56\end{tabular}
     57 
     58\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
     59\end{table*}
     60
    861
    962\begin{table} [h]
    … …  
    1265
    1366\toprule
    14 \textbf{VCI} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\
    15  \textbf{-PI}& \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
     67\emph{Global}   &\emph{Verification} & \emph{Refinement}  & \emph{Verif.}  \\
     68\emph{Property} & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\
    1669\midrule
    1770\midrule
    18              & Prop. Selection &    2.2    & 1 \\
    19  $\phi_1$   & Incremental      &  18.1    & 0    \\
    20              & Standard MC    &  14.9    & - \\
     71\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
     72                 & Prop. Selection   & 1    &    2.2     \\
     73 $\phi_1$   & Incremental       & 0    &   18.1        \\
     74            & Standard MC       & -    &   14.9     \\
    2175\midrule
    22              & Prop\_Selection &     1.0    & 0 \\
    23  $\phi_2$   & Incremental      & 168.0    & 467    \\
    24              & Standard MC    &   14.9    & - \\
     76                 & Prop. Selection   & 0    &     1.0     \\
     77 $\phi_2$   & Incremental       & 467  &   168.0         \\
     78                 & Standard MC       & -    &    14.9      \\
     79\midrule   
     80\midrule
     81\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
     82                 & Prop. Selection   & 1    &    2.0     \\
     83 $\phi_1$   & Incremental       & 0    &    1.3        \\
     84            & Standard MC       & -    &    1.5     \\
     85\midrule
     86                 & Prop. Selection   & 0    &    1.0    \\
     87 $\phi_2$   & Incremental       & 0    &   15.3       \\
     88                 & Standard MC       & -    &   14.6    \\
     89\midrule
     90\midrule 
     91\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\
     92                 & Prop. Selection   & 1    &    2.1     \\
     93 $\phi_1$   & Incremental       & 0    &    6.8        \\
     94            & Standard MC       & -    &  175.5     \\
     95\midrule
     96                 & Prop. Selection   &  0    &   1.0 \\
     97 $\phi_2$   & Incremental       &  0    &   7.5    \\
     98                 & Standard MC       &  -    & 195.1 \\
     99\midrule
     100\midrule
     101\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\
     102                                & Prop. Selection   & 1   &  xxx     \\
     103 $\phi_1$   & Incremental       & xxx &  xxx         \\
     104            & Standard MC       & -   &  2231.3    \\
     105\midrule
     106            & Prop. Selection   & 0   &  xxx\\
     107 $\phi_2$   & Incremental       & N/A &  >1 day    \\
     108            & Standard MC       & -   &  12814.1 \\
     109\bottomrule       
    25110\bottomrule
    26111
    27112\end{tabular}
    28113 
    29 \caption{\label{TabVCI_PI} Results on VCI-PI platform }
     114\caption{\label{TabVCI_PI} Results on the VCI-PI platform }
    30115\end{table}
    31116
    … …  
    34119\begin{table} [h]
    35120%\hspace*{-8mm}
    36 \begin{tabular}{cccc}
     121\begin{tabular}{lcccc}
    37122
    38123\toprule
    39 \textbf{CAN} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\
    40 \textbf{Bus}  & \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
     124\emph{Global}  & \emph{Verification} & \emph{Refinement} & \emph{Verif.}  \\
     125\emph{Property}  & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\
    41126\midrule
    42127\midrule
    43               & Prop. Selection  &             &       \\
    44  $\phi_1$   & Incremental       &  >1 day  & 0    \\
    45               & Standard MC     &  51.9    & - \\
     128                 & Prop. Selection  &  xxx        &  xxx     \\
     129 $\phi_3$   & Incremental      & N/A            &  >1 day \\
     130                 & Standard MC      & -                         &  51.9    \\
    46131\midrule
    47              & Prop\_Selection &              &  \\
    48  $\phi_2$   & Incremental      &   57.3    & 0   \\
    49              & Standard MC     &     2.2    & - \\
     132                 & Prop. Selection   &  xxx       &  xxx \\
     133 $\phi_4$   & Incremental       & 0          &   57.3     \\
     134                 & Standard MC       & -          &    2.2    \\
    50135\bottomrule
    51136
    52137\end{tabular}
    53138 
    54 \caption{\label{TabCANBus} Results on CAN Bus platform }
     139\caption{\label{TabCANBus} Results on the CAN Bus platform }
    55140\end{table}
    56141
Note: See TracChangeset for help on using the changeset viewer.