source: papers/FDL2012/framework.tex @ 52

Last change on this file since 52 was 52, checked in by cecile, 13 years ago

Decomposition de papier en fichier

File size: 9.1 KB
Line 
1The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. 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}.
2
3\subsection{Overall Description of our methodology}
4In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
5concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
6generated and tested in the model-checker. As the abstract model is an
7upper-approximation of the concrete model and we have restrained our
8verification to ACTL properties only, if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well.
9However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
10$\sigma$ given by the model-checker has been analyzed. \remark{Cecile}{cite
11Grumberg ovver-approx et ACTL poperties}
12%\bigskip
13%\begin{definition}
14%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas 
15%are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
16%\end{definition}
17\remark{Cecile}{remettre la défintion du modÚle concret}
18\begin{definition}
19Given $\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:
20
21\begin{itemize}
22\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
23\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. }
24\end{itemize}
25\end{definition}
26
27%\bigskip
28We 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}.
29
30\begin{figure}[h!]
31%   \centering
32%   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
33%     \hspace*{-5mm}
34     \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
35   \caption{\label{cegar} Verification Process }
36\end{figure}
37
38As 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$. The generation of an abstract model in the form of AKS from CTL formulas, based on the works of Braunstein \cite{braunstein07ctl_abstraction}, has been successfully implemented by Bara \cite{bara08abs_composant}.
39
40In the case where model-checking failed, the counterexample given by the model-checker \cite{ucberkeley96vis}  has to be analysed. We use a SATSolver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
41
42\subsection{Definition of the abstraction of a component and of the complete system}
43
44The abstraction of a component is represented by an Abstract Kripke Structure (AKS for short), derived from a subset of the CTL properties the component satisfies. Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property $\varphi$, simulates all execution trees whose initial state satisfies $\varphi$. In AKS($\varphi$), states are tagged with the truth values of $\varphi$'s atomic propositions, among four truth values : inconsistent, false, true and unknown (or undefined). States with inconsistent truth values are not represented since they refer to non possible assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
45
46 
47%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}.
48The AKS associated with a CTL property $\varphi$ whose set of atomic propositions is $AP$ is a 6-tuple, \\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows:
49
50\begin{definition}
51An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :
52
53\begin{itemize}
54\item { $\widehat{AP}$ : a finite set of atomic propositions}   
55\item { $\widehat{S}$ : a finite set of states}
56\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
57\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:}
58                \begin{itemize}
59                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
60                        \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
61                        \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
62                  \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
63                \end{itemize}
64\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}$ }
65\item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi
66acceptance condition)}
67\end{itemize}
68\end{definition}
69%\bigskip
70
71
72As 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.
73%\bigskip
74
75\begin{definition}
76Let $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]$:
77
78\begin{itemize}
79\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
80\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
81\item{$ V_{\widehat{C}_j} \subseteq V_{C_j}$ (with $V_{\widehat{C}_j}$ and $V_{C_j}$ are variables of $\widehat{C}_j$ and $C_j$ respectively.) TODO : LES V ICI NE SONT-ELLES PAS L'UNION DES AP DES $\varphi_{C_j^k}$ ???????}
82\end{itemize}
83
84\hspace*{3mm}with :\\
85\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
86\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
87
88\end{definition}
89%\bigskip
90
91
92
93
94\subsection{Characterization of AKS}
95TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
96
971. Ordering of AKS
98
99Def : Concrete and abstract variables in AKS
100
101Def : Concretization of an abstract variable
102
103Def (dual) : Abstraction of a concrete variable
104
105Prop : Let A1 and A2 two AKS 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.
106
107A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ???
108 
1092. Negation of states in an AKS
110
111a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
112
113b) The negation of an configuration may be represented by a set of abstract configurations
114
115c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
116
117
Note: See TracBrowser for help on using the repository browser.