Index: /papers/FDL2012/FDL2012.tex =================================================================== --- /papers/FDL2012/FDL2012.tex (revision 88) +++ /papers/FDL2012/FDL2012.tex (revision 89) @@ -85,7 +85,22 @@ %\section*{Drawbacks} -We have presented a new strategy in the abstraction generation and refinement which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of complex systems. Our preliminary experimental results shows an interesting performance in terms duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph. +We have presented a new strategy in the abstraction generation and refinement +which is well adapted for compositional embedded systems. This verification +technique is compatible and suits well in the natural development process of +complex systems. Our preliminary experimental results shows an interesting +performance in terms of duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph. -Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoqued by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases. +Nevertheless, in order to function well, this refinement technique requires a +complete specification of every components of the concrete model. Futhermore, +it may be possible that none of the properties available is capable of +eliminating the counterexample which is probably due to an uncomplete +specification or a counterexample that should be eliminated by the product of +local properties. In this case, other refinement techniques such as the +refinement by eliminating the counterexample only, or the identification of a +good set of local properties to be integreted simultaneously, should be considered. +We are currently investigating other complementary techniques to overcome these particular cases. +A complementary approach consists in oimproving the specification of the +model~: at the component level, or for groups of components. The work of +Kroening \cite{pwk2009-date} could help us in this direction. Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 88) +++ /papers/FDL2012/abstraction_refinement.tex (revision 89) @@ -14,9 +14,9 @@ $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$. \item The spurious counterexample in $\widehat{M}_i$ is removed from -$\widehat{M_{i+1}}$. +$\widehat{M}_{i+1}$. \end{enumerate} \label{def:goodrefinement} \end{definition} -Moreover, the refinement steps should be easy to compute and ensure a fast +Furthermore, the refinement steps should be easy to compute and ensure a fast convergence by minimizing the number of iterations of the CEGAR loop. @@ -32,5 +32,5 @@ according to definition \ref{def:goodrefinement}. We have several options. The most straightforward consists in building -an AKS representing all possible executions except the spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$. +an AKS representing all possible executions except the spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$. @@ -43,5 +43,5 @@ The spurious counterexample $\sigma$ is defined such that : \begin{definition} -Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, +Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, \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]$. @@ -56,5 +56,5 @@ \end{definition} The construction of the AKS representing all executions except the one -described by the spurious counter-example is done in two steps. +described by the spurious counterexample is done in two steps. \subsubsection{Step 1~:~Build the structure of the AKS.} @@ -62,6 +62,6 @@ \begin{definition} -Let $\sigma$ be a spurious counter-example of length $|\sigma| = n$, the \emph{ AKS of the -counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, +Let $\sigma$ be a spurious counterexample of length $|\sigma| = n$, the \emph{ AKS of the +counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$ is such that : @@ -101,22 +101,36 @@ \emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$. -To build the final AKS representing all sequences but spurious counter-example +To build the final AKS representing all sequences but spurious counterexample $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by $k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$ and assigns to each of them a label of $k$ variables $\{v_0, \ldots, -v_{k-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1], +v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1], v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each state $\bar{s_i^j}$ is connected to the same predecessor and successor states as state $\bar{s_i}$. -This final AKS presents a number of states in $\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ : $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priors know if at least one of these sequence is executable in the concrete model. +This final AKS presents a number of states in +$\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each +refinement step, the spurious counterexample {\em only} induces a low +convergence. Moreover, in some cases, this strategy may not converge: suppose +that all sequences of the form $a.b^*.c$ are spurious counterexamples (here +$a$, $b$ and $c$ represent concrete state configurations). Assume, at a given +refinement step $i$, a particular counterexample $\sigma_i = s_0 \rightarrow +s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = +b, L(s_n) = c$. Removing this counterexample does not prevent from a new +spurious counterexample at step $i+1$ : $\sigma_{i+1} = s_0 \rightarrow s_1 +\rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = +b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious +counterexample {\em one by one} diverges in this case. However, we cannot +eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step +since we do not {\it a priori} know if at least one of these sequences is executable in the concrete model. From these considerations, we are interested in removing {\em sets of -behaviors encompassing the spurious counter-example} but still guaranteeing an +behaviors encompassing the spurious counterexample} but still guaranteeing an over-approximation of the set of tree-organized behaviors of the concrete model. The strengthening of the abstraction $\widehat{M}_i$ with the addition of AKS of already verified local CTL properties eliminates sets of behaviors and guarantees the over-approximation (property -\ref{prop:concrete_compose}) but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example. +\ref{prop:concrete_compose}) but does not guarantee the elimination of the counterexample. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counterexample. Index: /papers/FDL2012/exp_results.tex =================================================================== --- /papers/FDL2012/exp_results.tex (revision 88) +++ /papers/FDL2012/exp_results.tex (revision 89) @@ -1,3 +1,9 @@ -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}. +We have conducted preliminary experiments to test and compare the performance +of our strategy with existing abstraction-refinement 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}. @@ -115,10 +121,23 @@ -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. +In Table \ref{TabVerif}, we compare the execution time and the number of refinment +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 +27 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. -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. +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 +for the initial abstraction, 3 selected component properties were sufficient +to verify both global properties without refinement. -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. +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. Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 88) +++ /papers/FDL2012/framework.tex (revision 89) @@ -48,5 +48,5 @@ \subsection{Concrete system definition} -As mention earlier, our concrete model consists of several components and each +As mentioned earlier, our concrete model consists of several components and each component comes with its specification. The concrete system is a synchronous composition of components, each of which @@ -178,5 +178,5 @@ Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property of a component $C_j$ of M, $\widehat{M}_{i+1} = \widehat{M_i}\parallel -AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}} +AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. \end{property} @@ -185,5 +185,6 @@ Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ and $s_{\varphi_j^k} \in S_{\varphi_j^k}$. -The label of $s_{i+1}$ is obtained by applying the Belnap's logic operators to four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in +The label of $s_{i+1}$ is obtained by applying the Belnap's logic operators +{\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} @@ -196,5 +197,6 @@ (resp. $s_{\varphi_j^k}$). \end{itemize} -By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by +By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than +$\widehat{M}_i$ and by the property of parallel composition, $\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$). Index: /papers/FDL2012/introduction.tex =================================================================== --- /papers/FDL2012/introduction.tex (revision 88) +++ /papers/FDL2012/introduction.tex (revision 89) @@ -39,5 +39,10 @@ -In 2007, a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component verifies \cite{braunstein07ctl_abstraction}. The method is actually a tentative to associate compositional and abstraction-refinement verification techniques. The generations of AKS from CTL formula have been successfully automated \cite{bara08abs_composant}. These work will be the base of the techniques in this paper. +In 2007, a method to build abstractions of components into AKS (Abstract +Kripke Structure), based on the set of the properties (CTL) each component +verifies \cite{braunstein07ctl_abstraction}. The method is actually a +tentative to associate compositional and abstraction-refinement verification +techniques. The generations of AKS from CTL formula have been successfully +automated \cite{bara08abs_composant}. This work will be the base of the techniques in this paper. Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 88) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 89) @@ -15,13 +15,14 @@ %behaviors that may have an impact on the global property. We observed that -the more closer a variable is from the primary -variable the more it affects the primary variable. Hence, a property -has higher priority according to the number of primary or close to primary variables it -contains. +the closer a variable is from the primary +variable, the higher influence it has on it. +%Hence, a property +%has higher priority according to the number of primary or close to primary variables it +%contains. Moreover, a global property often specifies the behavior at the interface of components. Typically, a global property ensures that a message sent is always acknowledged or the good target gets the message. This kind of behavior relates the input-output behaviors of components. -We have decided to allocate an extra weight for variables which are present at the interface of a component +We have decided to allocate an extra weight for interface variables whereas variables which do not interfere with a primary variable are weighted 0. Here is how we proceed: @@ -44,17 +45,18 @@ \label{algo:weight} -\KwIn{ $\{V\}$, the set of all dependency graph variable} +\KwIn{ $G$, the set of all dependency graph variable} +{ $V$ the set of variables} \KwOut{$\{(v,w)| v \in V, w \in N\}$, The set of variables with their weight} \Begin{ -$p = $ max(depth(V)) \\ +$p = $ max(depth(G)) \\ \For{$v\in V$}{ - d = depth(v) \; + $d$ = depth($v$) \; $w = 2^{p-d}*p$\; - \If(v is primary variable){$d == 0$} + \If($v$ is primary variable){$d == 0$} { $w = 5 * w$\; } - \If(v is an interface variable){$v\in{I\cup O}$} + \If($v$ is an interface variable){$v\in{I\cup O}$} { $w = 3 * w $ @@ -134,5 +136,5 @@ It is definitely not an exact pertinence calculation of properties but provides a good indicator of their possible impact on the global property. -After this pre-processing phase, we have a list of properties $L_\phi$ +After this pre-processing phase, we have a list of properties ordered according to their pertinence with regards to the global property. @@ -149,10 +151,10 @@ %are characterized. Hence there is more constrains behavior and more concretize %states. -As we would like to ensure the elimination of the counter-example previously found, +As we would like to ensure the elimination of the counterexample previously found, we filter out properties that do not have an impact on the counterexample $\sigma$ thus will not eliminate it. 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 @@ -172,5 +174,5 @@ % \begin{definition} -Let $\sigma$ be a counter-example of length $n$ in $\widehat{M}_i$ such +Let $\sigma$ be a counterexample of length $n$ in $\widehat{M}_i$ such that $ \sigma = s_{0}\rightarrow s_{1}\rightarrow \ldots \rightarrow s_{n-1}$. The \emph{Kripke structure derived from $\sigma$} is 6-tuple @@ -240,9 +242,11 @@ All the properties available for refinement are then model-checked on $K(\sigma)$. If the -property holds then the property will not discriminate the counterexample. +property holds then the property will not eliminate the counterexample. Hence this property is not a good candidate for refinement. -Therefore all properties that are not satisfied are chosen to be -integrated in the next step of refinement. At this stage, we already have a -list of potential properties that definitely eliminates the current counterexample $\sigma$ and might converge the abstract model towards a model sufficient to verify the global property $\Phi$. +Therefore the highest weighted property not satisfied in $K(\sigma)$ is choosen to be +integrated in the next refinement step. This process is iterated for each +refinement step. +%At this stage, we already have a +%list of potential properties that definitely eliminates the current counterexample $\sigma$ and might converge the abstract model towards a model sufficient to verify the global property $\Phi$. \begin{property}{Counterexample eviction} @@ -267,5 +271,5 @@ \end{proof} -The proposed approach ensures that the refinement excludes the counter-example +The proposed approach ensures that the refinement excludes the counterexample and respects the definition \ref{def:goodrefinement}. We will show in our experiments that first the time needed to build an AKS is