\BOOKMARK [1][-]{section.1}{ Introduction}{}% 1 \BOOKMARK [2][-]{subsection.1.1}{ Related Works}{section.1}% 2 \BOOKMARK [1][-]{section.2}{ Our Framework}{}% 3 \BOOKMARK [2][-]{subsection.2.1}{ Overall Description of our methodology}{section.2}% 4 \BOOKMARK [2][-]{subsection.2.2}{ Definition of the abstraction of a component and of the complete system}{section.2}% 5 \BOOKMARK [2][-]{subsection.2.3}{ Characterization of AKS}{section.2}% 6 \BOOKMARK [1][-]{section.3}{ Abstraction Generation and Refinement}{}% 7 \BOOKMARK [2][-]{subsection.3.1}{ Generalities}{section.3}% 8 \BOOKMARK [3][-]{subsubsection.3.1.1}{ Refinement}{subsection.3.1}% 9 \BOOKMARK [3][-]{subsubsection.3.1.2}{ The Counterexample}{subsection.3.1}% 10 \BOOKMARK [2][-]{subsection.3.2}{ Pre-processing and pertinency ordering of properties}{section.3}% 11 \BOOKMARK [2][-]{subsection.3.3}{ Initial abstraction generation}{section.3}% 12 \BOOKMARK [2][-]{subsection.3.4}{ Abstraction refinement}{section.3}% 13 \BOOKMARK [1][-]{section.4}{ Experimental results}{}% 14 \BOOKMARK [1][-]{section.5}{ Conclusion and Future Works}{}% 15 \BOOKMARK [1][-]{section.6}{ References}{}% 16