Index: /papers/FDL2012/FDL2012.tex =================================================================== --- /papers/FDL2012/FDL2012.tex (revision 92) +++ /papers/FDL2012/FDL2012.tex (revision 93) @@ -33,5 +33,5 @@ - \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process} + \title{ An efficient refinement strategy exploiting component properties in a CEGAR process} % \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ} % \thanks{This work was supported by...}} @@ -96,5 +96,5 @@ complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of -eliminating the counterexample which is probably due to an uncomplete +eliminating the counterexample which is probably due to an incomplete specification or a counterexample that should be eliminated by the product of local properties. In this case, other refinement techniques such as the @@ -102,5 +102,5 @@ good set of local properties to be integreted simultaneously, should be considered. We are currently investigating other complementary techniques to overcome these particular cases. -A complementary approach consists in oimproving the specification of the +A complementary approach consists in improving the specification of the model~: at the component level, or for groups of components. The work of Kroening \cite{pwk2009-date} could help us in this direction. Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 92) +++ /papers/FDL2012/abstraction_refinement.tex (revision 93) @@ -24,8 +24,8 @@ Refinements based on the concretization of selected abstract variables in -$\widehat{M}_i$ ensure item 2. Concretization can be performed either in -modifying the AKS of $\widehat{M}_i$, by changing some abstract value to -concrete ones, but this approach is rude : in order to ensure item 1, -concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value. +$\widehat{M}_i$ ensure item 2. Concretization can be performed by +modifying the AKS of $\widehat{M}_i$ by changing some abstract value to +concrete ones. However, this approach is rude : in order to ensure item 1, +the concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value. %Another way to concretize some variables at selected instants is to compose %(by a synchronous product) the AKS of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop. @@ -96,5 +96,5 @@ \end{itemize} \end{definition} -The labeling function fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all +The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all configurations {\it but} the one of $s_i$. This last set may not be representable by the labeling function defined in def \ref{def-aks}. State labeling is treated @@ -114,5 +114,5 @@ and assigns to each of them a label of $k$ variables $\{v_0, \ldots, v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1], -v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each +v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. Each state $\bar{s_i^j}$ is connected to the same predecessor and successor states as state $\bar{s_i}$. Index: /papers/FDL2012/exp_results.tex =================================================================== --- /papers/FDL2012/exp_results.tex (revision 92) +++ /papers/FDL2012/exp_results.tex (revision 93) @@ -121,5 +121,5 @@ -In Table \ref{TabVerif}, we compare the execution time and the number of refinment +In Table \ref{TabVerif}, we compare the execution time and the number of refinement between our technique (Prop. Select.), \emph{incremental\_ctl\_verification} (Incremental) and the standard model checking (Standard MC) computed using the @@ -128,5 +128,5 @@ $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of -26 verifed components properties to be selected in VCI-PI plateform. +26 verifed components properties to be selected in VCI-PI platform. In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 92) +++ /papers/FDL2012/framework.tex (revision 93) @@ -15,6 +15,6 @@ %generated and tested in the model-checker. As the abstract model is an %over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, -As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$ -holds on the the abstract model then it holds in the concrete model as well. +As shown in \cite{clarke94model} for over-approximation abstraction, if $\Phi$ +holds in the abstract model then it holds in the concrete model as well. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed. The test of spurious counter-example is then translated into a @@ -60,6 +60,6 @@ %\topsep -0.5em \itemsep -0.3em -\item $I$ is a finite set of Boolean inputs signals. -\item $O$ is a finite set of Boolean outputs signals. +\item $I$ is a finite set of Boolean input signals. +\item $O$ is a finite set of Boolean output signals. \item $R$ is a finite set of Boolean sequential elements (registers). \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function. @@ -76,5 +76,5 @@ $M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots -\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose +\varphi_i^k\}$. Each $\varphi_i^j$ is a CTL$\setminus$X formula whose propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ . \end{definition} @@ -126,5 +126,5 @@ \vspace*{-2mm} -We 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$. +We 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$. @@ -155,9 +155,9 @@ %\subsection{Characterization of AKS} -In an AKS a state where a variable $p$ is {\it unknown} +In an AKS, a state where a variable $p$ is {\it unknown} can simulate all states in which $p$ is either true or false. It is a concise representation of the set of more concrete states in which $p$ is either true or false. A state $s$ is said to be an \emph{abstract state} -if one its variable $p$ is {\it unknown}. +if one of its variable $p$ is {\it unknown}. %\begin{definition} Index: /papers/FDL2012/introduction.tex =================================================================== --- /papers/FDL2012/introduction.tex (revision 92) +++ /papers/FDL2012/introduction.tex (revision 93) @@ -7,5 +7,5 @@ and programmers as it may delay getting a new product to the market or cause failure of some critical devices that are already in use. System verification -using formal methods such as model checking guarantee a high level of quality in terms of safety and reliability while reducing financial risk. +using formal methods such as model checking guarantees a high level of quality in terms of safety and reliability while reducing financial risk. @@ -25,5 +25,5 @@ - Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}. + Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software has been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}. @@ -34,5 +34,5 @@ -Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abtraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time. +Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abstraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time. @@ -42,5 +42,5 @@ In 2007, a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component -verifies \cite{braunstein07ctl_abstraction}. The method is actually a +verifies was presented in \cite{braunstein07ctl_abstraction}. The method is actually a tentative to associate compositional and abstraction-refinement verification techniques. The generations of AKS from CTL formula have been successfully Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 92) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 93) @@ -15,5 +15,5 @@ %behaviors that may have an impact on the global property. We observed that -the closer a variable is from the primary +the closer a variable is to the primary variable, the higher influence it has on it. %Hence, a property