Index: /papers/FDL2012/FDL2012.tex =================================================================== --- /papers/FDL2012/FDL2012.tex (revision 91) +++ /papers/FDL2012/FDL2012.tex (revision 92) @@ -34,5 +34,5 @@ \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process} -% \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN} +% \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ} % \thanks{This work was supported by...}} % \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\ @@ -106,5 +106,6 @@ Kroening \cite{pwk2009-date} could help us in this direction. - +%footnote for Table 1 +\footnotetext[1]{Computed on a calculation server.} %\begin{thebibliography} Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 91) +++ /papers/FDL2012/abstraction_refinement.tex (revision 92) @@ -8,5 +8,7 @@ \begin{definition} An efficient \emph{refinement} verifies the following properties: +\vspace*{-2mm} \begin{enumerate} +\itemsep -0.3em \item The new refinement is an over-approximation of the concrete model: $\widehat{M} \sqsubseteq \widehat{M}_{i+1}$. @@ -46,5 +48,8 @@ \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$. +%\vspace*{-2mm} \begin{itemize} +%\topsep 0pt +\itemsep -0.3em \item All its variables are concrete: $\forall s_i$ and $\forall p\in \widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$. @@ -66,5 +71,8 @@ \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$ is such that : +\vspace*{-2mm} \begin{itemize} +%\topsep 0pt +\itemsep -0.3em \item $AP_{\overline{\sigma}} = {AP}_i$: The set of atomic propositions coincides with the one of $\sigma$ Index: /papers/FDL2012/exp_results.tex =================================================================== --- /papers/FDL2012/exp_results.tex (revision 91) +++ /papers/FDL2012/exp_results.tex (revision 92) @@ -1,9 +1,9 @@ We have conducted preliminary experiments to test and compare the performance -of our strategy with existing abstraction-refinement techniques available in +of our strategy with existing techniques available in VIS. There are 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 available -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}. +\emph{incremental\_ctl\_verification} commands. However, among the available +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}. @@ -18,5 +18,5 @@ \toprule \multicolumn{3}{l}{\textbf{Experiment}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ -\multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ +\multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ \midrule \midrule @@ -24,5 +24,5 @@ & Concrete & 2 Masters-1 Slave & 445 & 24406 & 7.71723e+06 & 35.2 \\ & Model & 4 Masters-1 Slave & 721 & 84118 & 3.17332e+12 & 2818.3 \\ - & & 4 Masters-2 Slaves & 911 & N/A & N/A & >1 day \\ + & & 4 Masters-2 Slaves & 895 & 238990 & 5.708e+15 & 68882.3\footnotemark[1] \\ \cline{2-7} \cline{2-7} @@ -36,7 +36,7 @@ & Model & 4 Masters-1 Slave & 498 & 121 & 1.80144e+18 & 0.02 \\ & for $\phi_2$ & 4 Masters-2 Slaves & 586 & 141 & 3.68935e+21 & 0.02 \\ - \midrule +% \midrule \midrule - &\multicolumn{2}{c}{Concrete Model} & 822 & 161730 & 3.7354e+07 & 300.12 \\ + &\multicolumn{2}{c}{Concrete Model} & 822 & 161730 & 3.7354e+07 & 300.12 \\ \cline{2-7} \cline{2-7} @@ -45,5 +45,6 @@ &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$} & 425 & 187 & 1.66005e+12 & 0.04 \\ \bottomrule -\bottomrule +%\bottomrule + \end{tabular} @@ -51,4 +52,5 @@ \end{table*} +%\footnotetext[1]{Computed on a calculation server.} @@ -72,5 +74,5 @@ & & Standard MC & - & 6.13 \\ \midrule -\midrule +%\midrule & & Prop. Select. & 1 & 2.0 \\ VCI-PI: & $\phi_1$ & Incremental & 0 & 20.4 \\ @@ -81,5 +83,5 @@ & & Standard MC & - & 39.4 \\ \midrule -\midrule +%\midrule & & Prop. Select. & 1 & 2.1 \\ @@ -91,5 +93,5 @@ & & Standard MC & - & >1 day \\ \midrule -\midrule +%\midrule & & Prop. Select. & 1 & 2.2 \\ @@ -101,5 +103,5 @@ & & Standard MC & - & >1 day\\ \midrule -\midrule +%\midrule & & Prop. Select. & 0 & 1.02 \\ &$\phi_3$ & Incremental & N/A & >1 day \\ @@ -111,5 +113,5 @@ \bottomrule -\bottomrule +%\bottomrule \end{tabular} @@ -117,6 +119,4 @@ \caption{\label{TabVerif} Verification Results } \end{table} - - @@ -128,5 +128,5 @@ $\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 -27 verifed components properties to be selected in VCI-PI plateform. +26 verifed components properties to be selected in VCI-PI plateform. 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. Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 91) +++ /papers/FDL2012/framework.tex (revision 92) @@ -43,8 +43,9 @@ % \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG} % \hspace*{-5mm} - \includegraphics{our_framework_cegar_png} + \includegraphics[scale=0.37]{our_framework_cegar_png} \caption{\label{cegar} Verification Process } \end{figure} +\vspace*{-5mm} \subsection{Concrete system definition} As mentioned earlier, our concrete model consists of several components and each @@ -54,5 +55,9 @@ \begin{definition} A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where, -\begin{itemize} +\vspace*{-2mm} +\begin{itemize} +%\partopsep= -1.0em +%\topsep -0.5em +\itemsep -0.3em \item $I$ is a finite set of Boolean inputs signals. \item $O$ is a finite set of Boolean outputs signals. @@ -104,5 +109,9 @@ $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: -\begin{itemize} +\vspace*{-3mm} +\begin{itemize} +%\partopsep=0pt +%\topsep 0pt +\itemsep -0.3em \item { $AP$ : The finite set of atomic propositions of property $\varphi$ } \item { $\widehat{S}$ : a finite set of states} @@ -116,4 +125,5 @@ %\bigskip +\vspace*{-2mm} 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$. @@ -129,5 +139,8 @@ 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]$: -\begin{itemize} +\vspace*{-3mm} +\begin{itemize} +%\topsep 0pt +\itemsep -0.3em \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $} \item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $} @@ -137,5 +150,5 @@ -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}). +%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}). @@ -154,6 +167,5 @@ \begin{definition}[] The \emph {concretization} of an abstract state $s$ with respect to the variable $p$ -({\it unknown} in that state), assigns either true or false to $p$. - +({\it unknown} in that state), assigns either true or false to $p$.\\ The \emph {abstraction} of a state $s$ with respect to the variable $p$ (either true or false in that state), assigns {\it unknown} to $p$. @@ -188,7 +200,8 @@ {\it and} to the four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in AP_i \cup AP_{\varphi_j^k}$ we have the following label~: -\begin{itemize} -\topsep -.5em -\itemsep -0.5em +\vspace*{-2mm} +\begin{itemize} +%\topsep 0pt +\itemsep -0.3em \item $\widehat{L}_{i+1}[p] = \top$ iff p is {\it unknown} in both states or does not belong to the set of atomic proposition. @@ -197,4 +210,5 @@ (resp. $s_{\varphi_j^k}$). \end{itemize} +\vspace*{-2mm} By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than $\widehat{M}_i$ and by @@ -203,4 +217,5 @@ \end{proof} +\vspace*{-5mm} \subsection{Initial abstraction} 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$. Index: /papers/FDL2012/introduction.tex =================================================================== --- /papers/FDL2012/introduction.tex (revision 91) +++ /papers/FDL2012/introduction.tex (revision 92) @@ -7,5 +7,5 @@ and programmers as it may delay getting a new product to the market or cause failure of some critical devices that are already in use. System verification -using formal methods such as model checking guarantees a high level of quality in terms of safety and reliabilty while reducing financial risk. +using formal methods such as model checking guarantee a high level of quality in terms of safety and reliability while reducing financial risk. @@ -18,5 +18,5 @@ -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. +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. @@ -28,10 +28,8 @@ -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. +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}. - - -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. - +%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. +%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,5 +37,5 @@ -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. +%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. Index: /papers/FDL2012/myBib.bib =================================================================== --- /papers/FDL2012/myBib.bib (revision 91) +++ /papers/FDL2012/myBib.bib (revision 92) @@ -72,5 +72,5 @@ address = "Chicago, IL", year = 2000, - publisher = "Lecture Notes in Computer Science" + publisher = "LNCS" } @@ -159,5 +159,5 @@ year = 2003, month = Nov, - publisher = "Lecture Notes in Computer Science" + publisher = "LNCS" } @@ -212,5 +212,5 @@ pages = {103-122}, year = 2000, - publisher = "Lecture Notes in Computer Science, Springer Verlag" + publisher = "LNCS, Springer Verlag" } @@ -223,5 +223,5 @@ address = "Taipei, Taiwan", year = 2005, - publisher = "Lecture Notes in Computer Science, Springer" + publisher = "LNCS, Springer" } @@ -230,10 +230,10 @@ author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani", title = "{ You Assume, We Guarantee : Methodology and Case Studies} ", - booktitle = "CAV ’98 : Proceedings of the 10th International Conference on Computer Aided Verification", + booktitle = "CAV’98: Proceedings of the 10th Int. Conference on Computer Aided Verification", volume = 1427, pages = {440-451}, address = "Vancouver, Canada", year = 1998, - publisher = " Lecture Notes in Computer Science, Springer-Verlag" + publisher = " LNCS, Springer-Verlag" } @@ -246,5 +246,5 @@ pages = {250-263}, year = 1991, - publisher = " Lecture Notes in Computer Science, Springer-Verlag" + publisher = " LNCS, Springer-Verlag" } @@ -256,5 +256,5 @@ volume = 1254, year = 1997, - publisher = " Lecture Notes in Computer Science, Springer" + publisher = " LNCS, Springer" } @@ -264,9 +264,9 @@ author = " S. Pardo and G. Hachtel", title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ", - booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification", + booktitle = " In CAV ’97", volume = 1254, pages = {12-23}, year = 1997, - publisher = " Lecture Notes in Computer Science, Springer-Verlag" + publisher = " LNCS, Springer-Verlag" } @@ -304,5 +304,5 @@ author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke", title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ", - booktitle = " In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)", + booktitle = " In TACAS '07 ", year = 2007, } @@ -322,9 +322,9 @@ author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani", title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ", - booktitle = " Fourth International Conference on Integrated Formal Methods (IFM 2004)", + booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)", volume = 2999, pages = {1-20}, year = 2004, - publisher = " Lecture Notes in Computer Science, Springer" + publisher = " LNCS, Springer" } Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 91) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 92) @@ -27,5 +27,7 @@ whereas variables which do not interfere with a primary variable are weighted 0. Here is how we proceed: +\vspace*{-5mm} \begin{enumerate} +\itemsep -0.3em \item Build the structural dependency graph for all primary variables. \item Compute the depth of all variables @@ -157,5 +159,5 @@ In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$ is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies -the global property~$\Phi$ +the global property~$\Phi$. %as show in figure \ref{AKSNegCex}. %In case where the spurious counter-example exhibits a bounded path, we add a last @@ -181,6 +183,9 @@ R_{\sigma},F_{\sigma})$ such that: - +\vspace*{-2mm} \begin{itemize} +%\parsep=2pt +%\topsep 0pt +\itemsep -0.3em \item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ @@ -252,5 +257,7 @@ \begin{property}{Counterexample eviction} +\vspace*{-2mm} \begin{enumerate} +\itemsep -0.3em \item If {\textbf{$K(\sigma) \vDash \varphi \Rightarrow AKS(\varphi) $ will not eliminate $\sigma$}}. @@ -272,4 +279,5 @@ \end{proof} +\vspace*{-2mm} The proposed approach ensures that the refinement excludes the counterexample and respects the definition \ref{def:goodrefinement}.