source: papers/FDL2012/framework.tex @ 103

Last change on this file since 103 was 101, checked in by syed, 12 years ago

final

File size: 13.4 KB
Line 
1The model-checking technique we propose is based on the Counterexample-guided
2Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
3description of our methodology is shown in Figure \ref{cegar}.
4We take into account the structure of the system as a set of synchronous components,
5each of which has been previously verified and a set of CTL properties is
6attached to each component. This set refers to the specification of the
7component. We would like to verify whether a concrete model, $M$ presumably
8big sized and composed of several components, satisfies a global ACTL property $\Phi$.
9%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.
10Instead 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}.
11
12%\subsection{Overall Description of our methodology}
13%In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
14%concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
15%generated and tested in the model-checker. As the abstract model is an
16%over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment,
17As shown in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
18holds in the abstract model then it holds in the concrete model as well.
19However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed.
20The test of spurious counter-example is then translated into a
21SAT 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.
22
23%\bigskip
24%\begin{definition}
25%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas
26%are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
27%\end{definition}
28
29%\begin{definition}
30%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:
31%
32%\begin{itemize}
33%\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
34%\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. }
35%\end{itemize}
36%\end{definition}
37
38%\bigskip
39%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}.
40
41\begin{figure}[h!]
42%   \centering
43%   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
44%     \hspace*{-5mm}
45     \includegraphics[scale=0.37]{our_framework_cegar_png}
46   \caption{\label{cegar} Verification Process }
47\end{figure}
48
49\vspace*{-5mm}
50\subsection{Concrete system definition}
51As mentioned earlier, our concrete model consists of several components and each
52component comes with its specification.
53The concrete system is a synchronous composition of components, each of which
54described as a Moore machine.
55\begin{definition}
56A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
57\vspace*{-2mm}
58\begin{itemize}
59%\partopsep= -1.0em
60%\topsep -0.5em
61\itemsep -0.3em
62\item $I$ is a finite set of Boolean input signals.
63\item $O$ is a finite set of Boolean output signals.
64\item $R$ is a finite set of Boolean sequential elements (registers).
65\item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
66\item $\lambda : 2^R \rightarrow 2^O$ is the output function.
67\item $\mathbf{R}_0 \subseteq 2^R$ is the set of initial states.
68\end{itemize}
69\end{definition}
70
71\emph{States} (or configurations) of the circuit correspond to Boolean configurations of all the sequential elements.
72
73\begin{definition}
74A \emph{Concrete system} $M$ is obtained by synchronous composition of the
75component.\\
76$M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
77Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
78\varphi_i^k\}$. Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
79propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ .
80\end{definition}
81
82\subsection{Abstraction definition}
83
84Our abstraction reduces the size of the representation model by
85letting free some of its variables. The point is to determine the good set of variable
86to be freed and when to free them. We take advantage of the CTL specification
87of each component: a CTL property may be seen as a partial view of the tree of
88behaviors of its variables. All the variables not specified by the property
89can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
90specifies when the variable of the property can be freed.
91The abstraction of a component is represented by an AKS,
92derived from a subset of the CTL properties the component satisfies.
93Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property
94$\varphi$, simulates all execution trees whose initial state satisfies
95$\varphi$. In AKS($\varphi$), states are tagged with the truth values of
96$\varphi$'s atomic propositions, among the four truth values of Belnap's logic \cite{belnap77}: inconsistent ($\bot$),
97false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)).
98States with inconsistent truth values are not represented since they refer to non possible
99assignments of the atomic propositions. A set of fairness constraints
100eliminates non-progress cycles. The transformation algorithm of a
101CTL$\setminus$X property into an AKS is described in
102\cite{braunstein07ctl_abstraction,braunstein_phd07}.
103
104
105%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}.
106
107\begin{definition}{\label{def-aks}}
108Given a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is
109$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:
110
111\vspace*{-3mm}
112\begin{itemize}
113%\partopsep=0pt
114%\topsep 0pt
115\itemsep -0.3em
116\item { $AP$ : The finite set of atomic propositions of property $\varphi$ }   
117\item { $\widehat{S}$ : a finite set of states}
118\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
119\item { $\widehat{L} : \widehat{S} \rightarrow \cal{B}^{\mid AP \mid}$ with $\cal{B} = \{\bot, \mathbf{f}, \mathbf{t},\top\}$: a labeling function which labels each state with configuration of current value of each atomic proposition.}
120\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}$ }
121\item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi
122acceptance condition)}
123\end{itemize}
124\end{definition}
125%\bigskip
126
127\vspace*{-2mm}
128We denote by $\widehat{L}(s)$, the configuration of atomic propositions in state $s$, and by $\widehat{L}(s)[p]$, the projection of configuration $\widehat{L}(s)$ according to atomic proposition $p$.
129
130
131As 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.
132The AKS composition has been defined in \cite{braunstein_phd07}; it extends
133the classical synchronous composition of Moore machine to deal with
134four-valued variables.
135%\bigskip
136
137\begin{definition} An \emph{Abstract model} $\widehat{M}$ is obtained by
138synchronous composition of components abstractions. Let $n$ be the number of components in the model and $m$ be the number of selected verified properties of a component;
139let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
140
141\vspace*{-3mm}
142\begin{itemize}
143%\topsep 0pt
144\itemsep -0.3em
145\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
146\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
147\end{itemize}
148
149\end{definition}
150
151
152%The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}).
153
154
155%\subsection{Characterization of AKS}
156
157In an AKS, a state where a variable $p$ is {\it unknown}
158can simulate all states in which $p$ is either true or false. It
159is a concise representation of the set of more concrete states in which $p$
160is either true or false.  A state $s$ is said to be an \emph{abstract state}
161if one of its variable $p$ is {\it unknown}.
162
163%\begin{definition}
164%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}.
165%\end{definition}
166
167\begin{definition}[]
168The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
169({\it unknown} in that state), assigns either true or false to $p$.\\
170The \emph {abstraction} of a state $s$ with respect to the variable $p$
171(either true or false in that state), assigns  {\it unknown} to $p$.
172\end{definition}
173
174\begin{property}[Concretization]
175\label{prop:concrete}
176Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by
177concretizing one abstract variable of $A_i$ (resp. $A_i$ is obtained by
178abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by
179$A_j \sqsubseteq A_i$.
180\end{property}
181\begin{proof}
182As the concretization of state reduces the set of concrete configuration the
183abstract state represents but does not affect the transition relation of the
184AKS. The unroll execution tree of $A_j$ is a sub-tree of the one of $A_i$. Then
185$A_i$ simulates $A_j$.
186\end{proof}
187
188\begin{property}[Composition and Concretization]
189\label{prop:concrete_compose}
190Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property
191of a component $C_j$ of M,  $\widehat{M}_{i+1} = \widehat{M_i}\parallel
192AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M}_{i+1}
193\sqsubseteq \widehat{M}_i$.
194\end{property}
195
196\begin{proof}
197Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$
198and $s_{\varphi_j^k} \in S_{\varphi_j^k}$.
199The label of $s_{i+1}$ is obtained by applying the Belnap's logic operators
200{\it and} to the  four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in
201AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
202\vspace*{-2mm}
203\begin{itemize}
204%\topsep 0pt
205\itemsep -0.3em
206\item  $\widehat{L}_{i+1}[p] = \top$ iff  p is {\it unknown} in both states or
207does not belong to the set of atomic proposition.
208\item  $\widehat{L}_{i+1}[p] = \mathbf{t}$ (or $\mathbf{f}$) iff $p$ is true
209(or false) in $s_{\varphi_j^k}$ (resp. $s_i$)  and {\it unknown} in $s_i$
210(resp. $s_{\varphi_j^k}$).
211\end{itemize}
212\vspace*{-2mm}
213By Property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
214$\widehat{M}_i$ and by
215the property of parallel composition,
216$\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$).
217\end{proof}
218
219\vspace*{-5mm}
220\subsection{Initial abstraction}
221Given 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$.
222%We suppose that our concrete model is a composition of several components and
223%each component has been previously verified. Hence, we have a set of verified
224%properties for each component of the concrete model. The main idea of this
225%technique is that we would like to make use of these properties to generate a
226%better abstract model. Properties of the components that appear to be related
227%to the global property to be verified, $\Phi$ are selected to generate the
228%abstract model $\widehat{M}_i$. This method is particularly interesting as it
229%gives a possibility to converge quicker to an abstract model that is
230%sufficient to satisfy the global property $\Phi$.
231%In the following, we will name primary variables the set of variable that
232%appears in the global property.
233In the initial abstraction generation, all variables that appear in $\Phi$ have to be
234represented. Therefore the properties in the specification of each component
235where these variables are present will be used to generate the initial
236abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the
237global 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.
238
239
Note: See TracBrowser for help on using the repository browser.