Changeset 83 for papers/FDL2012/introduction.tex

Timestamp:

Apr 5, 2012, 1:59:16 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/introduction.tex (modified) (3 diffs)

papers/FDL2012/introduction.tex

@@ -22 +22 @@
 
 
-\textbf{\emph{Related Works:}} 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.
+\textbf{\emph{Related Works :}} 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}. 
 
 
@@ -33 +33 @@
 
 
-Recently, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification \cite{pwk2009-date}. The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems.
+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.
+
+
+In \cite{pwk2009-date}, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification . The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems.
 
 
@@ -40 +43 @@
 
 %\subsection{Contribution}
-\textbf{\emph{Contribution :}} We would like to contribute to the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. 
+\textbf{\emph{Contribution :}} In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. We propose a technique to classify component properties according to their pertinency towards the global property, thus, enabling a better selection of properties for the initial abstraction generation. Futhermore, in the case where the verification is not conclusive, we propose a technique guided by the counterexample given by the model-checker to select supplementary properties to improve the abstraction.   
+
 
 In the next section, we will give an overview of our framework and introduce the notations that will be used later. The rest of the paper is organized as follows: section 3 details our strategy of refinement. Section 4 presents the experimentation results and finally, section 5 draws the conclusions and summarize our possible future works.