source: papers/FDL2012/FDL2012.tex @ 102

Last change on this file since 102 was 101, checked in by syed, 12 years ago

final

File size: 4.6 KB
Line 
1 \documentclass{article}
2
3  \usepackage{spconf}
4\usepackage{cmap}
5\usepackage[utf8]{inputenc}
6\usepackage[T1]{fontenc}
7\usepackage{lmodern}
8\usepackage{textcomp}
9\usepackage{amsmath}
10\usepackage{amssymb}
11\usepackage{amsfonts}
12\usepackage{bbm}
13\usepackage{bbold}
14\usepackage{amsthm}
15\usepackage{array}
16\usepackage{verbatim}
17\usepackage{hyperref}
18\usepackage{booktabs}
19\usepackage{graphicx}
20\usepackage{tikz}
21\usepackage{pgf}
22\usetikzlibrary{arrows,automata}
23\usepackage[francais, american]{babel}
24\usepackage[babel=true,kerning=true]{microtype}
25\usepackage[ruled]{algorithm2e}
26
27
28\graphicspath{{schema/}}
29\newtheorem{definition}{Definition}
30\newtheorem{property}{Property}
31\newcommand{\TODO}[1] {\textcolor{red}{TODO : #1}}
32\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
33
34%\vspace*{-15mm}
35 \title{ An efficient refinement strategy exploiting component properties in a CEGAR process}
36 \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ}
37% \thanks{This work was supported by...}}
38 \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
39                 LIP6-SOC (CNRS UMR 7606), \\
40                            4, place Jussieu, \\
41                75005 Paris, FRANCE. }
42%\name{Removed for blind review}
43%\address{ }
44
45\begin{document}
46 % OPTIONAL -->   \ninept            <-- OPTIONAL, for nine pt only
47
48\maketitle
49
50\begin{abstract}
51Embedded 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 show that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS \cite{ucberkeley96vis}.
52\end{abstract}
53
54\begin{keywords}
55Compositional verification, CTL properties, CEGAR, model-checking
56\end{keywords}
57
58
59%\def\abstract{\begin{center}
60%{\bf ABSTRACT\vspace{-.5em}\vspace{0pt}}
61%\end{center}}
62%\def\endabstract{\par}
63
64\section{Introduction}
65
66\input{introduction}
67
68
69\section{Our Framework}
70
71\input{framework}
72\section{Refinement}
73
74\input{abstraction_refinement}
75
76
77
78\section{Experimental results}
79
80 \input{exp_results}
81
82
83
84
85\section{Conclusion and Future Works}
86
87%\section*{Drawbacks}
88
89We have presented a new strategy in the abstraction generation and refinement
90which is well adapted for compositional embedded systems. This verification
91technique is compatible and suits well in the natural development process of
92complex systems. Our preliminary experimental results show an interesting
93performance in terms of duration of abstraction generation and the number of refinement iteration. Furthermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.
94
95Nevertheless, in order to function well, this refinement technique requires a
96well constituted specification of every components of the concrete model. Furthermore,
97it may be possible that none of the properties available is capable of
98eliminating the counterexample which is probably due to an incomplete
99specification or a counterexample that should be eliminated by the product of
100local properties. In this case, other refinement techniques such as the
101refinement by eliminating the counterexample only, or the identification of a
102good set of local properties to be integrated simultaneously, should be considered.
103We are currently investigating other complementary techniques to overcome these particular cases.
104The work of Kroening \cite{pwk2009-date}, for example, could also help us in improving the specification of the
105model: at the component level, or for groups of components.
106
107%A complementary approach consists in improving the specification of the
108%model~: at the component level, or for groups of components. The work of
109%Kroening \cite{pwk2009-date} could help us in this direction.
110
111
112
113
114%\begin{thebibliography}
115 \ninept
116%  <-- OPTIONAL, for nine pt only
117%\bibliographystyle{plain}
118\bibliographystyle{IEEEbib}
119\bibliography{myBib}
120
121%\end{thebibliography}
122
123%footnote for Table 1
124\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
125
126\end{document} 
Note: See TracBrowser for help on using the repository browser.