Ignore:
Timestamp:
Mar 7, 2012, 5:10:31 PM (13 years ago)
Author:
cecile
Message:

Decomposition de papier en fichier

File:
1 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r50 r52  
    2626\newtheorem{definition}{Definition}
    2727\newtheorem{property}{Property}
     28\newcommand{\TODO}[1] {\textcolor{red}{TODO : #1}}
     29\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
    2830
    2931
    … …  
    5759\section{Introduction}
    5860
    59 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.
    60 
    61 
    62 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.
    63 
    64 
    65 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.
    66 
    67 
    68 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.
    69 
    70 
    71 \subsection{Related Works}
    72 
    73 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.
    74 
    75 
    76 
    77 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.
    78 
    79 
    80 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.
    81 
    82 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.
    83 
    84 
    85 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.
    86 
    87 
    88 
    89 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.
    90 
    91 
    92 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}.
    93 
    94 
    95 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.
    96 
    97 
    98 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.
    99 
     61\input{introduction}
    10062
    10163
    10264\section{Our Framework}
    10365
    104 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}.
    105 
    106 \subsection{Overall Description of our methodology}
    107 In CEGAR loop methodology, in order to verify a global property $\Phi$ 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 $\Phi$ hold on the the abstract model then we are certain that it holds in the concrete model as well. However, if $\Phi$ 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 analyzed.
    108 %\bigskip
    109 \begin{definition}
    110 The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas  are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
    111 \end{definition}
    112 
    113 TODO : FAUT-IL METTRE CETTE DEFINITION DE $\Phi$ ??
    114 
    115 \begin{definition}
    116 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:
    117 
    118 \begin{itemize}
    119 \item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
    120 \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. }
    121 \end{itemize}
    122 \end{definition}
    123 
    124 %\bigskip
    125 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}.
    126 
    127 \begin{figure}[h!]
    128 %   \centering
    129 %   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
    130 %     \hspace*{-5mm}
    131      \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
    132    \caption{\label{cegar} Verification Process }
    133 \end{figure}
    134 
    135 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}.
    136 
    137 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.
    138 
    139 \subsection{Definition of the abstraction of a component and of the complete system}
    140 
    141 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.
    142 
    143  
    144 %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}.
    145 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:
    146 
    147 \begin{definition}
    148 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 :
    149 
    150 \begin{itemize}
    151 \item { $\widehat{AP}$ : a finite set of atomic propositions}   
    152 \item { $\widehat{S}$ : a finite set of states}
    153 \item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
    154 \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:}
    155                 \begin{itemize}
    156                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
    157                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
    158                         \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
    159                   \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
    160                 \end{itemize}
    161 \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}$ }
    162 \item { $\widehat{F}$ : a set of fairness constraints TODO : PRECISER LEUR REPRESENTATION ET LES ARBRES ACCEPTES}
    163 \end{itemize}
    164 \end{definition}
    165 %\bigskip
    166 
    167 
    168 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.
    169 %\bigskip
    170 
    171 \begin{definition}
    172 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]$:
    173 
    174 \begin{itemize}
    175 \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
    176 \item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
    177 \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}$ ???????}
    178 \end{itemize}
    179 
    180 \hspace*{3mm}with :\\
    181 \hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
    182 \hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
    183 
    184 \end{definition}
    185 %\bigskip
    186 
    187 
    188 
    189 
    190 \subsection{Characterization of AKS}
    191 TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
    192 
    193 1. Ordering of AKS
    194 
    195 Def : Concrete and abstract variables in AKS
    196 
    197 Def : Concretization of an abstract variable
    198 
    199 Def (dual) : Abstraction of a concrete variable
    200 
    201 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.
    202 
    203 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 ???
    204  
    205 2. Negation of states in an AKS
    206 
    207 a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
    208 
    209 b) The negation of an configuration may be represented by a set of abstract configurations
    210 
    211 c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
    212 
    213 
     66\input{framework}
    21467\section{Abstraction Generation and Refinement}
    21568
    216 \subsection{Generalities}
    217 
    218 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$.
    219 
    220 \subsubsection{Refinement}
    221 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:
    222 
    223 %\medskip
    224 
    225 \begin{property}
    226 All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$.
    227 \end{property}
    228 %\bigskip
    229 \begin{property}
    230 $\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$.
    231 \end{property}
    232 
    233 %\bigskip
    234 %\newpage
    235 
    236 \subsubsection{The Counterexample}
    237 
    238 
    239 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.
    240 %\medskip
    241 
    242 \begin{definition}
    243 \textbf{\emph{The counterexample $\sigma_i$ :}} \\
    244 \\
    245 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$. \\
    246 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$. \\
    247 \\
    248 (\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$.)\\
    249 
    250 %\medskip
    251 
    252 \end{definition}
    253 
    254 %\bigskip
    255 
    256 \begin{definition}
    257 \textbf{\emph{Spurious counterexample :}} \\
    258 \\
    259 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'}$.\\
    260 
    261 \smallskip
    262 
    263 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}.
    264 
    265 \end{definition}
    266 
    267 
    268 
    269 \subsection{Pre-processing and pertinency ordering of properties}
    270 
    271 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}.
    272 
    273 %\bigskip
    274 
    275 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:
    276 
    277 
    278 \begin{enumerate}
    279 
    280 \item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
    281 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.
    282 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})) $.
    283 
    284 }
    285 
    286 \item {\emph{Weight allocation for each variables} \\
    287 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:
    288 \begin{itemize}
    289 \item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
    290  \\ \hspace*{20mm} $Wv_{max_d} = p$
    291 \item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
    292 \\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
    293 \item{...}
    294 \item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
    295  \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
    296 \item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
    297  \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
    298 \end{itemize}
    299 
    300 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$.
    301 }
    302 
    303 
    304 \item {\emph{Ordering of the properties} \\
    305 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}}$ .
    306 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$.
    307 
    308 
    309 }
    310 
    311 \end{enumerate}
    312 
    313 %\bigskip
    314 
    315 \emph{\underline{Example:}}  \\
    316 
    317 For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
    318 \begin{itemize}
    319 \item{$p$ is dependent of $a$ and $b$}
    320 \item{$b$ is dependent of $c$}
    321 \item{$q$ is dependent of $x$}
    322 \item{$r$ is independent}
    323 \end{itemize}
    324 
    325 Example with unit weight= 50.
    326 The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
    327 The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
    328 The tertiary level variable $c$ is weighted $50$. \\
    329 The weight of a non-related variable is $0$.
    330 
    331 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.
    332 
    333 \bigskip
    334 \begin{figure}[h!]
    335    \centering
    336 %   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
    337 %     \hspace*{-15mm}
    338      \includegraphics{Dependency_graph_weight_PNG}
    339    \caption{\label{DepGraphWeight} Example of weighting}
    340 \end{figure}
    341 
    342 %Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 

    343 
    344 
    345 
    346 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.
    347 
    348 
    349 
    350 
    351 \subsection{Initial abstraction generation}
    352 
    353 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.
    354 
    355 
    356 
    357 \subsection{Abstraction refinement}
    358 
    359 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
    360 
    361 \begin{enumerate}
    362 
    363 \item {\emph{\underline{Step 1:}} \\
    364 
    365 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$.
    366 
    367 \bigskip
    368 
    369 \begin{definition}
    370 \textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
    371 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 \\
    372 $K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :
    373 
    374 \begin{itemize}
    375 \item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }     
    376 \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}\}$}
    377 \item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
    378 \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. }
    379 \item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
    380 \end{itemize}
    381 \end{definition}
    382 
    383 %\bigskip
    384 All the properties available are then model-checked on $K(\sigma_i)$.
    385 
    386 If:
    387 \begin{itemize}
    388 \item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
    389 \item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
    390 \end{itemize}
    391 
    392 %\bigskip
    393 
    394 
    395 \begin{figure}[h!]
    396    \centering
    397 %   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
    398 %     \hspace*{-15mm}
    399      \includegraphics{K_sigma_i_S_PNG}
    400    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    401 \end{figure}
    402 
    403 %Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 

    404 
    405 %\bigskip
    406 
    407 
    408 \begin{figure}[h!]
    409    \centering
    410 
    411 \begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm,
    412                     thick]
    413   \tikzstyle{every state}=[fill=none,draw=blue,text=black]
    414 
    415   \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
    416   \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};
    417 
    418   \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};
    419 
    420   \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
    421   \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};
    422 
    423   \path (A) edge              node {} (B)
    424             (B) edge       node {} (C)
    425             (C) edge             node {} (D)
    426             (D) edge             node {} (E);
    427 
    428 \end{tikzpicture}
    429 
    430    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    431 \end{figure}
    432 
    433 
    434 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$.
    435 
    436 }
    437 %\bigskip
    438 
    439 \item {\emph{\underline{Step 2:}} \\
    440 
    441 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}$.
    442 %\bigskip
    443 
    444 }
    445 \end{enumerate}
    446 
    447 $\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.
    448 
    449 
     69\input{abstraction_refinement}
    45070
    45171
Note: See TracChangeset for help on using the changeset viewer.