source: papers/FDL2012/FDL2012.tex @ 48

 \documentclass{article}

  \usepackage{spconf}
\usepackage{cmap}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{bbm}
\usepackage{bbold}
\usepackage{amsthm}
\usepackage{array}
\usepackage{verbatim}
\usepackage{hyperref}
\usepackage{booktabs}
\usepackage{graphicx}
\usepackage{tikz}
\usepackage{pgf}
\usetikzlibrary{arrows,automata}
\usepackage[francais, american]{babel}
\usepackage[babel=true,kerning=true]{microtype}

\newtheorem{definition}{Definition}
\newtheorem{property}{Property}


 \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinement process}
 \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN}
% \thanks{This work was supported by...}}
 \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
                 LIP6-SOC (CNRS UMR 7606), \\
                            4, place Jussieu, \\
                75005 Paris, FRANCE. }

\begin{document}
 % OPTIONAL -->   \ninept            <-- OPTIONAL, for nine pt only

\maketitle
                 
\begin{abstract}
Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have tested this technique on a set of benchmarks which shows that our approach is promising in comparison to other abstraction-refinement techniques.
\end{abstract}

\begin{keywords}
Compositional verification, CTL properties, CEGAR, model-checking
\end{keywords}
                         

%\def\abstract{\begin{center}
%{\bf ABSTRACT\vspace{-.5em}\vspace{0pt}}
%\end{center}}
%\def\endabstract{\par}
    
\section{Introduction}

The embedded systems correspond to the integration into the same electronic circuit, a huge number of complex functionalities performed by several heterogenous components. Current SoC (System on Chips) contain multiple processors executing numerous cooperating tasks, specialized co-processors (for particular data treatment or communication purposes), Radio-Frequency components, etc. These systems are usually submitted to safety and robustness requirements.  Depending on their application domains, their failure may induce serious damages. Generally failures on these systems are unacceptable and have to be avoided.


Therefore, it is important to ensure, during their design phase, their correctness with respect to their specifications. Errors found late in the design of these systems is a major problem for electronic circuit designers 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, indeed, guarantees a certain level of quality in terms of safety and reliabilty while reducing financial risk.


The main challenge in model checking is dealing with the state space combinatorial explosion phenomenon. Systems with many components that can interact with each other or systems with data structure that can assume many different values will increase the number of state transition possibilities at a particular instance. In such cases, the number of global states will grow exponentially in function of the complexity of the system and unfortunately may surpasses our computation capacity. 


In this research we would like to contribute in the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. 


\subsection{Related Works}

We are inspired by the compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, we show that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If that's the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. Several works have manipulated this technique notably in \cite{GrumbergLong91assume_guarantee} where Grumberg and Long described the methodology using a subset of CTL in their framework and later in \cite{HQR98assume_guarantee} where Herzinger and al. presented their successful implementations and case study regarding this approach. 



A strategy to overcome the state explosion problem is by abstraction. A method for the construction of  an abstract state graph of an arbitrary system automatically was proposed by Graf and Saidi \cite{GrafSaidi97abstract_construct} using Pvs theorem prover. Here, the abstract states are generated from the valuations of a set of predicates on the concrete variables. The construction approach is automatic and incremental. 


A few years later, an interesting abstraction-refinement methodology called counterexample-guided abstraction refinement (CEGAR) was proposed by Clarke and al. \cite{clarke00cegar}. The abstraction was done by generating an abstract model of the system by considering only the variables that possibly have a role in verifying a particular property. In this technique, the counterexample provided by the model-checker in case of failure is used to refine the system. 

There have been works related to this PhD research domain in the recent years, for example, Xie and Browne have proposed a method for software verification based on composistion of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. 


In another research, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL \cite{PMT02compositional_MC}. 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 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.


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}.   


Recently, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification \cite{pwk2009-date}. The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In 2011, the electronic design automation group of University of Kaiserslautern suggested a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique \cite{Kunz_al11ipc_abs}. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems. 


Nevertheless, LIP6 has proposed a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component verifies in 2007  \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.



\section{Our Framework}

The model-checking technique used in this research is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. We would like to verify whether a concrete model, $M$ presumedly huge sized and might consist of several components, satisfies a global property $\varphi$. 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.  

\subsection{AKS generation from CTL Properties}

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, $\varphi$. The abstraction method is based on the work described in \cite{ braunstein07ctl_abstraction}. The AKS used is a 6-tuple, \\ $\widehat{M} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows:

\begin{definition}
An abstract Kripke structure,\\ $\widehat{M} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :

\begin{itemize}
\item { $\widehat{AP}$ : a finite set of atomic propositions}   
\item { $\widehat{S}$ : a finite set of states}
\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
\item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:}
                \begin{itemize}
                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
                        \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
                  \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
                \end{itemize}
\item { $\widehat{R} \subseteq \widehat{S} \times \widehat{S}$ : a transition relation where $ \forall s \in \widehat{S}, \exists s' \in \widehat{S}$ such that $(s,s') \in \widehat{R}$ }
\item { $\widehat{F}$ : a set of fairness constraints }
\end{itemize}
\end{definition}
%\bigskip


As 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. 
%\bigskip

\begin{definition}
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}
\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 $}
\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.)}
\end{itemize}

\hspace*{3mm}with :\\  
\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component

\end{definition}
%\bigskip


\begin{definition} 
The property to be verified, $\varphi$ is an ACTL formula. ACTL formulas  are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.  
\end{definition}
%\bigskip



\subsection{CEGAR Loop}

In CEGAR loop methodology, in order to verify a global property $\varphi$ on a concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is generated and tested in the model-checker. As the abstract model is an upper-approximation of the concrete model and we have restrained our verification to ACTL properties only, if $\varphi$ hold on the the abstract model then we are certain that it holds in the concrete model as well. However, if $\varphi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, $\sigma$ given by the model-checker has been analysed.    
%\bigskip

\begin{definition}
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 $\varphi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows:

\begin{itemize}
\item{$\widehat{M} \vDash \varphi \Rightarrow M \vDash \varphi$ : verification completed }
\item{$\widehat{M} \nvDash \varphi$  and  $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \varphi$ or $\widehat{M}$ is too coarse. }
\end{itemize}
\end{definition}

%\bigskip
We can conclude that the property $\varphi$ 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 \varphi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}.


%\medskip

\begin{figure}[h!]
%   \centering
%   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
%     \hspace*{-5mm}
     \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
   \caption{\label{cegar} Verification Process }
\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 


\bigskip

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 $\varphi$, 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}. 

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. 


\section{Abstraction Generation and Refinement}

\subsection{Generalities}

We 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$.

\subsubsection{Refinement}
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:

%\medskip

\begin{property}
All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. 
\end{property}
%\bigskip
\begin{property}
$\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$.
\end{property}

%\bigskip
%\newpage

\subsubsection{The Counterexample}


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.
%\medskip

\begin{definition}
\textbf{\emph{The counterexample $\sigma_i$ :}} \\
\\
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$. \\
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$. \\
\\
(\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$.)\\

%\medskip

\end{definition}

%\bigskip

\begin{definition} 
\textbf{\emph{Spurious counterexample :}} \\
\\
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'}$.\\

\smallskip

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}. 

\end{definition}



\subsection{Pre-processing and pertinency ordering of properties}

Before 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}.

%\bigskip

The ordering of the properties will be based on the variable dependency graph. The variables in the model are weighted according to their dependency level \emph{vis-Ã -vis} primary variables and the properties will be weighted according to the sum of the weights of the variables present in it. We have decided to allocate a supplementary weight for variables which are present at the interface of a component whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. Here is how we proceed:


\begin{enumerate}

\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
Each primary variable will be examined and their dependency graph is elobarated. The maximum graph depth among the primary variable dependency graphs will be identified and used to calibrate the weight of all the variables related to the global property. 
Given the primary variables of $\phi$, $V_{\phi} =  \langle v_{\phi_0}, v_{\phi_1}, ... , v_{\phi_k}, ... , v_{\phi_n} \rangle$ and $G{\_v_{\phi_k}}$ the dependency graph of primary variable $v_{\phi_k}$, we have the maximum graph depth $max_{d} = max(depth(Gv_{\phi_0}), depth(Gv_{\phi_1}), ... , depth(Gv_{\phi_k}), ... ,$\\$ depth(Gv_{\phi_n})) $.

}

\item {\emph{Weight allocation for each variables} \\
Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows:
\begin{itemize} 
\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
 \\ \hspace*{20mm} $Wv_{max_d} = p$ 
\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
\item{...}
\item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
 \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
\item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
 \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
\end{itemize}

We can see here that the primary variables are given a considerable ponderation due to their pertinency \emph{vis-Ã -vis} global  property. Furthermore, we will allocate a supplementary weight of $3Wv_{1}$ to variables at the interface of a component as they are the variables which assure the connection between the components if there is at least one variable in the dependency graph established in the previous step in the property. All other non-related variables have a weight equals to $0$.
}


\item {\emph{Ordering of the properties} \\
Properties will be ordered according to the sum of the weight of the variables in it. Therefore, given a property $\varphi_i$ which contains $n+1$ variables, $V_{\varphi_i} =  \langle v_{\varphi_{i0}}, v_{\varphi_{i1}}, ... , v_{\varphi_{ik}}, ... , v_{\varphi_{in}} \rangle$, the weight  of $\varphi_i$ , $W_{\varphi_i} = \sum_{k=0}^{n} Wv_{\varphi_{ik}}$ .
After this stage, we will check all the properties with weight $>0$ and allocate a supplementary weight of $3Wv_{1}$ for every variable at the interface present in the propery. After this process, the final weight of a property is obtained and the properties will be ordered in a list with the weight  decreasing (the heaviest first). We will refer to the ordered list of properties related to the global property $\phi$ as $L_\phi$. 


}

\end{enumerate}

%\bigskip

\emph{\underline{Example:}}  \\

For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where: 
\begin{itemize}
\item{$p$ is dependent of $a$ and $b$}
\item{$b$ is dependent of $c$}
\item{$q$ is dependent of $x$}
\item{$r$ is independent}
\end{itemize}

Example with unit weight= 50.
The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
The tertiary level variable $c$ is weighted $50$. \\
The weight of a non-related variable is $0$.

So each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property. 

\bigskip
\begin{figure}[h!]
   \centering
%   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
%     \hspace*{-15mm}
     \includegraphics{Dependency_graph_weight_PNG}
   \caption{\label{DepGraphWeight} Example of weighting}
\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 




After this pre-processing phase, we will have a list of properties $L_\phi  $ ordered according to their pertinency in comparison to the global property.




\subsection{Initial abstraction generation}

In the initial abstraction generation, all primary variables have to be represented. Therefore the first element(s) in the list where the primary variables are present will be used to generate the initial abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the global 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.



\subsection{Abstraction refinement}
  
The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:

\begin{enumerate}

\item {\emph{\underline{Step 1:}} \\

As we would like to ensure the elimination of the counterexample previously found, we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. In order to reach this obective, a Kripke Structure of the counterexample $\sigma_i$, $K(\sigma_i)$ is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies the global property $\phi$.

\bigskip

\begin{definition}
\textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
Let a counterexample of length $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]$, we have \\
$K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :

\begin{itemize}
\item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }      
\item { $S_{\sigma_i} = \{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}\}$}
\item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
\item { $L_{\sigma_i}$ : $S_{\sigma_i} \rightarrow 2^{AP_{\sigma_i}}$ : a labeling function which labels each state with the set of atomic propositions true in that state. }
\item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
\end{itemize}
\end{definition}

%\bigskip
All the properties available are then model-checked on $K(\sigma_i)$.

If:
\begin{itemize}
\item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
\item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
\end{itemize}

%\bigskip


\begin{figure}[h!]
   \centering
%   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
%     \hspace*{-15mm}
     \includegraphics{K_sigma_i_S_PNG}
   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 


%\bigskip


\begin{figure}[h!]
   \centering

\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm,
                    thick]
  \tikzstyle{every state}=[fill=none,draw=blue,text=black]

  \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
  \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};

  \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};

  \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
  \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};

  \path (A) edge              node {} (B)
            (B) edge       node {} (C)
            (C) edge             node {} (D)
            (D) edge             node {} (E);

\end{tikzpicture}

   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
\end{figure}


Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$.

}
%\bigskip

\item {\emph{\underline{Step 2:}} \\

The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
%\bigskip

}
\end{enumerate}

$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction.





\section{Experimental results}

 Work in progress... \\




\section{Conclusion and Future Works}

%\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.  

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.



%\begin{thebibliography}
 \ninept          
%  <-- OPTIONAL, for nine pt only
%\bibliographystyle{plain}
\bibliographystyle{IEEEbib}
\bibliography{myBib}

%\end{thebibliography}



\end{document}