Index: papers/FDL2012/abstraction_refinement.tex =================================================================== --- papers/FDL2012/abstraction_refinement.tex (revision 67) +++ papers/FDL2012/abstraction_refinement.tex (revision 68) @@ -7,5 +7,5 @@ %\medskip -\begin{definition} An efficient \emph{refinement} verified the following properties: +\begin{definition} An efficient \emph{refinement} verifies the following properties: \begin{enumerate} \item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$. @@ -29,6 +29,4 @@ \subsection{Refinement by negation of the counterexample} -\TODO{Mettre la def avant ?} -\TODO{Rafinement par négation du contre-exemple} The counterexample at a refinement step $i$, $\sigma$ 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. @@ -51,12 +49,32 @@ \end{definition} -2. Negation of states in an AKS +The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps. +\subsubsection{step 1 : Build the structure of the AKS.} +Let us denote $AKS(\overline{\sigma})$ this AKS. $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, +\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$. +\begin{itemize} +\item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$ +\item Build a state $s_T$, and for each state $s_i$ in $\sigma$, build two states $s'_i$ and $s"_i$. $s_T \in S_{\overline{\sigma}}$ and forall $i$ in $[0..n-1]$ : $s'_i \in S_{\overline{\sigma}}$ and $s"_i \in S_{\overline{\sigma}}.$ +\item State labeling : $s'_i$ represents the (concrete) configuration of state $s_i$ and state $s"_i$ represents all configurations but the one of $s_i$. This last set may not be representable by the labeling function defined in def \ref{def-aks}. State labeling is treated in the second step. +\item States $s'_0$ and $s"_0$ are initial states. +\item Transitions : Forall $i$ in $[1..n-1]$, connect $s'_i$ and $s"_i$ to their predecessor state $s'_{i-1}$: $(s'_{i-1},s'_i) \in R_{\overline{\sigma}}$ and $(s'_{i-1},s"_i) \in R_{\overline{\sigma}}$ and connect all $s"$ states as predecessor of the $s_T$ state : $(s"_i,s_T) \in R_{\overline{\sigma}}$. +\item \TODO{FAIRNESS} +\end{itemize} +The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels. -a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component. +\subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.} +We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$. +The set of configurations associated with a state $s"_i$ represents the negation of the one represented by ${L}_{\overline{\sigma}}(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels. -b) The negation of an configuration may be represented by a set of abstract configurations +\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1, \ldots$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ meaning the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$. -c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS +To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$. +\TODO{connexion des $s"_i^k$} +This final AKS presents a number of states which is linear with the length of the counter-example and the number of atomic propositions. + +\TODO{Revoir notation def 3 pour f,t,top et introduire notation ${L}_{i}(s'_i)[v_l]$} + +Removing the spurious counter-example only has little chance to converge. %\bigskip Index: papers/FDL2012/framework.tex =================================================================== --- papers/FDL2012/framework.tex (revision 67) +++ papers/FDL2012/framework.tex (revision 68) @@ -2,5 +2,5 @@ Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall descritpion of our methodology is shown in figure \ref{cegar}. -We take into account the structure of the system as a set of synchronous components, +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}. @@ -10,7 +10,7 @@ generated and tested in the model-checker. As the abstract model is an over-approximation of the concrete model and we have restrained our -verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well. -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. +verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well. +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. In the case where model-checking failed, the counterexample given by the @@ -20,5 +20,5 @@ %\bigskip %\begin{definition} -%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas +%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} @@ -45,5 +45,5 @@ \subsection{Concrete system definition} -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$. +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$. @@ -82,5 +82,5 @@ can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly specifies when the variable of the prperty can be freed. -The abstraction of a component is represented by an AKS, +The abstraction of a component is represented by an AKS, derived from a subset of the CTL properties the component satisfies. Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property @@ -92,8 +92,8 @@ 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}. -\begin{definition} +%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}. + +\begin{definition}{\label{def-aks}} Given a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is $AP$, An \emph{Abstract Kripke Structure}, $AKS(\varphi) =(AP, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of: @@ -142,5 +142,5 @@ The generation of an abstract model in the form of AKS from CTL formulas, -based on the works of Braunstein \cite{braunstein07ctl_abstraction}, +based on the works of Braunstein \cite{braunstein07ctl_abstraction}, has been successfully implemented by Bara \cite{bara08abs_composant}. @@ -155,5 +155,5 @@ %\begin{definition} -%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. +%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. %\end{definition} Index: papers/FDL2012/ordering_filter_properties.tex =================================================================== --- papers/FDL2012/ordering_filter_properties.tex (revision 67) +++ papers/FDL2012/ordering_filter_properties.tex (revision 68) @@ -3,5 +3,5 @@ specification relevent for the proof of the global property. We propose an heuristic to order the properties of each component depending on the structure -of each component. +of each component. %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 has to be analysed. @@ -11,5 +11,5 @@ The ordering of the properties will be based on the variable dependency graph -where the roots are primary variables. +where the roots are primary variables. 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 @@ -22,7 +22,7 @@ components. Typicaly, a global property will ensure that a message sent is always acknoledge or the good target get the message. This kind of behavior -relates the input-output behaviors of components. -We have decided to allocate an extra 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. +relates the input-output behaviors of components. +We have decided to allocate an extra weight for variables which are present at the interface of a component +whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. Here is how we proceed: \begin{enumerate} @@ -131,5 +131,5 @@ 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 +It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property. After this pre-processing phase, we will have a list of properties $L_\phi$ @@ -142,17 +142,17 @@ The refinement step consists of adding new AKS of properties selected according to their pertinency. This refinement respects the points 1 and 2 of definition -\ref{def:goodrefinement}. The first item comes form AKS definition. +\ref{def:goodrefinement}. The first item comes form AKS definition. Adding a new AKS in the abstraction leads to an abstraction where more behaviors are characterized. Hence there is more constrains behavior and more concretize -states. - -\Remark{Cécile}{Mettre definition, property and proof ?????} +states. + +\TODO{Cecile}{Mettre definition, property and proof ?????} Unforutnatly, this refinement does not ensure that the spurious counter-example -is evicted. +is evicted. 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. +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 AKS 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 +is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies the global property $\Phi$. It is an abstract kripke structure since not all variables are concrete.