Changeset 89


Ignore:
Timestamp:
Apr 6, 2012, 4:44:06 PM (12 years ago)
Author:
cecile
Message:

corrections typos and co

Location:
papers/FDL2012
Files:
6 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r83 r89  
    8585%\section*{Drawbacks}
    8686
    87 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.
     87We have presented a new strategy in the abstraction generation and refinement
     88which is well adapted for compositional embedded systems. This verification
     89technique is compatible and suits well in the natural development process of
     90complex systems. Our preliminary experimental results shows an interesting
     91performance 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.
    8892
    89 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.
     93Nevertheless, in order to function well, this refinement technique requires a
     94complete specification of every components of the concrete model. Futhermore,
     95it may be possible that none of the properties available is capable of
     96eliminating the counterexample which is probably due to an uncomplete
     97specification or a counterexample that should be eliminated by the product of
     98local properties. In this case, other refinement techniques such as the
     99refinement by eliminating the counterexample only, or the identification of a
     100good set of local properties to be integreted simultaneously, should be considered.
     101We are currently investigating other complementary techniques to overcome these particular cases.
     102A complementary approach consists in oimproving the specification of the
     103model~: at the component level, or for groups of components. The work of
     104Kroening \cite{pwk2009-date} could help us in this direction.
    90105
    91106

  • papers/FDL2012/abstraction_refinement.tex

    r82 r89  
    1414$\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$.
    1515\item The spurious counterexample in $\widehat{M}_i$ is  removed from
    16 $\widehat{M_{i+1}}$.
     16$\widehat{M}_{i+1}$.
    1717\end{enumerate}
    1818\label{def:goodrefinement}
    1919\end{definition}
    20 Moreover, the refinement steps should be easy to compute and ensure a fast
     20Furthermore, the refinement steps should be easy to compute and ensure a fast
    2121convergence by minimizing the number of iterations of the CEGAR loop.
    2222
    … …  
    3232according to definition \ref{def:goodrefinement}.
    3333We have  several options. The most straightforward consists in building
    34 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$.
     34an 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$.
    3535
    3636
    … …  
    4343The spurious counterexample $\sigma$ is defined such that :
    4444\begin{definition}
    45 Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
     45Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
    4646\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
    4747\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
    … …  
    5656\end{definition}
    5757The construction of the AKS representing all executions except the one
    58 described by the spurious counter-example is done in two steps.
     58described by the spurious counterexample is done in two steps.
    5959
    6060\subsubsection{Step 1~:~Build the structure of the AKS.}
    … …  
    6262
    6363\begin{definition}
    64 Let $\sigma$ be a spurious counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
    65 counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
     64Let $\sigma$ be a spurious counterexample of  length $|\sigma| = n$, the \emph{ AKS of the
     65counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
    6666\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
    6767\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
    … …  
    101101\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}\}\}$.
    102102
    103 To build the final AKS representing all sequences but spurious counter-example
     103To build the final AKS representing all sequences but spurious counterexample
    104104$\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by
    105105$k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$
    106106and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
    107 v_{k-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1],
     107v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1],
    108108v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each
    109109state $\bar{s_i^j}$ is connected to the same predecessor and successor states
    110110as state $\bar{s_i}$.
    111111
    112 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.
     112This final AKS presents a number of states in
     113$\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each
     114refinement step, the spurious counterexample {\em only} induces a low
     115convergence. Moreover, in some cases, this strategy may not converge: suppose
     116that all sequences of the form $a.b^*.c$ are spurious counterexamples (here
     117$a$, $b$ and $c$ represent concrete state configurations). Assume, at a given
     118refinement step $i$, a particular counterexample $\sigma_i = s_0 \rightarrow
     119s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) =
     120b, L(s_n) = c$. Removing this counterexample does not prevent from a new
     121spurious counterexample at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1
     122\rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) =
     123b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious
     124counterexample {\em one by one} diverges in this case. However, we cannot
     125eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step
     126since we do not {\it a priori} know if at least one of these sequences is executable in the concrete model.
    113127
    114128From these considerations, we are interested in removing {\em sets of
    115 behaviors encompassing the spurious counter-example} but still guaranteeing an
     129behaviors encompassing the spurious counterexample} but still guaranteeing an
    116130over-approximation of the set of tree-organized behaviors of the concrete
    117131model. The strengthening of the abstraction $\widehat{M}_i$ with the
    118132addition of AKS of already verified local CTL properties eliminates sets of
    119133behaviors and guarantees the over-approximation (property
    120 \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.
     134\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.
    121135
    122136

  • 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}.
     1We have conducted preliminary experiments to test and compare the performance
     2of our strategy with existing abstraction-refinement techniques available in
     3VIS. There are several abstraction-refinement techniques implemented in VIS
     4accessible 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
     7techniques, \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}.
    28
    39
    … …  
    115121
    116122
    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. 
     123In Table \ref{TabVerif}, we compare the execution time and the number of refinment
     124between 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
     127enabled 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
     129version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of
     13027 verifed components properties to be selected in VCI-PI plateform.
     131In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
    118132
    119133
    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.
     134In 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
     137our disposal 103 verified component properties and after the selection process
     138for the initial abstraction, 3 selected component properties were sufficient
     139to verify both global properties without refinement.
    121140
    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 the more connected components, in contrary to the other two methods, our computation time remains stable.
     141Globally, 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.
    123142
    124143

  • papers/FDL2012/framework.tex

    r86 r89  
    4848
    4949\subsection{Concrete system definition}
    50 As mention earlier, our concrete model consists of several components and each
     50As mentioned earlier, our concrete model consists of several components and each
    5151component comes with its specification.
    5252The concrete system is a synchronous composition of components, each of which
    … …  
    178178Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property
    179179of a component $C_j$ of M,  $\widehat{M}_{i+1} = \widehat{M_i}\parallel
    180 AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}}
     180AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M}_{i+1}
    181181\sqsubseteq \widehat{M}_i$.
    182182\end{property}
    … …  
    185185Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$
    186186and $s_{\varphi_j^k} \in S_{\varphi_j^k}$.
    187 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
     187The label of $s_{i+1}$ is obtained by applying the Belnap's logic operators
     188{\it and} to the  four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in
    188189AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
    189190\begin{itemize}
    … …  
    196197(resp. $s_{\varphi_j^k}$).
    197198\end{itemize}
    198 By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by
     199By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
     200$\widehat{M}_i$ and by
    199201the property of parallel composition,
    200202$\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$).

  • papers/FDL2012/introduction.tex

    r83 r89  
    3939
    4040
    41 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.
     41In 2007, a method to build abstractions of components into AKS (Abstract
     42Kripke Structure), based on the set of the properties (CTL) each component
     43verifies \cite{braunstein07ctl_abstraction}. The method is actually a
     44tentative to associate compositional and abstraction-refinement verification
     45techniques. The generations of AKS from CTL formula have been successfully
     46automated \cite{bara08abs_composant}. This work will be the base of the techniques in this paper.
    4247
    4348

  • papers/FDL2012/ordering_filter_properties.tex

    r82 r89  
    1515%behaviors that may have an impact on the global property.
    1616We observed that
    17 the more closer a variable is from the primary
    18 variable the more it affects the primary variable. Hence, a property
    19 has higher priority according to the number of primary or close to primary variables it
    20 contains.
     17the closer a variable is from the primary
     18variable, the higher influence it has on it.
     19%Hence, a property
     20%has higher priority according to the number of primary or close to primary variables it
     21%contains.
    2122Moreover, a global property often specifies the behavior at the interface of
    2223components. Typically, a global property ensures that a message sent is
    2324always acknowledged or the good target gets the message. This kind of behavior
    2425relates the input-output behaviors of components.
    25 We have decided to allocate an extra weight for variables which are present at the interface of a component
     26We have decided to allocate an extra weight for interface variables
    2627whereas variables which do not interfere with a primary variable are weighted 0.
    2728Here is how we proceed:
    … …  
    4445\label{algo:weight}
    4546
    46 \KwIn{ $\{V\}$, the set of all dependency graph variable}
     47\KwIn{ $G$, the set of all dependency graph variable}
     48{ $V$ the set of variables}
    4749\KwOut{$\{(v,w)| v \in V, w \in N\}$, The set of variables with their weight}
    4850
    4951\Begin{
    50 $p = $ max(depth(V))  \\
     52$p = $ max(depth(G))  \\
    5153\For{$v\in V$}{
    52         d = depth(v) \;
     54        $d$ = depth($v$) \;
    5355        $w = 2^{p-d}*p$\;
    54         \If(v is primary variable){$d == 0$}
     56        \If($v$ is primary variable){$d == 0$}
    5557        {
    5658                $w = 5 * w$\;
    5759        }
    58         \If(v is an interface variable){$v\in{I\cup O}$}
     60        \If($v$ is an interface variable){$v\in{I\cup O}$}
    5961        {
    6062                $w = 3 * w $
    … …  
    134136It is definitely not an exact pertinence calculation of properties but provides a good indicator
    135137of their possible impact on the global property.
    136 After this pre-processing phase, we  have a list of properties $L_\phi$
     138After this pre-processing phase, we  have a list of properties
    137139ordered according to their pertinence with regards to the global property.
    138140
    … …  
    149151%are characterized. Hence there is more constrains behavior and more concretize
    150152%states.
    151 As we would like to ensure the elimination of the counter-example previously found,
     153As we would like to ensure the elimination of the counterexample previously found,
    152154we filter out properties that do not have an impact on the counterexample
    153155$\sigma$ thus will not eliminate it.
    154156In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
    155157is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies
    156 the global property $\Phi$
     158the global property~$\Phi$
    157159%as show in figure \ref{AKSNegCex}.
    158160%In case where the spurious counter-example exhibits a bounded path, we add a last
    … …  
    172174%
    173175\begin{definition}
    174 Let $\sigma$ be a counter-example of length $n$ in $\widehat{M}_i$ such
     176Let $\sigma$ be a counterexample of length $n$ in $\widehat{M}_i$ such
    175177that $ \sigma =  s_{0}\rightarrow  s_{1}\rightarrow \ldots \rightarrow
    176178s_{n-1}$. The \emph{Kripke structure derived from $\sigma$} is 6-tuple
    … …  
    240242
    241243All the properties available for refinement are then model-checked on $K(\sigma)$. If the
    242 property holds then the property will not discriminate the counterexample.
     244property holds then the property will not eliminate the counterexample.
    243245Hence this property is not a good candidate for refinement.
    244 Therefore all properties that are not satisfied are chosen to be
    245 integrated in the next step of refinement. At this stage, we already have a
    246 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$.
     246Therefore the highest weighted property not satisfied in $K(\sigma)$ is choosen to be
     247integrated in the next refinement step. This process is iterated for each
     248refinement step.
     249%At this stage, we already have a
     250%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$.
    247251
    248252\begin{property}{Counterexample eviction}
    … …  
    267271\end{proof}
    268272
    269 The proposed approach ensures that the refinement excludes the counter-example
     273The proposed approach ensures that the refinement excludes the counterexample
    270274and  respects the definition \ref{def:goodrefinement}.
    271275We will show in our experiments that first the time needed to build an AKS is
Note: See TracChangeset for help on using the changeset viewer.