![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 68
- Timestamp:
- Mar 15, 2012, 1:43:45 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 3 edited
-
abstraction_refinement.tex (modified) (3 diffs)
-
framework.tex (modified) (8 diffs)
-
ordering_filter_properties.tex (modified) (5 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/abstraction_refinement.tex
r67 r68 7 7 %\medskip 8 8 9 \begin{definition} An efficient \emph{refinement} verifie dthe following properties:9 \begin{definition} An efficient \emph{refinement} verifies the following properties: 10 10 \begin{enumerate} 11 11 \item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$. … … 29 29 \subsection{Refinement by negation of the counterexample} 30 30 31 \TODO{Mettre la def avant ?}32 \TODO{Rafinement par négation du contre-exemple}33 31 The counterexample at a refinement step $i$, $\sigma$ is a path in the 34 32 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 49 \end{definition} 52 50 53 2. Negation of states in an AKS 51 The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps. 52 \subsubsection{step 1 : Build the structure of the AKS.} 53 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}}}, 54 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$. 55 \begin{itemize} 56 \item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$ 57 \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}}.$ 58 \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. 59 \item States $s'_0$ and $s"_0$ are initial states. 60 \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}}$. 61 \item \TODO{FAIRNESS} 62 \end{itemize} 63 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. 54 64 55 a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component. 65 \subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.} 66 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)$. 67 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. 56 68 57 b) The negation of an configuration may be represented by a set of abstract configurations 69 \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}\}\}$. 58 70 59 c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS 71 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\}$. 72 \TODO{connexion des $s"_i^k$} 60 73 74 This final AKS presents a number of states which is linear with the length of the counter-example and the number of atomic propositions. 75 76 \TODO{Revoir notation def 3 pour f,t,top et introduire notation ${L}_{i}(s'_i)[v_l]$} 77 78 Removing the spurious counter-example only has little chance to converge. 61 79 62 80 %\bigskip -
papers/FDL2012/framework.tex
r61 r68 2 2 Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall 3 3 descritpion of our methodology is shown in figure \ref{cegar}. 4 We take into account the structure of the system as a set of synchronous components, 4 We take into account the structure of the system as a set of synchronous components, 5 5 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}. 6 6 … … 10 10 generated and tested in the model-checker. As the abstract model is an 11 11 over-approximation of the concrete model and we have restrained our 12 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. 13 However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, 14 $\sigma$ given by the model-checker has been analyzed. 12 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. 13 However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, 14 $\sigma$ given by the model-checker has been analyzed. 15 15 16 16 In the case where model-checking failed, the counterexample given by the … … 20 20 %\bigskip 21 21 %\begin{definition} 22 %The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas 22 %The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas 23 23 %are CTL formulas with only universal path quantifiers: AX, AF, AG and AU. 24 24 %\end{definition} … … 45 45 46 46 \subsection{Concrete system definition} 47 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$. 47 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$. 48 48 49 49 … … 82 82 can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly 83 83 specifies when the variable of the prperty can be freed. 84 The abstraction of a component is represented by an AKS, 84 The abstraction of a component is represented by an AKS, 85 85 derived from a subset of the CTL properties the component satisfies. 86 86 Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property … … 92 92 assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. 93 93 94 95 %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}.96 94 97 \begin{definition} 95 %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}. 96 97 \begin{definition}{\label{def-aks}} 98 98 Given a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is 99 99 $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 142 143 143 The generation of an abstract model in the form of AKS from CTL formulas, 144 based on the works of Braunstein \cite{braunstein07ctl_abstraction}, 144 based on the works of Braunstein \cite{braunstein07ctl_abstraction}, 145 145 has been successfully implemented by Bara \cite{bara08abs_composant}. 146 146 … … 155 155 156 156 %\begin{definition} 157 %A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. 157 %A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. 158 158 %\end{definition} 159 159 -
papers/FDL2012/ordering_filter_properties.tex
r67 r68 3 3 specification relevent for the proof of the global property. We propose an 4 4 heuristic to order the properties of each component depending on the structure 5 of each component. 5 of each component. 6 6 %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$. 7 7 In order to do so, the variable dependency of the variables present in global property has to be analysed. … … 11 11 12 12 The ordering of the properties will be based on the variable dependency graph 13 where the roots are primary variables. 13 where the roots are primary variables. 14 14 The variables in the model are weighted according to their dependency level 15 15 \emph{vis-à -vis} primary variables and the properties will be weighted according to the sum of the weights … … 22 22 components. Typicaly, a global property will ensure that a message sent is 23 23 always acknoledge or the good target get the message. This kind of behavior 24 relates the input-output behaviors of components. 25 We have decided to allocate an extra weight for variables which are present at the interface of a component 26 whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. 24 relates the input-output behaviors of components. 25 We have decided to allocate an extra weight for variables which are present at the interface of a component 26 whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. 27 27 Here is how we proceed: 28 28 \begin{enumerate} … … 131 131 132 132 Each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. 133 It is definitely not an exact pertinency calculation of properties but provides a good indicator 133 It is definitely not an exact pertinency calculation of properties but provides a good indicator 134 134 of their possible impact on the global property. 135 135 After this pre-processing phase, we will have a list of properties $L_\phi$ … … 142 142 The refinement step consists of adding new AKS of properties selected according to 143 143 their pertinency. This refinement respects the points 1 and 2 of definition 144 \ref{def:goodrefinement}. The first item comes form AKS definition. 144 \ref{def:goodrefinement}. The first item comes form AKS definition. 145 145 Adding a new AKS in the abstraction leads to an abstraction where more behaviors 146 146 are characterized. Hence there is more constrains behavior and more concretize 147 states. 148 149 \ Remark{Cécile}{Mettre definition, property and proof ?????}147 states. 148 149 \TODO{Cecile}{Mettre definition, property and proof ?????} 150 150 151 151 Unforutnatly, this refinement does not ensure that the spurious counter-example 152 is evicted. 152 is evicted. 153 153 As we would like to ensure the elimination of the counterexample previously found, 154 we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. 154 we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. 155 155 In order to reach this obective, a AKS of the counterexample $\sigma_i$, $K(\sigma_i)$ 156 is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies 156 is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies 157 157 the global property $\Phi$. It is an abstract kripke structure since not all 158 158 variables are concrete.
Note: See TracChangeset
for help on using the changeset viewer.
