Changeset 50 for papers


Ignore:
Timestamp:
Mar 6, 2012, 4:58:19 PM (13 years ago)
Author:
ema
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/FDL2012.tex

    r48 r50  
    4040
    4141\maketitle
    42                  
     42
    4343\begin{abstract}
    4444Embedded 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.
     
    4848Compositional verification, CTL properties, CEGAR, model-checking
    4949\end{keywords}
    50                          
     50
    5151
    5252%\def\abstract{\begin{center}
     
    5454%\end{center}}
    5555%\def\endabstract{\par}
    56    
     56
    5757\section{Introduction}
    5858
     
    6363
    6464
    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. 
     65The 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
     68In 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.
    6969
    7070
    7171\subsection{Related Works}
    7272
    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. 
     73We 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
     77A 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
     80A 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
     82There 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
     85In 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.
    8686
    8787
     
    9090
    9191
    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. 
     92Several 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
     95Recently, 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.
    9696
    9797
     
    102102\section{Our Framework}
    103103
    104 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. 
    105 
    106 \subsection{AKS generation from CTL Properties}
    107 
    108 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:
    109 
    110 \begin{definition}
    111 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 :
     104The 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}
     107In 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}
     110The 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
     113TODO : FAUT-IL METTRE CETTE DEFINITION DE $\Phi$ ??
     114
     115\begin{definition}
     116Given $\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
     125We 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
     135As 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
     137In 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
     141The 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}.
     145The 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}
     148An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :
    112149
    113150\begin{itemize}
     
    123160                \end{itemize}
    124161\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}$ }
    125 \item { $\widehat{F}$ : a set of fairness constraints }
    126 \end{itemize}
    127 \end{definition}
    128 %\bigskip
    129 
    130 
    131 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. 
     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
     168As 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.
    132169%\bigskip
    133170
     
    136173
    137174\begin{itemize}
    138 \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $} 
     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}) $}
    139176\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
    140 \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.)}
    141 \end{itemize}
    142 
    143 \hspace*{3mm}with :\\ 
     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 :\\
    144181\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
    145182\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
     
    149186
    150187
    151 \begin{definition}
    152 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. 
    153 \end{definition}
    154 %\bigskip
    155 
    156 
    157 
    158 \subsection{CEGAR Loop}
    159 
    160 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.   
    161 %\bigskip
    162 
    163 \begin{definition}
    164 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:
    165 
    166 \begin{itemize}
    167 \item{$\widehat{M} \vDash \varphi \Rightarrow M \vDash \varphi$ : verification completed }
    168 \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. }
    169 \end{itemize}
    170 \end{definition}
    171 
    172 %\bigskip
    173 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}.
    174 
    175 
    176 %\medskip
    177 
    178 \begin{figure}[h!]
    179 %   \centering
    180 %   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
    181 %     \hspace*{-5mm}
    182      \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
    183    \caption{\label{cegar} Verification Process }
    184 \end{figure}
    185 
    186 %Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 

    187 
    188 \bigskip
    189 
    190 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}.
    191 
    192 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.
     188
     189
     190\subsection{Characterization of AKS}
     191TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
     192
     1931. Ordering of AKS
     194
     195Def : Concrete and abstract variables in AKS
     196
     197Def : Concretization of an abstract variable
     198
     199Def (dual) : Abstraction of a concrete variable
     200
     201Prop : 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
     203A 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 
     2052. Negation of states in an AKS
     206
     207a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
     208
     209b) The negation of an configuration may be represented by a set of abstract configurations
     210
     211c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
    193212
    194213
     
    205224
    206225\begin{property}
    207 All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. 
     226All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$.
    208227\end{property}
    209228%\bigskip
     
    235254%\bigskip
    236255
    237 \begin{definition} 
     256\begin{definition}
    238257\textbf{\emph{Spurious counterexample :}} \\
    239258\\
     
    242261\smallskip
    243262
    244 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}. 
     263If $\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}.
    245264
    246265\end{definition}
     
    260279
    261280\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
    262 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. 
     281Each 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.
    263282Given 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})) $.
    264283
     
    267286\item {\emph{Weight allocation for each variables} \\
    268287Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows:
    269 \begin{itemize} 
     288\begin{itemize}
    270289\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
    271  \\ \hspace*{20mm} $Wv_{max_d} = p$ 
     290 \\ \hspace*{20mm} $Wv_{max_d} = p$
    272291\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
    273292\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
     
    285304\item {\emph{Ordering of the properties} \\
    286305Properties 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}}$ .
    287 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$. 
     306After 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$.
    288307
    289308
     
    296315\emph{\underline{Example:}}  \\
    297316
    298 For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where: 
     317For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
    299318\begin{itemize}
    300319\item{$p$ is dependent of $a$ and $b$}
     
    310329The weight of a non-related variable is $0$.
    311330
    312 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. 
     331So 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.
    313332
    314333\bigskip
     
    337356
    338357\subsection{Abstraction refinement}
    339  
     358
    340359The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
    341360
     
    443462%\section*{Drawbacks}
    444463
    445 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. 
     464We 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.
    446465
    447466Nevertheless, 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.
     
    450469
    451470%\begin{thebibliography}
    452  \ninept         
     471 \ninept
    453472%  <-- OPTIONAL, for nine pt only
    454473%\bibliographystyle{plain}
     
    460479
    461480
    462 \end{document}
     481\end{document} 
Note: See TracChangeset for help on using the changeset viewer.