Changeset 91 for papers/FDL2012/introduction.tex

Timestamp:

Apr 6, 2012, 4:53:13 PM (13 years ago)

Author:

cecile

Message:

intro+ blind

File:

• papers/FDL2012/introduction.tex (modified) (2 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 high level of quality in terms of safety and reliabilty while reducing financial risk.
-
-
-The main challenge in model checking is dealing with the state space combinatorial explosion phenomenon. Systems with many components that can interact with each other or systems with data structure that can assume many different values will increase the number of state transition possibilities at a particular instance. In such cases, the number of global states will grow exponentially in function of the complexity of the system and unfortunately may surpasses our computation capacity.
+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
+using formal methods such as model checking guarantees a high level of quality in terms of safety and reliabilty while reducing financial risk.
 
 
 
-%\subsection{Related Works}
+The main challenge in model checking is dealing with the state space combinatorial explosion phenomenon. %\subsection{Related Works}
 A strategy to overcome the state explosion problem is by performing abstraction. A method for the construction of an abstract state graph of an arbitrary system automatically was first 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.
 
@@ -19 +21 @@
 
 
-An alternative method to get over the state explosion problem is the compositional strategy. The 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.
+An alternative method to get over the state explosion problem is the compositional strategy. The strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. 
+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 Henzinger and al. presented their successful implementations and case study regarding this approach.
 
 
-\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}. 
+ 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}.