Ignore:
Timestamp:
Mar 9, 2012, 5:16:33 PM (13 years ago)
Author:
cecile
Message:

reordoring of the firsts definitions

File:
1 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/framework.tex

    r57 r58  
    1 The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. We take into account the structure of the system as a set of synchronous components, each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
     1The model-checking technique we propose is based on the Counterexample-guided
     2Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
     3descritpion of our methodology is shown in figure \ref{cegar}.
     4We take into account the structure of the system as a set of synchronous components,
     5each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
    26
    3 \subsection{Overall Description of our methodology}
     7%\subsection{Overall Description of our methodology}
    48In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
    59concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
    610generated and tested in the model-checker. As the abstract model is an
    711over-approximation of the concrete model and we have restrained our
    8 verification 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.
     12verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well.
    913However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
    10 $\sigma$ given by the model-checker has been analyzed. \remark{Cecile}{cite
    11 Grumberg ovver-approx et ACTL poperties}
     14$\sigma$ given by the model-checker has been analyzed.
     15
     16In the case where model-checking failed, the counterexample given by the
     17model-checker  has to be analysed. We use a SAT solver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
     18\TODO{ref du papier sur le spurious + petite explication sur SAT et
     19déroulement}
    1220%\bigskip
    1321%\begin{definition}
    … …  
    1624%\end{definition}
    1725
    18 \begin{definition}
    19 Given $\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:
    20 
    21 \begin{itemize}
    22 \item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
    23 \item{$\widehat{M} \nvDash \Phi$  and  $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. }
    24 \end{itemize}
    25 \end{definition}
     26%\begin{definition}
     27%Given $\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:
     28%
     29%\begin{itemize}
     30%\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
     31%\item{$\widehat{M} \nvDash \Phi$  and  $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. }
     32%\end{itemize}
     33%\end{definition}
    2634
    2735%\bigskip
    28 We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}.
     36%We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}.
    2937
    3038\begin{figure}[h!]
    … …  
    3644\end{figure}
    3745
     46\subsection{Concrete system definition}
    3847As 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$.
    3948
    40 In 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
    42 déroulement}
    43 \subsection{Concrete system definition}
    4449
    4550The concrete system is a synchronous compositon of components, each of which
    … …  
    5762\end{definition}
    5863
    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.
     64\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.
    6065
    6166\begin{definition}
    … …  
    6469$M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
    6570Moore 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
     71\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
    6772propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
    6873\end{definition}
    … …  
    7176
    7277Our abstraction consists in reducing the size of the representation model by
    73 freeing some its variables. The point is to determine the good set of variable
     78freeing some of its variables. The point is to determine the good set of variable
    7479to be freed and when to free them. We take advantage of the CTL specification
    7580of each component: a CTL property may be seen as a partial view of the tree of
    7681behaviors of its variables. All the variables not specified by the property
    7782can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
    78 specifies when the variable of the prperty can be frreed.
     83specifies when the variable of the prperty can be freed.
    7984The abstraction of a component is represented by an AKS,
    8085derived from a subset of the CTL properties the component satisfies.
    … …  
    8994 
    9095%Assume that we have an abstract Kripke structure (AKS) representing the abstract model $\widehat{M}$ of the concrete model of the system M with regard to the property to be verified, $\Phi$. The abstraction method is based on the work described in \cite{ braunstein07ctl_abstraction}.
    91 The AKS associated with a CTL property $\varphi$ whose set of atomic propositions is $AP$ is a 6-tuple, \\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows:
    9296
    9397\begin{definition}
    94 An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :
     98Give a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is
     99$\widehat{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 :
    95100
    96101\begin{itemize}
    97 \item { $\widehat{AP}$ : a finite set of atomic propositions}   
     102\item { $AP$ : The finite set of atomic propositions of property $\varphi$ }   
    98103\item { $\widehat{S}$ : a finite set of states}
    99104\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
    … …  
    119124%\bigskip
    120125
    121 \begin{definition}
     126\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
     127synchronous composition of components abstractions.
    122128Let $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]$:
    123129
    … …  
    140146
    141147
    142 \subsection{Characterization of AKS}
    143 TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
     148%\subsection{Characterization of AKS}
    144149
    145 \begin{definition}
    146 A state $s$ is an abstract state if one its variable $p$ is {\it unknown}. It
     150In an abstract kripke structure a state where a variable $p$ is {\it unknown}
     151can simulate all states in which $p$ is either true or false. It
    147152is concise representation of the set of more concrete states in which $p$
    148 is either true or false.
    149 \end{definition}
     153is either true or false.  A state $s$ is said to be an \emph{abstract state}
     154if one its variable $p$ is {\it unknown}.
    150155
    151 \begin{definition}
    152 The {\emph concretization} of an abstract $s$ with respect to the variable $p$
     156%\begin{definition}
     157%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}.
     158%\end{definition}
     159
     160\begin{definition}[]
     161The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
    153162({\it unknown} in that state), assigns either true or false to $p$.
    154163
    155 The {\emph abstraction} of a state $s$ with respect to the variable $p$
     164The \emph {abstraction} of a state $s$ with respect to the variable $p$
    156165(either true or false in that state), assigns  {\it unknown} to $p$.
    157166\end{definition}
    158167
    159168\begin{property}
    160 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.
     169Let A1 and A2 two abstractions 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.
    161170\end{property}
    162171\begin{proof}
    … …  
    166175\end{proof}
    167176
    168  
    169 2. Negation of states in an AKS
     177\TODO{Name the simulation/concretization relation}
    170178
    171 a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
     179\subsection{Initial abstraction}
     180We suppose that our concrete model is a composition of several components and
     181each component has been previously verified. Hence, we have a set of verified
     182properties for each component of the concrete model. The main idea of this
     183technique is that we would like to make use of these properties to generate a
     184better abstract model. Properties of the components that appear to be related
     185to the global property to be verified, $\Phi$ are selected to generate the
     186abstract model $\widehat{M}_i$. This method is particularly interesting as it
     187gives a possibility to converge quicker to an abstract model that is
     188sufficient to satisfy the global property $\Phi$.
     189In the following, we will name primary variables the set of variable that
     190appears in the global property.
    172191
    173 b) The negation of an configuration may be represented by a set of abstract configurations
    174 
    175 c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
     192In the initial abstraction generation, all primary variables have to be
     193represented. Therefore the properties in the specification of each component
     194where the primary variables are present will be used to generate the initial
     195abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the
     196global property $\Phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process.
    176197
    177198
Note: See TracChangeset for help on using the changeset viewer.