source: papers/FDL2012/FDL2012.tex @ 81

 \documentclass{article}

  \usepackage{spconf}
\usepackage{cmap}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{bbm}
\usepackage{bbold}
\usepackage{amsthm}
\usepackage{array}
\usepackage{verbatim}
\usepackage{hyperref}
\usepackage{booktabs}
\usepackage{graphicx}
\usepackage{tikz}
\usepackage{pgf}
\usetikzlibrary{arrows,automata}
\usepackage[francais, american]{babel}
\usepackage[babel=true,kerning=true]{microtype}
\usepackage[ruled]{algorithm2e}


\graphicspath{{schema/}}
\newtheorem{definition}{Definition}
\newtheorem{property}{Property}
\newcommand{\TODO}[1] {\textcolor{red}{TODO : #1}}
\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}


 \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinement process}
 \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN}
% \thanks{This work was supported by...}}
 \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
                 LIP6-SOC (CNRS UMR 7606), \\
                            4, place Jussieu, \\
                75005 Paris, FRANCE. }

\begin{document}
 % OPTIONAL -->   \ninept            <-- OPTIONAL, for nine pt only

\maketitle

\begin{abstract}
Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have conducted several preliminary experimentations which shows that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS \cite{ucberkeley96vis}.
\end{abstract}

\begin{keywords}
Compositional verification, CTL properties, CEGAR, model-checking
\end{keywords}


%\def\abstract{\begin{center}
%{\bf ABSTRACT\vspace{-.5em}\vspace{0pt}}
%\end{center}}
%\def\endabstract{\par}

\section{Introduction}

\input{introduction}


\section{Our Framework}

\input{framework}
\section{Refinement}

\input{abstraction_refinement}



\section{Experimental results}

 \input{exp_results}




\section{Conclusion and Future Works}

%\section*{Drawbacks}

We have presented a new strategy in the abstraction generation and refinement which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of complex systems. Our preliminary experimental results shows an interesting performance in terms duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.

Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoqued by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases.



%\begin{thebibliography}
 \ninept
%  <-- OPTIONAL, for nine pt only
%\bibliographystyle{plain}
\bibliographystyle{IEEEbib}
\bibliography{myBib}

%\end{thebibliography}



\end{document}