![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 83
- Timestamp:
- Apr 5, 2012, 1:59:16 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 4 edited
-
FDL2012.tex (modified) (1 diff)
-
exp_results.tex (modified) (5 diffs)
-
introduction.tex (modified) (3 diffs)
-
myBib.bib (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.tex
r80 r83 33 33 34 34 35 \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinementprocess}35 \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process} 36 36 \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN} 37 37 % \thanks{This work was supported by...}} -
papers/FDL2012/exp_results.tex
r80 r83 14 14 \midrule 15 15 \midrule 16 & 1 Master-1 Slave & 30 8 & 33 442 & 3.64116e+06 & 41.49\\17 Concrete & 2 Masters-1 Slave & 4 53 & 140297 & 2.42518e+11 & 1922.75\\18 Model & 4 Masters-1 Slave & 7 37 & N/A & N/A & >3days\\19 & 4 Masters-2 Slaves & 911 & N/A & N/A & > 3days\\16 & 1 Master-1 Slave & 304 & 7207 & 4.711e+3 & 6.36 \\ 17 Concrete & 2 Masters-1 Slave & 445 & 24406 & 7.71723e+06 & 35.2 \\ 18 Model & 4 Masters-1 Slave & 721 & 84118 & 3.17332e+12 & 2818.3 \\ 19 & 4 Masters-2 Slaves & 911 & N/A & N/A & >1 day \\ 20 20 \midrule 21 21 \midrule … … 48 48 \midrule 49 49 \midrule 50 Concrete Model & 822 & 1 40586 & 3.7354e+07 & 294.6\\50 Concrete Model & 822 & 161730 & 3.7354e+07 & 300.12 \\ 51 51 \midrule 52 52 \midrule … … 75 75 \multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\ 76 76 & Prop. Selection & 1 & 2.2 \\ 77 $\phi_1$ & Incremental & 0 & 18.1\\78 & Standard MC & - & 14.9\\77 $\phi_1$ & Incremental & 0 & 6.3 \\ 78 & Standard MC & - & 6.06 \\ 79 79 \midrule 80 80 & Prop. Selection & 0 & 1.0 \\ 81 $\phi_2$ & Incremental & 467 & 168.0\\82 & Standard MC & - & 14.9\\81 $\phi_2$ & Incremental & 562 & 200.9 \\ 82 & Standard MC & - & 6.13 \\ 83 83 \midrule 84 84 \midrule 85 85 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 86 86 & Prop. Selection & 1 & 2.0 \\ 87 $\phi_1$ & Incremental & 0 & 107.7\\88 & Standard MC & - & 1181.8\\87 $\phi_1$ & Incremental & 0 & 20.4 \\ 88 & Standard MC & - & 37.9 \\ 89 89 \midrule 90 90 & Prop. Selection & 0 & 1.0 \\ 91 $\phi_2$ & Incremental & 0 & 108.5\\92 & Standard MC & - & 1103.3\\91 $\phi_2$ & Incremental & 74 & 786.3 \\ 92 & Standard MC & - & 39.4 \\ 93 93 \midrule 94 94 \midrule 95 95 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 96 & Prop. Selection & 1& 2.1 \\97 $\phi_1$ & Incremental & N/A & >3 days\\98 & Standard MC & - & >3 days\\96 & Prop. Selection & 1 & 2.1 \\ 97 $\phi_1$ & Incremental & 0 & 261.6 \\ 98 & Standard MC & - & >1 day \\ 99 99 \midrule 100 & Prop. Selection & 0 & 1.0\\101 $\phi_2$ & Incremental & N/A & >3 days\\102 & Standard MC & - & >3 days\\100 & Prop. Selection & 0 & 1.0 \\ 101 $\phi_2$ & Incremental & 0 & 263.5 \\ 102 & Standard MC & - & >1 day \\ 103 103 \midrule 104 104 \midrule 105 105 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 106 106 & Prop. Selection & 1 & 2.2 \\ 107 $\phi_1$ & Incremental & N/A & > 3 days\\108 & Standard MC & - & > 3 days\\107 $\phi_1$ & Incremental & N/A & >1 day \\ 108 & Standard MC & - & >1 day \\ 109 109 \midrule 110 110 & Prop. Selection & 0 & 1.1\\ 111 $\phi_2$ & Incremental & N/A & > 3 days\\112 & Standard MC & - & > 3 days\\111 $\phi_2$ & Incremental & N/A & >1 day \\ 112 & Standard MC & - & >1 day\\ 113 113 \bottomrule 114 114 \bottomrule … … 132 132 \midrule 133 133 & Prop. Selection & 0 & 1.02 \\ 134 $\phi_3$ & Incremental & N/A & N/A\\135 & Standard MC & - & N/A\\134 $\phi_3$ & Incremental & N/A & >1 day \\ 135 & Standard MC & - & 2645.4 \\ 136 136 \midrule 137 & Prop. Selection & 0 & 1.01 \\138 $\phi_4$ & Incremental & N/A & N/A\\139 & Standard MC & - & N/A\\137 & Prop. Selection & 0 & 1.01 \\ 138 $\phi_4$ & Incremental & N/A & >1 day \\ 139 & Standard MC & - & 1678.1 \\ 140 140 \bottomrule 141 141 … … 147 147 148 148 149 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), 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.149 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), \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. 150 150 151 151 152 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)) -> AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) ->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.152 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. 153 153 154 154 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 the more connected components, in contrary to the other two methods, our computation time remains stable. -
papers/FDL2012/introduction.tex
r80 r83 22 22 23 23 24 \textbf{\emph{Related Works :}} Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity.24 \textbf{\emph{Related Works :}} Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}. 25 25 26 26 … … 33 33 34 34 35 Recently, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification \cite{pwk2009-date}. The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems. 35 Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abtraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time. 36 37 38 In \cite{pwk2009-date}, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification . The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems. 36 39 37 40 … … 40 43 41 44 %\subsection{Contribution} 42 \textbf{\emph{Contribution :}} We would like to contribute to the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. 45 \textbf{\emph{Contribution :}} In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. We propose a technique to classify component properties according to their pertinency towards the global property, thus, enabling a better selection of properties for the initial abstraction generation. Futhermore, in the case where the verification is not conclusive, we propose a technique guided by the counterexample given by the model-checker to select supplementary properties to improve the abstraction. 46 43 47 44 48 In the next section, we will give an overview of our framework and introduce the notations that will be used later. The rest of the paper is organized as follows: section 3 details our strategy of refinement. Section 4 presents the experimentation results and finally, section 5 draws the conclusions and summarize our possible future works. -
papers/FDL2012/myBib.bib
r76 r83 167 167 title = "{Verified Systems by Composition from Verified Components} ", 168 168 booktitle = " In ESEC/FSE 2003: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference", 169 169 pages = {227-286}, 170 170 address = "Helsinki, Finland", 171 171 year = 2003, 172 172 publisher = "ACM Press" 173 173 } 174 175 176 @conference{ LiSunXieSong08compAbsRef, 177 author = "J. Li and X. Sun and F. Xie and X. Song", 178 title = "{Component-Based Abstraction Refinement} ", 179 booktitle = "In Proc. of 10th International Conference on Software Reuse (ICSR)", 180 pages = {39-51}, 181 address = "Beijing, China", 182 year = 2008, 183 publisher = "Springer-Verlag" 184 } 185 174 186 175 187 … … 297 309 298 310 311 @ARTICLE { Sharygina_al12PreciseApprox, 312 AUTHOR = { Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich }, 313 TITLE = { {An Abstraction Refinement Approach Combining Precise and Approximated Techniques} }, 314 JOURNAL = { International Journal on Software Tools for Technology Transfer (STTT) }, 315 VOLUME = {14}, 316 PAGES ={1-14}, 317 YEAR = { 2012}, 318 } 319 320 299 321 @conference{ microsoft04SLAM, 300 322 author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani", … … 324 346 YEAR = { 2009 }, 325 347 PUBLISHER = { ACM }, 326 PAGES = { 1692- -1697 },348 PAGES = { 1692-1697 }, 327 349 } 328 350
Note: See TracChangeset
for help on using the changeset viewer.
