![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 92 for papers/FDL2012
- Timestamp:
- Apr 6, 2012, 10:37:41 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 8 edited
-
FDL2012.tex (modified) (2 diffs)
-
abstraction_refinement.tex (modified) (3 diffs)
-
exp_results.tex (modified) (13 diffs)
-
framework.tex (modified) (10 diffs)
-
introduction.tex (modified) (4 diffs)
-
myBib.bib (modified) (10 diffs)
-
ordering_filter_properties.tex (modified) (5 diffs)
-
schema/our_framework_cegar_png.png (modified) (previous)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.tex
r91 r92 34 34 35 35 \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process} 36 % \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN}36 % \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ} 37 37 % \thanks{This work was supported by...}} 38 38 % \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\ … … 106 106 Kroening \cite{pwk2009-date} could help us in this direction. 107 107 108 108 %footnote for Table 1 109 \footnotetext[1]{Computed on a calculation server.} 109 110 110 111 %\begin{thebibliography} -
papers/FDL2012/abstraction_refinement.tex
r89 r92 8 8 9 9 \begin{definition} An efficient \emph{refinement} verifies the following properties: 10 \vspace*{-2mm} 10 11 \begin{enumerate} 12 \itemsep -0.3em 11 13 \item The new refinement is an over-approximation of the concrete model: 12 14 $\widehat{M} \sqsubseteq \widehat{M}_{i+1}$. … … 46 48 \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots 47 49 \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$. 50 %\vspace*{-2mm} 48 51 \begin{itemize} 52 %\topsep 0pt 53 \itemsep -0.3em 49 54 \item All its variables are concrete: $\forall s_i$ and $\forall p\in 50 55 \widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$. … … 66 71 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, 67 72 \widehat{F}_{\overline{\sigma}} \rangle$ is such that : 73 \vspace*{-2mm} 68 74 \begin{itemize} 75 %\topsep 0pt 76 \itemsep -0.3em 69 77 \item $AP_{\overline{\sigma}} = {AP}_i$: 70 78 The set of atomic propositions coincides with the one of $\sigma$ -
papers/FDL2012/exp_results.tex
r89 r92 1 1 We have conducted preliminary experiments to test and compare the performance 2 of our strategy with existing abstraction-refinementtechniques available in2 of our strategy with existing techniques available in 3 3 VIS. There are several abstraction-refinement techniques implemented in VIS 4 4 accessible via \emph{approximate\_model\_check}, 5 5 \emph{iterative\_model\_check}, \emph{check\_invariant} and 6 \emph{incremental\_ctl\_ model\_check} commands. However, among the available7 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}.6 \emph{incremental\_ctl\_verification} commands. However, among the available 7 techniques, \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 8 9 9 … … 18 18 \toprule 19 19 \multicolumn{3}{l}{\textbf{Experiment}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 20 \multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\20 \multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 21 21 \midrule 22 22 \midrule … … 24 24 & Concrete & 2 Masters-1 Slave & 445 & 24406 & 7.71723e+06 & 35.2 \\ 25 25 & Model & 4 Masters-1 Slave & 721 & 84118 & 3.17332e+12 & 2818.3 \\ 26 & & 4 Masters-2 Slaves & 911 & N/A & N/A & >1 day\\26 & & 4 Masters-2 Slaves & 895 & 238990 & 5.708e+15 & 68882.3\footnotemark[1] \\ 27 27 \cline{2-7} 28 28 \cline{2-7} … … 36 36 & Model & 4 Masters-1 Slave & 498 & 121 & 1.80144e+18 & 0.02 \\ 37 37 & for $\phi_2$ & 4 Masters-2 Slaves & 586 & 141 & 3.68935e+21 & 0.02 \\ 38 \midrule38 % \midrule 39 39 \midrule 40 &\multicolumn{2}{c}{Concrete Model} & 822 & 161730 & 3.7354e+07 & 300.12 \\40 &\multicolumn{2}{c}{Concrete Model} & 822 & 161730 & 3.7354e+07 & 300.12 \\ 41 41 \cline{2-7} 42 42 \cline{2-7} … … 45 45 &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$} & 425 & 187 & 1.66005e+12 & 0.04 \\ 46 46 \bottomrule 47 \bottomrule 47 %\bottomrule 48 48 49 \end{tabular} 49 50 … … 51 52 \end{table*} 52 53 54 %\footnotetext[1]{Computed on a calculation server.} 53 55 54 56 … … 72 74 & & Standard MC & - & 6.13 \\ 73 75 \midrule 74 \midrule76 %\midrule 75 77 & & Prop. Select. & 1 & 2.0 \\ 76 78 VCI-PI: & $\phi_1$ & Incremental & 0 & 20.4 \\ … … 81 83 & & Standard MC & - & 39.4 \\ 82 84 \midrule 83 \midrule85 %\midrule 84 86 85 87 & & Prop. Select. & 1 & 2.1 \\ … … 91 93 & & Standard MC & - & >1 day \\ 92 94 \midrule 93 \midrule95 %\midrule 94 96 95 97 & & Prop. Select. & 1 & 2.2 \\ … … 101 103 & & Standard MC & - & >1 day\\ 102 104 \midrule 103 \midrule105 %\midrule 104 106 & & Prop. Select. & 0 & 1.02 \\ 105 107 &$\phi_3$ & Incremental & N/A & >1 day \\ … … 111 113 112 114 \bottomrule 113 \bottomrule115 %\bottomrule 114 116 115 117 \end{tabular} … … 117 119 \caption{\label{TabVerif} Verification Results } 118 120 \end{table} 119 120 121 121 122 122 … … 128 128 $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger 129 129 version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of 130 2 7verifed components properties to be selected in VCI-PI plateform.130 26 verifed components properties to be selected in VCI-PI plateform. 131 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. 132 132 -
papers/FDL2012/framework.tex
r89 r92 43 43 % \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG} 44 44 % \hspace*{-5mm} 45 \includegraphics {our_framework_cegar_png}45 \includegraphics[scale=0.37]{our_framework_cegar_png} 46 46 \caption{\label{cegar} Verification Process } 47 47 \end{figure} 48 48 49 \vspace*{-5mm} 49 50 \subsection{Concrete system definition} 50 51 As mentioned earlier, our concrete model consists of several components and each … … 54 55 \begin{definition} 55 56 A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where, 56 \begin{itemize} 57 \vspace*{-2mm} 58 \begin{itemize} 59 %\partopsep= -1.0em 60 %\topsep -0.5em 61 \itemsep -0.3em 57 62 \item $I$ is a finite set of Boolean inputs signals. 58 63 \item $O$ is a finite set of Boolean outputs signals. … … 104 109 $AP$, An \emph{Abstract Kripke Structure}, $AKS(\varphi) =(AP, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of: 105 110 106 \begin{itemize} 111 \vspace*{-3mm} 112 \begin{itemize} 113 %\partopsep=0pt 114 %\topsep 0pt 115 \itemsep -0.3em 107 116 \item { $AP$ : The finite set of atomic propositions of property $\varphi$ } 108 117 \item { $\widehat{S}$ : a finite set of states} … … 116 125 %\bigskip 117 126 127 \vspace*{-2mm} 118 128 We denote by $\widehat{L}(s)$ the configuration of atomic propositions in state $s$ and by $\widehat{L}(s)[p]$ the projection of configuration $\widehat{L}(s)$ according to atomic proposition $p$. 119 129 … … 129 139 let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$: 130 140 131 \begin{itemize} 141 \vspace*{-3mm} 142 \begin{itemize} 143 %\topsep 0pt 144 \itemsep -0.3em 132 145 \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $} 133 146 \item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $} … … 137 150 138 151 139 The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}).152 %The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}). 140 153 141 154 … … 154 167 \begin{definition}[] 155 168 The \emph {concretization} of an abstract state $s$ with respect to the variable $p$ 156 ({\it unknown} in that state), assigns either true or false to $p$. 157 169 ({\it unknown} in that state), assigns either true or false to $p$.\\ 158 170 The \emph {abstraction} of a state $s$ with respect to the variable $p$ 159 171 (either true or false in that state), assigns {\it unknown} to $p$. … … 188 200 {\it and} to the four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in 189 201 AP_i \cup AP_{\varphi_j^k}$ we have the following label~: 190 \begin{itemize} 191 \topsep -.5em 192 \itemsep -0.5em 202 \vspace*{-2mm} 203 \begin{itemize} 204 %\topsep 0pt 205 \itemsep -0.3em 193 206 \item $\widehat{L}_{i+1}[p] = \top$ iff p is {\it unknown} in both states or 194 207 does not belong to the set of atomic proposition. … … 197 210 (resp. $s_{\varphi_j^k}$). 198 211 \end{itemize} 212 \vspace*{-2mm} 199 213 By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than 200 214 $\widehat{M}_i$ and by … … 203 217 \end{proof} 204 218 219 \vspace*{-5mm} 205 220 \subsection{Initial abstraction} 206 221 Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\Phi$. -
papers/FDL2012/introduction.tex
r91 r92 7 7 and programmers as it may delay getting a new product to the market or cause 8 8 failure of some critical devices that are already in use. System verification 9 using formal methods such as model checking guarantee s a high level of quality in terms of safety and reliabilty while reducing financial risk.9 using formal methods such as model checking guarantee a high level of quality in terms of safety and reliability while reducing financial risk. 10 10 11 11 … … 18 18 19 19 20 Several tools using counterexample-guided abstraction refinement technique have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive.20 Several tools using counterexample-guided abstraction refinement technique, like those implemented in the VIS model-checker, have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive. 21 21 22 22 … … 28 28 29 29 30 In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee. 30 In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee. Since, there have been other works on construction of components from interval temporal logic properties which could be used to speed up verification process \cite{SNBE06property_based} \cite{Kunz_al11ipc_abs}. 31 31 32 33 34 In 2006, Hans Eveking and al. introduced a technique of normalizing properties and transforming those normalized properties into an executable design description \cite{SNBE06property_based}. The generation of abstraction from PSL/Sugar specification language could then be used in the verification process to speed up the operation. This technique also allows the tests of specifications without having to build an implementation first. 35 32 %In 2006, Hans Eveking and al. introduced a technique of normalizing properties and transforming those normalized properties into an executable design description \cite{SNBE06property_based}. The generation of abstraction from PSL/Sugar specification language could then be used in the verification process to speed up the operation. This technique also allows the tests of specifications without having to build an implementation first. 33 %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 34 37 35 … … 39 37 40 38 41 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. 39 %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. 42 40 43 41 -
papers/FDL2012/myBib.bib
r83 r92 72 72 address = "Chicago, IL", 73 73 year = 2000, 74 publisher = "L ecture Notes in Computer Science"74 publisher = "LNCS" 75 75 } 76 76 … … 159 159 year = 2003, 160 160 month = Nov, 161 publisher = "L ecture Notes in Computer Science"161 publisher = "LNCS" 162 162 } 163 163 … … 212 212 pages = {103-122}, 213 213 year = 2000, 214 publisher = "L ecture Notes in Computer Science, Springer Verlag"214 publisher = "LNCS, Springer Verlag" 215 215 } 216 216 … … 223 223 address = "Taipei, Taiwan", 224 224 year = 2005, 225 publisher = "L ecture Notes in Computer Science, Springer"225 publisher = "LNCS, Springer" 226 226 } 227 227 … … 230 230 author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani", 231 231 title = "{ You Assume, We Guarantee : Methodology and Case Studies} ", 232 booktitle = "CAV â98 : Proceedings of the 10th InternationalConference on Computer Aided Verification",232 booktitle = "CAVâ98: Proceedings of the 10th Int. Conference on Computer Aided Verification", 233 233 volume = 1427, 234 234 pages = {440-451}, 235 235 address = "Vancouver, Canada", 236 236 year = 1998, 237 publisher = " L ecture Notes in Computer Science, Springer-Verlag"237 publisher = " LNCS, Springer-Verlag" 238 238 } 239 239 … … 246 246 pages = {250-263}, 247 247 year = 1991, 248 publisher = " L ecture Notes in Computer Science, Springer-Verlag"248 publisher = " LNCS, Springer-Verlag" 249 249 } 250 250 … … 256 256 volume = 1254, 257 257 year = 1997, 258 publisher = " L ecture Notes in Computer Science, Springer"258 publisher = " LNCS, Springer" 259 259 } 260 260 … … 264 264 author = " S. Pardo and G. Hachtel", 265 265 title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ", 266 booktitle = " In CAV â97 : Proceedings of the 9th International Conference on Computer Aided Verification",266 booktitle = " In CAV â97", 267 267 volume = 1254, 268 268 pages = {12-23}, 269 269 year = 1997, 270 publisher = " L ecture Notes in Computer Science, Springer-Verlag"270 publisher = " LNCS, Springer-Verlag" 271 271 } 272 272 … … 304 304 author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke", 305 305 title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ", 306 booktitle = " In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",306 booktitle = " In TACAS '07 ", 307 307 year = 2007, 308 308 } … … 322 322 author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani", 323 323 title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ", 324 booktitle = " Fourth InternationalConference on Integrated Formal Methods (IFM 2004)",324 booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)", 325 325 volume = 2999, 326 326 pages = {1-20}, 327 327 year = 2004, 328 publisher = " L ecture Notes in Computer Science, Springer"328 publisher = " LNCS, Springer" 329 329 } 330 330 -
papers/FDL2012/ordering_filter_properties.tex
r90 r92 27 27 whereas variables which do not interfere with a primary variable are weighted 0. 28 28 Here is how we proceed: 29 \vspace*{-5mm} 29 30 \begin{enumerate} 31 \itemsep -0.3em 30 32 \item Build the structural dependency graph for all primary variables. 31 33 \item Compute the depth of all variables … … 157 159 In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$ 158 160 is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies 159 the global property~$\Phi$ 161 the global property~$\Phi$. 160 162 %as show in figure \ref{AKSNegCex}. 161 163 %In case where the spurious counter-example exhibits a bounded path, we add a last … … 181 183 R_{\sigma},F_{\sigma})$ 182 184 such that: 183 185 \vspace*{-2mm} 184 186 \begin{itemize} 187 %\parsep=2pt 188 %\topsep 0pt 189 \itemsep -0.3em 185 190 \item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model 186 191 \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ … … 252 257 253 258 \begin{property}{Counterexample eviction} 259 \vspace*{-2mm} 254 260 \begin{enumerate} 261 \itemsep -0.3em 255 262 \item If {\textbf{$K(\sigma) \vDash \varphi \Rightarrow AKS(\varphi) $ will 256 263 not eliminate $\sigma$}}. … … 272 279 \end{proof} 273 280 281 \vspace*{-2mm} 274 282 The proposed approach ensures that the refinement excludes the counterexample 275 283 and respects the definition \ref{def:goodrefinement}.
Note: See TracChangeset
for help on using the changeset viewer.
