Last change
on this file since 66 was
66,
checked in by cecile, 12 years ago
|
refinement with property first part
|
File size:
2.2 KB
|
Rev | Line | |
---|
[66] | 1 | We 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}. |
---|
[64] | 2 | |
---|
[66] | 3 | |
---|
| 4 | We 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. |
---|
| 5 | |
---|
| 6 | |
---|
| 7 | \medskip |
---|
| 8 | |
---|
| 9 | \begin{table} [h] |
---|
| 10 | %\hspace*{-8mm} |
---|
| 11 | \begin{tabular}{cccc} |
---|
| 12 | |
---|
| 13 | \toprule |
---|
| 14 | \textbf{VCI} & \emph{Verification} & \emph{Verification} & \emph{Refinement} \\ |
---|
| 15 | \textbf{-PI}& \emph{Technique} & \emph{Time (s)} & \emph{Iteration} \\ |
---|
| 16 | \midrule |
---|
| 17 | \midrule |
---|
| 18 | & Prop. Selection & 2.2 & 1 \\ |
---|
| 19 | $\phi_1$ & Incremental & 18.1 & 0 \\ |
---|
| 20 | & Standard MC & 14.9 & - \\ |
---|
| 21 | \midrule |
---|
| 22 | & Prop\_Selection & 1.0 & 0 \\ |
---|
| 23 | $\phi_2$ & Incremental & 168.0 & 467 \\ |
---|
| 24 | & Standard MC & 14.9 & - \\ |
---|
| 25 | \bottomrule |
---|
| 26 | |
---|
| 27 | \end{tabular} |
---|
| 28 | |
---|
| 29 | \caption{\label{TabVCI_PI} Results on VCI-PI platform } |
---|
| 30 | \end{table} |
---|
| 31 | |
---|
| 32 | %\medskip |
---|
| 33 | |
---|
| 34 | \begin{table} [h] |
---|
| 35 | %\hspace*{-8mm} |
---|
| 36 | \begin{tabular}{cccc} |
---|
| 37 | |
---|
| 38 | \toprule |
---|
| 39 | \textbf{CAN} & \emph{Verification} & \emph{Verification} & \emph{Refinement} \\ |
---|
| 40 | \textbf{Bus} & \emph{Technique} & \emph{Time (s)} & \emph{Iteration} \\ |
---|
| 41 | \midrule |
---|
| 42 | \midrule |
---|
| 43 | & Prop. Selection & & \\ |
---|
| 44 | $\phi_1$ & Incremental & >1 day & 0 \\ |
---|
| 45 | & Standard MC & 51.9 & - \\ |
---|
| 46 | \midrule |
---|
| 47 | & Prop\_Selection & & \\ |
---|
| 48 | $\phi_2$ & Incremental & 57.3 & 0 \\ |
---|
| 49 | & Standard MC & 2.2 & - \\ |
---|
| 50 | \bottomrule |
---|
| 51 | |
---|
| 52 | \end{tabular} |
---|
| 53 | |
---|
| 54 | \caption{\label{TabCANBus} Results on CAN Bus platform } |
---|
| 55 | \end{table} |
---|
| 56 | |
---|
| 57 | \medskip |
---|
| 58 | |
---|
| 59 | Table 1 shows the... |
---|
| 60 | \TODO{Comments about Table 1, Table 2 and conclusion of Experimental Results} |
---|
| 61 | |
---|
| 62 | |
---|
Note: See
TracBrowser
for help on using the repository browser.