Changeset 93 for papers/FDL2012/introduction.tex

Timestamp:

Apr 10, 2012, 4:30:02 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

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

papers/FDL2012/introduction.tex

@@ -7 +7 @@
 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 +25 @@
 
 
- 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 +34 @@
 
 
-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 +42 @@
 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