Changeset 89 for papers/FDL2012/exp_results.tex
- Timestamp:
- Apr 6, 2012, 4:44:06 PM (12 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/exp_results.tex
r88 r89 1 We 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}. 1 We have conducted preliminary experiments to test and compare the performance 2 of our strategy with existing abstraction-refinement techniques available in 3 VIS. There are several abstraction-refinement techniques implemented in VIS 4 accessible 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 7 techniques, \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}. 2 8 3 9 … … 115 121 116 122 117 In Table \ref{TabVerif}, we compare the execution time between our technique (Prop. Select.), \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. 123 In Table \ref{TabVerif}, we compare the execution time and the number of refinment 124 between 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 127 enabled 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 129 version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of 130 27 verifed components properties to be selected in VCI-PI plateform. 131 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. 118 132 119 133 120 In 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. 134 In 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 137 our disposal 103 verified component properties and after the selection process 138 for the initial abstraction, 3 selected component properties were sufficient 139 to verify both global properties without refinement. 121 140 122 Globally, 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 themore connected components, in contrary to the other two methods, our computation time remains stable.141 Globally, 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. 123 142 124 143
Note: See TracChangeset
for help on using the changeset viewer.