Index: /papers/FDL2012/FDL2012.tex =================================================================== --- /papers/FDL2012/FDL2012.tex (revision 49) +++ /papers/FDL2012/FDL2012.tex (revision 50) @@ -40,5 +40,5 @@ \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. @@ -48,5 +48,5 @@ Compositional verification, CTL properties, CEGAR, model-checking \end{keywords} - + %\def\abstract{\begin{center} @@ -54,5 +54,5 @@ %\end{center}} %\def\endabstract{\par} - + \section{Introduction} @@ -63,25 +63,25 @@ -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. +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. +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. @@ -90,8 +90,8 @@ -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. +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. @@ -102,12 +102,49 @@ \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 : +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}. + +\subsection{Overall Description of our methodology} +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. +%\bigskip +\begin{definition} +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. +\end{definition} + +TODO : FAUT-IL METTRE CETTE DEFINITION DE $\Phi$ ?? + +\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 $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows: + +\begin{itemize} +\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed } +\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. } +\end{itemize} +\end{definition} + +%\bigskip +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}. + +\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} + +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}. + +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. + +\subsection{Definition of the abstraction of a component and of the complete system} + +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. + + +%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}. +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: + +\begin{definition} +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 : \begin{itemize} @@ -123,11 +160,11 @@ \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. +\item { $\widehat{F}$ : a set of fairness constraints TODO : PRECISER LEUR REPRESENTATION ET LES ARBRES ACCEPTES} +\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 @@ -136,10 +173,10 @@ \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{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 :\\ +\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}$ ???????} +\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 @@ -149,46 +186,28 @@ -\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. + + +\subsection{Characterization of AKS} +TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ?? + +1. Ordering of AKS + +Def : Concrete and abstract variables in AKS + +Def : Concretization of an abstract variable + +Def (dual) : Abstraction of a concrete variable + +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. + +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 ??? + +2. Negation of states in an AKS + +a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component. + +b) The negation of an configuration may be represented by a set of abstract configurations + +c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS @@ -205,5 +224,5 @@ \begin{property} -All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. +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 @@ -235,5 +254,5 @@ %\bigskip -\begin{definition} +\begin{definition} \textbf{\emph{Spurious counterexample :}} \\ \\ @@ -242,5 +261,5 @@ \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}. +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} @@ -260,5 +279,5 @@ \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. +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})) $. @@ -267,7 +286,7 @@ \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} +\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$ + \\ \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}$ @@ -285,5 +304,5 @@ \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$. +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$. @@ -296,5 +315,5 @@ \emph{\underline{Example:}} \\ -For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where: +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$} @@ -310,5 +329,5 @@ 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. +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 @@ -337,5 +356,5 @@ \subsection{Abstraction refinement} - + The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps: @@ -443,5 +462,5 @@ %\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. +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. @@ -450,5 +469,5 @@ %\begin{thebibliography} - \ninept + \ninept % <-- OPTIONAL, for nine pt only %\bibliographystyle{plain} @@ -460,3 +479,3 @@ -\end{document} +\end{document}