![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 81 for papers/FDL2012/framework.tex
- Timestamp:
- Apr 4, 2012, 3:21:25 PM (12 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/framework.tex (modified) (7 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/framework.tex
r79 r81 3 3 description of our methodology is shown in figure \ref{cegar}. 4 4 We take into account the structure of the system as a set of synchronous components, 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 and composed of several components, satisfies a global ACTL 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}. 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$ presumably huge sized and composed of several components, satisfies a global ACTL property $\Phi$. 6 %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. 7 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 8 7 9 %\subsection{Overall Description of our methodology} 8 In CEGAR loop methodology, in order to verify a global property $\Phi$ on a 9 concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is 10 generated and tested in the model-checker. As the abstract model is an 11 over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, if $\Phi$ holds on the the abstract model then it holds in the concrete model as well \cite{clarke94model}. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample, $\sigma$, given by the model-checker has been analyzed. 12 In this last case, the test of spurious counter-example is translated into a 10 %In CEGAR loop methodology, in order to verify a global property $\Phi$ on a 11 %concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is 12 %generated and tested in the model-checker. As the abstract model is an 13 %over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, 14 As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$ 15 holds on the the abstract model then it holds in the concrete model as well. 16 However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed. 17 The test of spurious counter-example is then translated into a 13 18 SAT problem as in \cite{clarke00cegar}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed. 14 19 … … 40 45 41 46 \subsection{Concrete system definition} 42 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 $\Phi$. 43 44 47 As mention earlier, our concrete model consists of several components and each 48 component comes with its specification. 45 49 The concrete system is a synchronous composition of components, each of which 46 50 described as a Moore machine. … … 48 52 A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where, 49 53 \begin{itemize} 50 \item $I$ is a finite set of boolean inputs signals.51 \item $O$ is a finite set of boolean outputs signals.52 \item $R$ is a finite set of boolean sequential elements (registers).54 \item $I$ is a finite set of Boolean inputs signals. 55 \item $O$ is a finite set of Boolean outputs signals. 56 \item $R$ is a finite set of Boolean sequential elements (registers). 53 57 \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function. 54 58 \item $\lambda : 2^R \rightarrow 2^O$ is the output function. … … 57 61 \end{definition} 58 62 59 \emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.63 \emph{States} (or configurations) of the circuit correspond to Boolean configurations of all the sequential elements. 60 64 61 65 \begin{definition} … … 70 74 \subsection{Abstraction definition} 71 75 72 Our abstraction consists in reducingthe size of the representation model by76 Our abstraction reduces the size of the representation model by 73 77 letting free some of its variables. The point is to determine the good set of variable 74 78 to be freed and when to free them. We take advantage of the CTL specification … … 132 136 %\subsection{Characterization of AKS} 133 137 134 In an abstract Kripke structurea state where a variable $p$ is {\it unknown}138 In an AKS a state where a variable $p$ is {\it unknown} 135 139 can simulate all states in which $p$ is either true or false. It 136 140 is a concise representation of the set of more concrete states in which $p$ … … 151 155 152 156 \begin{property}[Concretization] 157 \label{prop:concrete} 153 158 Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by 154 concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by 155 abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by 156 $A_i \sqsubseteq A_j$. 159 concretizing one abstract variable of $A_i$ (resp. $A_i$ is obtained by 160 abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$ and $A_j$ 161 concretizes $A_i$ , denoted by 162 $A_j \sqsubseteq A_i$. 157 163 \end{property} 158 164 \begin{proof} 159 165 As the concretization of state reduces the set of concrete configuration the 160 166 abstract state represents but does not affect the transition relation of the 161 AKS. The unroll execution tree of $A_j$ is a subtree of the one of $A_i$. Then $A_i$ simulates $A_j$. 167 AKS. The unroll execution tree of $A_j$ is a sub-tree of the one of $A_i$. Then 168 $A_i$ simulates $A_j$. 162 169 \end{proof} 163 170 164 \begin{property}[Compos tion and Concretization]171 \begin{property}[Composition and Concretization] 165 172 \label{prop:concrete_compose} 166 173 Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property 167 174 of a component $C_j$ of M, $\widehat{M}_{i+1} = \widehat{M_i}\parallel 168 AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i}169 \sqsubseteq \widehat{M}_ {i+1}$.175 AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}} 176 \sqsubseteq \widehat{M}_i$. 170 177 \end{property} 171 178 172 179 \begin{proof} 173 By the property of the parallel composition, we have directly $\widehat{M_i} 174 \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$. 180 Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ 181 and $s_{\varphi_j^k} \in S_{\varphi_j^k}$. 182 The label of $s_{i+1}$ respects the Belnap logic operator. For all $p \in 183 AP_i \cup AP_{\varphi_j^k}$ we have the following label~: 184 \begin{itemize} 185 \topsep -.5em 186 \itemsep -0.5em 187 \item $\widehat{L}_{i+1}[p] = \top$ iff p is {\it unknown} in both states or 188 does not belong to the set of atomic proposition. 189 \item $\widehat{L}_{i+1}[p] = \mathbf{t}$ (or $\mathbf{f}$) iff $p$ is true 190 (or false) in $s_{\varphi_j^k}$ (resp. $s_i$) and {\it unknown} in $s_i$ 191 (resp. $s_{\varphi_j^k}$). 192 \end{itemize} 193 By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by 194 the property of parallel composition, 195 $\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$). 175 196 \end{proof} 176 197 177 198 \subsection{Initial abstraction} 178 We suppose that our concrete model is a composition of several components and 179 each component has been previously verified. Hence, we have a set of verified180 properties for each component of the concrete model. The main idea of this 181 technique is that we would like to make use of these properties to generate a 182 better abstract model. Properties of the components that appear to be related 183 to the global property to be verified, $\Phi$ are selected to generate the 184 abstract model $\widehat{M}_i$. This method is particularly interesting as it 185 gives a possibility to converge quicker to an abstract model that is 186 sufficient to satisfy the global property $\Phi$. 187 In the following, we will name primary variables the set of variable that 188 appears in the global property. 189 190 In the initial abstraction generation, all primary variableshave to be199 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 $\Phi$. 200 %We suppose that our concrete model is a composition of several components and 201 %each component has been previously verified. Hence, we have a set of verified 202 %properties for each component of the concrete model. The main idea of this 203 %technique is that we would like to make use of these properties to generate a 204 %better abstract model. Properties of the components that appear to be related 205 %to the global property to be verified, $\Phi$ are selected to generate the 206 %abstract model $\widehat{M}_i$. This method is particularly interesting as it 207 %gives a possibility to converge quicker to an abstract model that is 208 %sufficient to satisfy the global property $\Phi$. 209 %In the following, we will name primary variables the set of variable that 210 %appears in the global property. 211 In the initial abstraction generation, all variables that appear int $\Phi$ have to be 191 212 represented. Therefore the properties in the specification of each component 192 where the primaryvariables are present will be used to generate the initial213 where these variables are present will be used to generate the initial 193 214 abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the 194 215 global property $\Phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process.
Note: See TracChangeset
for help on using the changeset viewer.
