source: papers/FDL2012/introduction.tex @ 95

The embedded systems correspond to the integration into the same electronic circuit, a huge number of complex functionalities performed by several heterogenous components. Current SoC (System on Chips) contain multiple processors executing numerous cooperating tasks, specialized co-processors (for particular data treatment or communication purposes), Radio-Frequency components, etc. These systems are usually submitted to safety and robustness requirements. Depending on their application domains, their failure may induce serious damages and catastrophic consequences.


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 reliability while reducing financial risk.



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.


In 2000, 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.


Several tools using counterexample-guided abstraction refinement technique, like those implemented in the VIS model-checker, 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}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive.


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.


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.


 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}. 


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. Since, there have been other works on construction of components from interval temporal logic properties which could be used to speed up verification process \cite{SNBE06property_based} \cite{Kunz_al11ipc_abs}.

%In 2006, Hans Eveking and al. introduced a technique of normalizing properties and transforming those normalized properties into an executable design description \cite{SNBE06property_based}. The generation of abstraction from PSL/Sugar specification language could then be used in the verification process to speed up the operation. This technique also allows the tests of specifications without having to build an implementation first.
%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.




%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 2007, a method to build abstractions of components into AKS (Abstract
Kripke Structure), based on the set of the properties (CTL) each component
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
automated \cite{bara08abs_composant}. This work will be the base of the techniques in this paper.


%\subsection{Contribution}
\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.