Changeset 68 for papers/FDL2012/framework.tex

Timestamp:

Mar 15, 2012, 1:43:45 PM (13 years ago)

Author:

ema

Message:

 

File:

• papers/FDL2012/framework.tex (modified) (8 diffs)

papers/FDL2012/framework.tex

@@ -2 +2 @@
 Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
 descritpion of our methodology is shown in figure \ref{cegar}.
-We take into account the structure of the system as a set of synchronous components, 
+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}.
 
@@ -10 +10 @@
 generated and tested in the model-checker. As the abstract model is an
 over-approximation of the concrete model and we have restrained our
-verification 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. 
-However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, 
-$\sigma$ given by the model-checker has been analyzed. 
+verification 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.
+However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
+$\sigma$ given by the model-checker has been analyzed.
 
 In the case where model-checking failed, the counterexample given by the
@@ -20 +20 @@
 %\bigskip
 %\begin{definition}
-%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas  
+%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas
 %are CTL formulas with only universal path quantifiers: AX, AF, AG and AU.
 %\end{definition}
@@ -45 +45 @@
 
 \subsection{Concrete system definition}
-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$. 
+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$.
 
 
@@ -82 +82 @@
 can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
 specifies when the variable of the prperty can be freed.
-The abstraction of a component is represented by an AKS, 
+The abstraction of a component is represented by an AKS,
 derived from a subset of the CTL properties the component satisfies.
 Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property
@@ -92 +92 @@
 assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
 
- 
-%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}. 
 
-\begin{definition}
+%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}.
+
+\begin{definition}{\label{def-aks}}
 Given a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is
 $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:
@@ -142 +142 @@
 
 The generation of an abstract model in the form of AKS from CTL formulas,
-based on the works of Braunstein \cite{braunstein07ctl_abstraction}, 
+based on the works of Braunstein \cite{braunstein07ctl_abstraction},
 has been successfully implemented by Bara \cite{bara08abs_composant}.
 
@@ -155 +155 @@
 
 %\begin{definition}
-%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. 
+%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}.
 %\end{definition}