Changeset 78

Timestamp:

Mar 28, 2012, 9:24:30 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

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

papers/FDL2012/introduction.tex

@@ -2 +2 @@
 
 
-Therefore, it is important to ensure, during their design phase, their correctness with respect to their specifications. Errors found late in the design of these systems is a major problem for electronic circuit designers 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, indeed, guarantees a certain level of quality in terms of safety and reliabilty while reducing financial risk.
+Therefore, it is important to ensure, during their design phase, their correctness with respect to their specifications. Errors found late in the design of these systems is a major problem for electronic circuit designers 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, indeed, guarantees a high level of quality in terms of safety and reliabilty while reducing financial risk.
 
 
@@ -8 +8 @@
 
 
-In this research 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. 
-
 
 %\subsection{Related Works}
-\emph{Related Works:} 
-We are inspired by the compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, we show that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If that's the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. Several works have manipulated this technique notably in \cite{GrumbergLong91assume_guarantee} where Grumberg and Long described the methodology using a subset of CTL in their framework and later in \cite{HQR98assume_guarantee} where Herzinger and al. presented their successful implementations and case study regarding this approach.
-
-
-
-A strategy to overcome the state explosion problem is by abstraction. A method for the construction of  an abstract state graph of an arbitrary system automatically was proposed by Graf and Saidi \cite{GrafSaidi97abstract_construct} using Pvs theorem prover. Here, the abstract states are generated from the valuations of a set of predicates on the concrete variables. The construction approach is automatic and incremental.
+\emph{Related Works:} A strategy to overcome the state explosion problem is by abstraction. A method for the construction of  an abstract state graph of an arbitrary system automatically was proposed by Graf and Saidi \cite{GrafSaidi97abstract_construct} using Pvs theorem prover. Here, the abstract states are generated from the valuations of a set of predicates on the concrete variables. The construction approach is automatic and incremental.
 
 
 A few years later, an interesting abstraction-refinement methodology called counterexample-guided abstraction refinement (CEGAR) was proposed by Clarke and al. \cite{clarke00cegar}. The abstraction was done by generating an abstract model of the system by considering only the variables that possibly have a role in verifying a particular property. In this technique, the counterexample provided by the model-checker in case of failure is used to refine the system.
 
-There have been works related to this PhD research domain in the recent years, for example, Xie and Browne have proposed a method for software verification based on composistion 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.
+
+Several tools using counterexample-guided abstraction refinement technique have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}.
 
 
-In another research, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL \cite{PMT02compositional_MC}. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee.
+The compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, it is shown that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If this is the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. Several works have manipulated this technique notably in \cite{GrumbergLong91assume_guarantee} where Grumberg and Long described the methodology using a subset of CTL in their framework and later in \cite{HQR98assume_guarantee} where Herzinger and al. presented their successful implementations and case study regarding this approach.
+
+
+
+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.
+
+
+In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee.
 
 
@@ -32 +33 @@
 
 
-Several tools using counterexample-guided abstraction refinement technique have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}.
+
+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, 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 2011, the electronic design automation group of University of Kaiserslautern suggested a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique \cite{Kunz_al11ipc_abs}. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems.
-
-
-Nevertheless, LIP6 has proposed a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component verifies in 2007  \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 automated \cite{bara08abs_composant}. These work will be the base of the techniques in this paper.
+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 tentative to associate compositional and abstraction-refinement verification techniques. The generations of AKS from CTL formula have been successfully automated \cite{bara08abs_composant}. These work will be the base of the techniques in this paper.
 
 
 %\subsection{Contribution}
-\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. 
+\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. 
 
 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.