![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 56 for papers/FDL2012/framework.tex
- Timestamp:
- Mar 8, 2012, 2:00:31 PM (13 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/framework.tex (modified) (7 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/framework.tex
r52 r56 5 5 concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is 6 6 generated and tested in the model-checker. As the abstract model is an 7 upper-approximation of the concrete model and we have restrained our7 over-approximation of the concrete model and we have restrained our 8 8 verification 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. 9 9 However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, … … 15 15 %are CTL formulas with only universal path quantifiers: AX, AF, AG and AU. 16 16 %\end{definition} 17 \remark{Cecile}{remettre la défintion du modÚle concret} 17 18 18 \begin{definition} 19 19 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: … … 36 36 \end{figure} 37 37 38 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$. 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}.38 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$. 39 39 40 40 In 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 \TODO{ref du papier sur le spurious + petite explication sur SAT et 42 déroulement} 43 \subsection{Concrete system definition} 41 44 42 \subsection{Definition of the abstraction of a component and of the complete system} 45 The concrete system is a synchronous compositon of components, each of which 46 described as a Moore machine. 47 \begin{definition} 48 A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where, 49 \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). 53 \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function. 54 \item $\lambda : 2^R \rightarrow 2^O$ is the output function. 55 \item $\mathbf{R}_0 \subseteq 2^R$ is the set of initial states. 56 \end{itemize} 57 \end{definition} 43 58 44 The 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. 59 \emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements. From now on, let $C = \langle I, O, R, \delta, \lambda, \mathbf{R}_0 \rangle$ be a sequential circuit. 60 61 \begin{definition} 62 A \emph{Concrete system} $M$ is obtained by synchronous composition of the 63 component.\\ 64 $M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a 65 Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots 66 \varphi_i^k\}$ Each $\varphi_i^j$ being a CTL$\setminus$X formula whose 67 propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ . 68 \end{definition} 69 70 \subsection{Abstraction definition} 71 72 Our abstraction consists in reducing the size of the representation model by 73 freeing some its variables. The point is to determine the good set of variable 74 to be freed and when to free them. We take advantage of the CTL specification 75 of each component: a CTL property may be seen as a partial view of the tree of 76 behaviors of its variables. All the variables not specified by the property 77 can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly 78 specifies when the variable of the prperty can be frreed. 79 The abstraction of a component is represented by an AKS, 80 derived from a subset of the CTL properties the component satisfies. 81 Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property 82 $\varphi$, simulates all execution trees whose initial state satisfies 83 $\varphi$. In AKS($\varphi$), states are tagged with the truth values of 84 $\varphi$'s atomic propositions, among four truth values : inconsistent, 85 false, true and unknown (either true or false). 86 States with inconsistent truth values are not represented since they refer to non possible 87 assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. 45 88 46 89 … … 71 114 72 115 As 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. 116 The AKS composition has been defined in \cite{these_braunstein}; it extends 117 the classical synchrounous composition of Moore machine to deal with 118 four-valued variables. 73 119 %\bigskip 74 120 … … 79 125 \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 126 \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 127 \end{itemize} 83 128 … … 90 135 91 136 137 The generation of an abstract model in the form of AKS from CTL formulas, 138 based on the works of Braunstein \cite{braunstein07ctl_abstraction}, 139 has been successfully implemented by Bara \cite{bara08abs_composant}. 92 140 93 141 … … 95 143 TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ?? 96 144 97 1. Ordering of AKS 145 \begin{definition} 146 A state $s$ is an abstract state if one its variable $p$ is {\it unknown}. It 147 is concise representation of the set of more concrete states in which $p$ 148 is either true or false. 149 \end{definition} 98 150 99 Def : Concrete and abstract variables in AKS 151 \begin{definition} 152 The {\emph concretization} of an abstract $s$ with respect to the variable $p$ 153 ({\it unknown} in that state), assigns either true or false to $p$. 100 154 101 Def : Concretization of an abstract variable 155 The {\emph abstraction} of a state $s$ with respect to the variable $p$ 156 (either true or false in that state), assigns {\it unknown} to $p$. 157 \end{definition} 102 158 103 Def (dual) : Abstraction of a concrete variable 159 \begin{property} 160 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. 161 \end{property} 162 \begin{proof} 163 As the concretization of state reduces the set of concrete configuration the 164 abstract state represents but does not affect the transition relation of the 165 AKS. The unroll execution tree of A2 is a subtree of the one of A1. Then A1 simulates A2. 166 \end{proof} 104 167 105 Prop : 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 107 A 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 168 109 169 2. Negation of states in an AKS
Note: See TracChangeset
for help on using the changeset viewer.
