Changeset 56 for papers


Ignore:
Timestamp:
Mar 8, 2012, 2:00:31 PM (13 years ago)
Author:
cecile
Message:

add defintions concrete, and modify refinement, cex defintion

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r54 r56  
    6565
    6666\input{framework}
    67 \section{Abstraction Generation and Refinement}
     67\section{Refinement}
    6868
    6969\input{abstraction_refinement}

  • papers/FDL2012/abstraction_refinement.tex

    r52 r56  
    1 \subsection{Generalities}
    21
    32We suppose that our concrete model is a composition of several components and each component has been previously verified. Hence, we have a set of verified properties for each component of the concrete model. The main idea of this technique is that we would like to make use of these properties to generate a better abstract model. Properties of the components that appear to be related to the global property to be verified, $\phi$ are selected to generate the abstract model $\widehat{M}_i$. This method is particularly interesting as it gives a possibility to converge quicker to an abstract model that is sufficient to satisfy the global property $\phi$.
    43
    5 \subsubsection{Refinement}
    6 The model-checker provides a counterexample when a property failed during model-checking. The counterexample can be \emph{spurious} which means that the path is impossible in the concrete model $M$ or the counterexample is real which implies that $M \nvDash \phi $.When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined. In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ has to be conservative and respects the properties below:
     4\subsection{Properties of good refinement}
     5When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined.
     6In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ respects the properties below:
    77
    88%\medskip
    99
    1010\begin{property}
    11 All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$.
     11\begin{enumerate}
     12\item The new refinment is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
     13\item The new refinment is more concrete than the previous one:
     14$\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
     15\item The spurious counter-example in $\widehat{M}_i$ is  removed from
     16$\widehat{M_{i+1}}$.
     17\end{enumerate}
    1218\end{property}
    13 %\bigskip
    14 \begin{property}
    15 $\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$.
    16 \end{property}
    17 
    18 %\bigskip
    19 %\newpage
    20 
    21 \subsubsection{The Counterexample}
    22 
    23 
    24 The counterexample at a refinement step $i$, $\sigma_i$ is a path in the abstract model $\widehat{M}_i$ which dissatisfy $\phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
    25 %\medskip
    26 
     19
     20Moreover, the refinement steps should be easy to compute and ensure a fast
     21convergence by the minimizing the number of iteration of the CEGAR loop.
     22
     23
     24A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ???
     25
     26\TODO{discussion sur comment garantir les points 1/2/3 et le reste du bon
     27rafinement}
     28\subsection{The Counterexample}
     29
     30\TODO{Mettre la def avant}
     31\TODO{Rafinement par négation du contre-exemple}
     32The counterexample at a refinement step $i$, $\sigma$ is a path in the
     33abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
     34The spurious counter-example $\sigma$ is defined such that :
    2735\begin{definition}
    28 \textbf{\emph{The counterexample $\sigma_i$ :}} \\
     36\textbf{\emph{The counterexample $\sigma$ :}} \\
    2937\\
    30 Let $\widehat{M}_i =(\widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, \widehat{L}_i, \widehat{R}_i, \widehat{F}_i)$ and let the length of the counterexample, $|\sigma_i| = n$: $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k},$ $s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1], ~s_{\bar{a}i,k} \subseteq s_{i,k}  \in \widehat{S}_i, ~s_{\bar{a}i,0} \subseteq s_{i,0} \in \widehat{S}_{0i}$ and $(s_{i,k}, s_{i,k+1}) \in \widehat{R}_i$. \\
    31 Furthermore, for each state in $\sigma_i$ we have $s_{\bar{a}i,k} = \langle v_{\bar{a}i,k}^1, v_{\bar{a}i,k}^2, ... ,  v_{\bar{a}i,k}^p, ... , v_{\bar{a}i,k}^q \rangle$, $\forall p \in [1,q], ~v_{\bar{a}i,k}^p \in \widehat{V}_{i,k}$ with $\widehat{V}_{i,k} \in 2^q$. \\
    32 \\
    33 (\emph{\underline{Note} :} In AKS $\widehat{M}_i$, the variables are actually 3-valued : $\widehat{V}_{i,k} \in 3^q$. We differenciate the 3-valued variables  $v_{i,k}^p$ from boolean variables with $v_{\bar{a}i,k}^p$.)\\
    34 
    35 %\medskip
    36 
     38Let $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
     39\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ and let the length of the
     40counterexample, $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
     41s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
     42\begin{itemize}
     43\item All its variables are concrete: $\forall s_i$ and $\forall p\in
     44\widehat{AP}_i$, $p$ is either true or false
     45(not {\it unknown}).
     46\item  $\sigma$ is a counter-example in  $\widehat{M}_i$: $s_0\not\models \Phi$.
     47\item  $\sigma$ is not a path of the concrete system $M$: $\exists k$ such
     48that $(s_{k}, s_{k+1}) \not\in R$.
    3749\end{definition}
    3850
    3951%\bigskip
    4052
    41 \begin{definition}
    42 \textbf{\emph{Spurious counterexample :}} \\
    43 \\
    44 Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... ,  v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\
    45 
    46 \smallskip
    47 
    48 If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}.
    49 
    50 \end{definition}
    51 
    52 
    53 
    54 \subsection{Pre-processing and pertinency ordering of properties}
     53%\begin{definition}
     54%\textbf{\emph{Spurious counterexample :}} \\
     55%\\
     56%Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... ,  v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\
     57%
     58%\smallskip
     59%
     60%If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}.
     61%
     62%\end{definition}
     63
     64
     65
     66\subsection{Ordering of properties}
    5567
    5668Before generating an abstract model to verify a global property $\phi$, the verified properties of all the components in the concrete model are ordered according to their pertinency in comparison to a global property $\phi$. In order to do so, the variable dependency of the variables present in global property $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}.

  • papers/FDL2012/framework.tex

    r52 r56  
    55concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
    66generated and tested in the model-checker. As the abstract model is an
    7 upper-approximation of the concrete model and we have restrained our
     7over-approximation of the concrete model and we have restrained our
    88verification to ACTL properties only, if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well.
    99However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
    … …  
    1515%are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
    1616%\end{definition}
    17 \remark{Cecile}{remettre la défintion du modÚle concret}
     17
    1818\begin{definition}
    1919Given $\widehat{M} = (\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ an abstract model of a concrete model, $M$ and $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows:
    … …  
    3636\end{figure}
    3737
    38 As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. 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 $\varphi$. The generation of an abstract model in the form of AKS from CTL formulas, based on the works of Braunstein \cite{braunstein07ctl_abstraction}, has been successfully implemented by Bara \cite{bara08abs_composant}.
     38As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. 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 $\varphi$.
    3939
    4040In the case where model-checking failed, the counterexample given by the model-checker \cite{ucberkeley96vis}  has to be analysed. We use a SATSolver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
     41\TODO{ref du papier sur le spurious + petite explication sur SAT et
     42déroulement}
     43\subsection{Concrete system definition}
    4144
    42 \subsection{Definition of the abstraction of a component and of the complete system}
     45The concrete system is a synchronous compositon of components, each of which
     46described as a Moore machine.
     47\begin{definition}
     48A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
     49\begin{itemize}
     50\item $I$ is a finite set of boolean inputs signals.
     51\item $O$ is a finite set of boolean outputs signals.
     52\item $R$ is a finite set of boolean sequential elements (registers).
     53\item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
     54\item $\lambda : 2^R \rightarrow 2^O$ is the output function.
     55\item $\mathbf{R}_0 \subseteq 2^R$ is the set of initial states.
     56\end{itemize}
     57\end{definition}
    4358
    44 The abstraction of a component is represented by an Abstract Kripke Structure (AKS for short), derived from a subset of the CTL properties the component satisfies. Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property $\varphi$, simulates all execution trees whose initial state satisfies $\varphi$. In AKS($\varphi$), states are tagged with the truth values of $\varphi$'s atomic propositions, among four truth values : inconsistent, false, true and unknown (or undefined). States with inconsistent truth values are not represented since they refer to non possible assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
     59\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements. From now on, let $C = \langle I, O, R, \delta, \lambda, \mathbf{R}_0 \rangle$ be a sequential circuit.
     60
     61\begin{definition}
     62A \emph{Concrete system} $M$ is obtained by synchronous composition of the
     63component.\\
     64$M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
     65Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
     66\varphi_i^k\}$ Each $\varphi_i^j$ being a CTL$\setminus$X formula whose
     67propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
     68\end{definition}
     69
     70\subsection{Abstraction definition}
     71
     72Our abstraction consists in reducing the size of the representation model by
     73freeing some its variables. The point is to determine the good set of variable
     74to be freed and when to free them. We take advantage of the CTL specification
     75of each component: a CTL property may be seen as a partial view of the tree of
     76behaviors of its variables. All the variables not specified by the property
     77can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
     78specifies when the variable of the prperty can be frreed.
     79The abstraction of a component is represented by an AKS,
     80derived from a subset of the CTL properties the component satisfies.
     81Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property
     82$\varphi$, simulates all execution trees whose initial state satisfies
     83$\varphi$. In AKS($\varphi$), states are tagged with the truth values of
     84$\varphi$'s atomic propositions, among four truth values : inconsistent,
     85false, true and unknown (either true or false).
     86States with inconsistent truth values are not represented since they refer to non possible
     87assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
    4588
    4689 
    … …  
    71114
    72115As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property.
     116The AKS composition has been defined in \cite{these_braunstein}; it extends
     117the classical synchrounous composition of Moore machine to deal with
     118four-valued variables.
    73119%\bigskip
    74120
    … …  
    79125\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
    80126\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
    81 \item{$ V_{\widehat{C}_j} \subseteq V_{C_j}$ (with $V_{\widehat{C}_j}$ and $V_{C_j}$ are variables of $\widehat{C}_j$ and $C_j$ respectively.) TODO : LES V ICI NE SONT-ELLES PAS L'UNION DES AP DES $\varphi_{C_j^k}$ ???????}
    82127\end{itemize}
    83128
    … …  
    90135
    91136
     137The generation of an abstract model in the form of AKS from CTL formulas,
     138based on the works of Braunstein \cite{braunstein07ctl_abstraction},
     139has been successfully implemented by Bara \cite{bara08abs_composant}.
    92140
    93141
    … …  
    95143TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
    96144
    97 1. Ordering of AKS
     145\begin{definition}
     146A state $s$ is an abstract state if one its variable $p$ is {\it unknown}. It
     147is concise representation of the set of more concrete states in which $p$
     148is either true or false.
     149\end{definition}
    98150
    99 Def : Concrete and abstract variables in AKS
     151\begin{definition}
     152The {\emph concretization} of an abstract $s$ with respect to the variable $p$
     153({\it unknown} in that state), assigns either true or false to $p$.
    100154
    101 Def : Concretization of an abstract variable
     155The {\emph abstraction} of a state $s$ with respect to the variable $p$
     156(either true or false in that state), assigns  {\it unknown} to $p$.
     157\end{definition}
    102158
    103 Def (dual) : Abstraction of a concrete variable
     159\begin{property}
     160Let A1 and A2 two AKS such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
     161\end{property}
     162\begin{proof}
     163As the concretization of state reduces the set of concrete configuration the
     164abstract state represents but does not affect the transition relation of the
     165AKS. The unroll execution tree of A2 is a subtree of the one of A1. Then  A1 simulates A2.
     166\end{proof}
    104167
    105 Prop : Let A1 and A2 two AKS such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
    106 
    107 A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ???
    108168 
    1091692. Negation of states in an AKS
Note: See TracChangeset for help on using the changeset viewer.