source: papers/FDL2012/framework.tex @ 69

Last change on this file since 69 was 68, checked in by ema, 13 years ago
File size: 12.3 KB
Line 
1The model-checking technique we propose is based on the Counterexample-guided
2Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
3descritpion 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 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
7%\subsection{Overall Description of our methodology}
8In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
9concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
10generated and tested in the model-checker. As the abstract model is an
11over-approximation of the concrete model and we have restrained our
12verification 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.
13However, 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
16In the case where model-checking failed, the counterexample given by the
17model-checker  has to be analysed. We use a SAT solver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
18\TODO{ref du papier sur le spurious + petite explication sur SAT et
19déroulement}
20%\bigskip
21%\begin{definition}
22%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas
23%are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
24%\end{definition}
25
26%\begin{definition}
27%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:
28%
29%\begin{itemize}
30%\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
31%\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. }
32%\end{itemize}
33%\end{definition}
34
35%\bigskip
36%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}.
37
38\begin{figure}[h!]
39%   \centering
40%   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
41%     \hspace*{-5mm}
42     \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
43   \caption{\label{cegar} Verification Process }
44\end{figure}
45
46\subsection{Concrete system definition}
47As 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
49
50The concrete system is a synchronous compositon of components, each of which
51described as a Moore machine.
52\begin{definition}
53A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
54\begin{itemize}
55\item $I$ is a finite set of boolean inputs signals.
56\item $O$ is a finite set of boolean outputs signals.
57\item $R$ is a finite set of boolean sequential elements (registers).
58\item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
59\item $\lambda : 2^R \rightarrow 2^O$ is the output function.
60\item $\mathbf{R}_0 \subseteq 2^R$ is the set of initial states.
61\end{itemize}
62\end{definition}
63
64\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.
65
66\begin{definition}
67A \emph{Concrete system} $M$ is obtained by synchronous composition of the
68component.\\
69$M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
70Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
71\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
72propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
73\end{definition}
74
75\subsection{Abstraction definition}
76
77Our abstraction consists in reducing the size of the representation model by
78freeing some of its variables. The point is to determine the good set of variable
79to be freed and when to free them. We take advantage of the CTL specification
80of each component: a CTL property may be seen as a partial view of the tree of
81behaviors of its variables. All the variables not specified by the property
82can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
83specifies when the variable of the prperty can be freed.
84The abstraction of a component is represented by an AKS,
85derived from a subset of the CTL properties the component satisfies.
86Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property
87$\varphi$, simulates all execution trees whose initial state satisfies
88$\varphi$. In AKS($\varphi$), states are tagged with the truth values of
89$\varphi$'s atomic propositions, among four truth values : inconsistent,
90false, true and unknown (either true or false).
91States with inconsistent truth values are not represented since they refer to non possible
92assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
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
97\begin{definition}{\label{def-aks}}
98Given a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is
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:
100
101\begin{itemize}
102\item { $AP$ : The finite set of atomic propositions of property $\varphi$ }   
103\item { $\widehat{S}$ : a finite set of states}
104\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
105\item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:}
106                \begin{itemize}
107                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
108                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
109                        \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
110                  \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
111                \end{itemize}
112\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}$ }
113\item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi
114acceptance condition)}
115\end{itemize}
116\end{definition}
117%\bigskip
118
119
120As 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.
121The AKS composition has been defined in \cite{braunstein_phd07}; it extends
122the classical synchrounous composition of Moore machine to deal with
123four-valued variables.
124%\bigskip
125
126\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
127synchronous composition of components abstractions.
128Let $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]$:
129
130\begin{itemize}
131\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
132\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
133\end{itemize}
134
135\hspace*{3mm}with :\\
136\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
137\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
138
139\end{definition}
140%\bigskip
141
142
143The generation of an abstract model in the form of AKS from CTL formulas,
144based on the works of Braunstein \cite{braunstein07ctl_abstraction},
145has been successfully implemented by Bara \cite{bara08abs_composant}.
146
147
148%\subsection{Characterization of AKS}
149
150In an abstract kripke structure a state where a variable $p$ is {\it unknown}
151can simulate all states in which $p$ is either true or false. It
152is concise representation of the set of more concrete states in which $p$
153is either true or false.  A state $s$ is said to be an \emph{abstract state}
154if one its variable $p$ is {\it unknown}.
155
156%\begin{definition}
157%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}.
158%\end{definition}
159
160\begin{definition}[]
161The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
162({\it unknown} in that state), assigns either true or false to $p$.
163
164The \emph {abstraction} of a state $s$ with respect to the variable $p$
165(either true or false in that state), assigns  {\it unknown} to $p$.
166\end{definition}
167
168\begin{property}
169Let A1 and A2 two abstractions 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.
170\end{property}
171\begin{proof}
172As the concretization of state reduces the set of concrete configuration the
173abstract state represents but does not affect the transition relation of the
174AKS. The unroll execution tree of A2 is a subtree of the one of A1. Then  A1 simulates A2.
175\end{proof}
176
177\TODO{Name the simulation/concretization relation}
178
179\subsection{Initial abstraction}
180We suppose that our concrete model is a composition of several components and
181each component has been previously verified. Hence, we have a set of verified
182properties for each component of the concrete model. The main idea of this
183technique is that we would like to make use of these properties to generate a
184better abstract model. Properties of the components that appear to be related
185to the global property to be verified, $\Phi$ are selected to generate the
186abstract model $\widehat{M}_i$. This method is particularly interesting as it
187gives a possibility to converge quicker to an abstract model that is
188sufficient to satisfy the global property $\Phi$.
189In the following, we will name primary variables the set of variable that
190appears in the global property.
191
192In the initial abstraction generation, all primary variables have to be
193represented. Therefore the properties in the specification of each component
194where the primary variables are present will be used to generate the initial
195abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the
196global 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.
197
198
Note: See TracBrowser for help on using the repository browser.