Index: /papers/FDL2012/FDL2012.aux =================================================================== --- /papers/FDL2012/FDL2012.aux (revision 51) +++ /papers/FDL2012/FDL2012.aux (revision 52) @@ -42,26 +42,43 @@ \citation{braunstein07ctl_abstraction} \@writefile{toc}{\contentsline {section}{\numberline {2} Our Framework}{2}{section.2}} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.1} AKS generation from CTL Properties}{2}{subsection.2.1}} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.1} Overall Description of our methodology}{2}{subsection.2.1}} \citation{braunstein07ctl_abstraction} \citation{bara08abs_composant} \citation{ucberkeley96vis} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} CEGAR Loop}{3}{subsection.2.2}} \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Verification Process }}{3}{figure.1}} \newlabel{cegar}{{1}{3}{Verification Process\relax }{figure.1}{}} -\@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{3}{section.3}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{3}{subsection.3.1}} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} Definition of the abstraction of a component and of the complete system}{3}{subsection.2.2}} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.3} Characterization of AKS}{4}{subsection.2.3}} +\@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{4}{section.3}} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{4}{subsection.3.1}} \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1} Refinement}{4}{subsubsection.3.1.1}} \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.2} The Counterexample}{4}{subsubsection.3.1.2}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{4}{subsection.3.2}} -\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Example of weighting}}{5}{figure.2}} -\newlabel{DepGraphWeight}{{2}{5}{Example of weighting\relax }{figure.2}{}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{5}{subsection.3.3}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{5}{subsection.3.4}} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{5}{subsection.3.2}} +\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Example of weighting}}{6}{figure.2}} +\newlabel{DepGraphWeight}{{2}{6}{Example of weighting\relax }{figure.2}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{6}{subsection.3.3}} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{6}{subsection.3.4}} \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.3}} \newlabel{AKSNegCex}{{3}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.3}{}} -\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.4}} -\newlabel{AKSNegCex}{{4}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}} -\@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{6}{section.4}} -\@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{6}{section.5}} \bibstyle{IEEEbib} \bibdata{myBib} +\bibcite{GrumbergLong91assume_guarantee}{1} +\bibcite{HQR98assume_guarantee}{2} +\bibcite{GrafSaidi97abstract_construct}{3} +\bibcite{clarke00cegar}{4} +\bibcite{XieBrowne03composition_soft}{5} +\bibcite{PMT02compositional_MC}{6} +\bibcite{SNBE06property_based}{7} +\bibcite{microsoft04SLAM}{8} +\bibcite{berkeley07BLAST}{9} +\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{7}{figure.4}} +\newlabel{AKSNegCex}{{4}{7}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}} +\@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{7}{section.4}} +\@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{7}{section.5}} +\@writefile{toc}{\contentsline {section}{\numberline {6} References}{7}{section.6}} +\bibcite{Kroening_al07vcegar}{10} +\bibcite{pwk2009-date}{11} +\bibcite{Kunz_al11ipc_abs}{12} +\bibcite{braunstein07ctl_abstraction}{13} +\bibcite{bara08abs_composant}{14} +\bibcite{ucberkeley96vis}{15} Index: /papers/FDL2012/FDL2012.log =================================================================== --- /papers/FDL2012/FDL2012.log (revision 51) +++ /papers/FDL2012/FDL2012.log (revision 52) @@ -1,3 +1,3 @@ -This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2011) (format=pdflatex 2012.2.19) 5 MAR 2012 17:30 +This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2011) (format=pdflatex 2012.2.19) 7 MAR 2012 16:44 entering extended mode restricted \write18 enabled. @@ -1075,25 +1075,25 @@ \openout1 = `FDL2012.aux'. -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 38. -LaTeX Font Info: Try loading font information for TS1+cmr on input line 38. +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 40. +LaTeX Font Info: Try loading font information for TS1+cmr on input line 40. (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd File: ts1cmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions ) -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 38. -LaTeX Font Info: ... okay on input line 38. -LaTeX Font Info: Try loading font information for T1+lmr on input line 38. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 40. +LaTeX Font Info: ... okay on input line 40. +LaTeX Font Info: Try loading font information for T1+lmr on input line 40. (/usr/share/texlive/texmf-dist/tex/latex/lm/t1lmr.fd @@ -1101,5 +1101,5 @@ ) \AtBeginShipoutBox=\box57 -Package hyperref Info: Link coloring OFF on input line 38. +Package hyperref Info: Link coloring OFF on input line 40. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty @@ -1111,7 +1111,7 @@ \c@section@level=\count139 ) -LaTeX Info: Redefining \ref on input line 38. -LaTeX Info: Redefining \pageref on input line 38. -LaTeX Info: Redefining \nameref on input line 38. +LaTeX Info: Redefining \ref on input line 40. +LaTeX Info: Redefining \pageref on input line 40. +LaTeX Info: Redefining \nameref on input line 40. (./FDL2012.out) (./FDL2012.out) @@ -1149,14 +1149,14 @@ )) ABD: EveryShipout initializing macros -LaTeX Info: Redefining \degres on input line 38. +LaTeX Info: Redefining \degres on input line 40. Package frenchb.ldf Warning: The definition of \@makecaption has been changed, (frenchb.ldf) frenchb will NOT customise it; -(frenchb.ldf) reported on input line 38. - -LaTeX Info: Redefining \dots on input line 38. -LaTeX Info: Redefining \up on input line 38. -LaTeX Info: Redefining \microtypecontext on input line 38. +(frenchb.ldf) reported on input line 40. + +LaTeX Info: Redefining \dots on input line 40. +LaTeX Info: Redefining \up on input line 40. +LaTeX Info: Redefining \microtypecontext on input line 40. Package microtype Info: Generating PDF output. Package microtype Info: Character protrusion enabled (level 2). @@ -1175,15 +1175,15 @@ (RS) ) -LaTeX Font Info: Try loading font information for OT1+lmr on input line 42. +LaTeX Font Info: Try loading font information for OT1+lmr on input line 44. (/usr/share/texlive/texmf-dist/tex/latex/lm/ot1lmr.fd File: ot1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern )<> -LaTeX Font Info: Try loading font information for OML+lmm on input line 42. +LaTeX Font Info: Try loading font information for OML+lmm on input line 44. (/usr/share/texlive/texmf-dist/tex/latex/lm/omllmm.fd File: omllmm.fd 2009/10/30 v1.6 Font defs for Latin Modern ) -LaTeX Font Info: Try loading font information for OMS+lmsy on input line 42. +LaTeX Font Info: Try loading font information for OMS+lmsy on input line 44. @@ -1191,5 +1191,5 @@ File: omslmsy.fd 2009/10/30 v1.6 Font defs for Latin Modern ) -LaTeX Font Info: Try loading font information for OMX+lmex on input line 42. +LaTeX Font Info: Try loading font information for OMX+lmex on input line 44. @@ -1198,10 +1198,10 @@ ) LaTeX Font Info: External font `lmex10' loaded for size -(Font) <12> on input line 42. +(Font) <12> on input line 44. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <8> on input line 42. +(Font) <8> on input line 44. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <6> on input line 42. -LaTeX Font Info: Try loading font information for U+msa on input line 42. +(Font) <6> on input line 44. +LaTeX Font Info: Try loading font information for U+msa on input line 44. (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd @@ -1211,5 +1211,5 @@ File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS) ) -LaTeX Font Info: Try loading font information for U+msb on input line 42. +LaTeX Font Info: Try loading font information for U+msb on input line 44. (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd @@ -1219,138 +1219,62 @@ File: mt-msb.cfg 2005/06/01 v1.0 microtype config. file: AMS symbols (b) (RS) ) +(./introduction.tex LaTeX Font Info: External font `lmex10' loaded for size -(Font) <10> on input line 73. +(Font) <10> on input line 15. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <7> on input line 73. +(Font) <7> on input line 15. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <5> on input line 73. - - -LaTeX Warning: Citation `GrumbergLong91assume_guarantee' on page 1 undefined on - input line 73. - - -LaTeX Warning: Citation `HQR98assume_guarantee' on page 1 undefined on input li -ne 73. - -[1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map} +(Font) <5> on input line 15. + [1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map} ] - -LaTeX Warning: Citation `GrafSaidi97abstract_construct' on page 2 undefined on -input line 77. - - -LaTeX Warning: Citation `clarke00cegar' on page 2 undefined on input line 80. - - -Overfull \hbox (1.1072pt too wide) in paragraph at lines 80--81 +Overfull \hbox (1.1072pt too wide) in paragraph at lines 22--23 []\T1/lmr/m/n/10 (-20) A few years later, an in-ter-est-ing abstraction-refinem ent [] - -LaTeX Warning: Citation `XieBrowne03composition_soft' on page 2 undefined on in -put line 82. - - -LaTeX Warning: Citation `PMT02compositional_MC' on page 2 undefined on input li -ne 85. - - -LaTeX Warning: Citation `SNBE06property_based' on page 2 undefined on input lin -e 89. - - -LaTeX Warning: Citation `microsoft04SLAM' on page 2 undefined on input line 92. - - - -LaTeX Warning: Citation `berkeley07BLAST' on page 2 undefined on input line 92. - - - -LaTeX Warning: Citation `Kroening_al07vcegar' on page 2 undefined on input line - 92. - - -LaTeX Warning: Citation `pwk2009-date' on page 2 undefined on input line 95. - - -LaTeX Warning: Citation `Kunz_al11ipc_abs' on page 2 undefined on input line 95 -. - - -LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 2 undefined on in -put line 98. - - -LaTeX Warning: Citation `bara08abs_composant' on page 2 undefined on input line - 98. - - -LaTeX Warning: Citation `clarke00cegar' on page 2 undefined on input line 104. - - -LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 2 undefined on in -put line 108. - -LaTeX Font Info: Try loading font information for TS1+lmr on input line 114. - -(/usr/share/texlive/texmf-dist/tex/latex/lm/ts1lmr.fd +) (./framework.tex [2] +LaTeX Font Info: Try loading font information for TS1+lmr on input line 23. + (/usr/share/texlive/texmf-dist/tex/latex/lm/ts1lmr.fd File: ts1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern -) [2] -LaTeX Font Info: Try loading font information for U+bbold on input line 144. - - (./Ubbold.fd) - +) + File: our_CEGAR_Loop_Enhanced_2S_PNG.png Graphic file (type png) Package pdftex.def Info: our_CEGAR_Loop_Enhanced_2S_PNG.png used on input line -182. +35. (pdftex.def) Requested size: 238.64096pt x 119.69688pt. - - -LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 3 undefined on in -put line 190. - - -LaTeX Warning: Citation `bara08abs_composant' on page 3 undefined on input line - 190. - - -LaTeX Warning: Citation `ucberkeley96vis' on page 3 undefined on input line 192 -. - -[3 <./our_CEGAR_Loop_Enhanced_2S_PNG.png>] -Underfull \hbox (badness 10000) in paragraph at lines 224--230 + [3 <./our_CEGAR_Loop_Enhanced_2S_PNG.png>] +LaTeX Font Info: Try loading font information for U+bbold on input line 86. + (./Ubbold.fd)) (./abstraction_refinement.tex +Underfull \hbox (badness 10000) in paragraph at lines 28--34 [] -Underfull \hbox (badness 10000) in paragraph at lines 224--230 +Underfull \hbox (badness 10000) in paragraph at lines 28--34 [] -Underfull \hbox (badness 10000) in paragraph at lines 224--230 +Underfull \hbox (badness 10000) in paragraph at lines 28--34 [] -Underfull \hbox (badness 10000) in paragraph at lines 238--241 +Underfull \hbox (badness 10000) in paragraph at lines 42--45 [] -Underfull \hbox (badness 10000) in paragraph at lines 238--241 +Underfull \hbox (badness 10000) in paragraph at lines 42--45 [] - -Overfull \hbox (0.81122pt too wide) in paragraph at lines 244--245 +[4] +Overfull \hbox (0.81122pt too wide) in paragraph at lines 48--49 []\T1/lmr/m/it/10 (-20) If $\OMS/lmsy/m/n/10 8\OML/lmm/m/it/10 k$ \T1/lmr/m/it/ 10 (-20) we have $[] \OMS/lmsy/m/n/10 ^^R \OML/lmm/m/it/10 V[]$ \T1/lmr/m/it/10 @@ -1360,5 +1284,5 @@ -Overfull \hbox (3.01537pt too wide) in paragraph at lines 261--264 +Overfull \hbox (3.01537pt too wide) in paragraph at lines 67--70 \OML/lmm/m/it/10 max\OT1/lmr/m/n/10 (-20) (\OML/lmm/m/it/10 depth\OT1/lmr/m/n/1 0 (-20) (\OML/lmm/m/it/10 Gv[]\OT1/lmr/m/n/10 (-20) )\OML/lmm/m/it/10 ; depth\O @@ -1368,32 +1292,32 @@ [] -[4] -Underfull \hbox (badness 10000) in paragraph at lines 296--297 + +Underfull \hbox (badness 10000) in paragraph at lines 103--104 [] - +[5] File: Dependency_graph_weight_PNG.png Graphic file (type png) -Package pdftex.def Info: Dependency_graph_weight_PNG.png used on input line 319 +Package pdftex.def Info: Dependency_graph_weight_PNG.png used on input line 126 . (pdftex.def) Requested size: 112.16878pt x 167.12395pt. -Underfull \hbox (badness 10000) in paragraph at lines 344--345 +Underfull \hbox (badness 10000) in paragraph at lines 151--152 [] -[5 <./Dependency_graph_weight_PNG.png>] -Overfull \hbox (11.93875pt too wide) in paragraph at lines 357--358 + +Overfull \hbox (11.93875pt too wide) in paragraph at lines 164--165 []$\OML/lmm/m/it/10 S[] \OT1/lmr/m/n/10 (-20) = \OMS/lmsy/m/n/10 f\OML/lmm/m/it /10 s[]; s[]; s[]; :::; s[]; s[]; :::; s[]\OMS/lmsy/m/n/10 g$ [] - + File: K_sigma_i_S_PNG.png Graphic file (type png) -Package pdftex.def Info: K_sigma_i_S_PNG.png used on input line 380. +Package pdftex.def Info: K_sigma_i_S_PNG.png used on input line 187. (pdftex.def) Requested size: 33.12366pt x 213.79822pt. @@ -1401,29 +1325,25 @@ LaTeX Warning: `!h' float specifier changed to `!ht'. - -Underfull \hbox (badness 10000) in paragraph at lines 420--421 +[6 <./Dependency_graph_weight_PNG.png> <./K_sigma_i_S_PNG.png>] +Underfull \hbox (badness 10000) in paragraph at lines 227--228 [] - -Underfull \hbox (badness 10000) in paragraph at lines 436--437 +) +Underfull \hbox (badness 10000) in paragraph at lines 75--76 [] -[6 <./K_sigma_i_S_PNG.png>] -No file FDL2012.bbl. -Package atveryend Info: Empty hook `BeforeClearDocument' on input line 462. -[7 +(./FDL2012.bbl [7]) +Package atveryend Info: Empty hook `BeforeClearDocument' on input line 101. + [8 ] -Package atveryend Info: Empty hook `AfterLastShipout' on input line 462. +Package atveryend Info: Empty hook `AfterLastShipout' on input line 101. (./FDL2012.aux) -Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 462. -Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 462. +Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 101. +Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 101. Package rerunfilecheck Info: File `FDL2012.out' has not changed. -(rerunfilecheck) Checksum: BA9407F3BD913632A2377663C2D85E5A;965. - - -LaTeX Warning: There were undefined references. +(rerunfilecheck) Checksum: 0706271851781CA86C089B6E9054600F;1151. @@ -1432,36 +1352,39 @@ ) Here is how much of TeX's memory you used: - 18495 strings out of 492508 - 332547 string characters out of 3115493 - 452738 words of memory out of 3000000 - 21197 multiletter control sequences out of 15000+200000 - 69857 words of font info for 127 fonts, out of 3000000 for 9000 + 18602 strings out of 492508 + 333954 string characters out of 3115493 + 452425 words of memory out of 3000000 + 21205 multiletter control sequences out of 15000+200000 + 80503 words of font info for 162 fonts, out of 3000000 for 9000 1648 hyphenation exceptions out of 8191 - 56i,10n,68p,951b,935s stack positions out of 5000i,500n,10000p,200000b,50000s -{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texl -ive/texmf-dist/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/share/texlive/texmf-dist/ -fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/ -lm-mathit.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ec.enc}{/usr + 56i,10n,68p,1177b,935s stack positions out of 5000i,500n,10000p,200000b,50000s +{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ec.enc}{/usr/share/texli +ve/texmf-dist/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texlive/texmf-dist/font +s/enc/dvips/lm/lm-mathsy.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/ +lm-rm.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-mathit.enc}{/usr /share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-mathex.enc}<./bbold10.pfb> -< -/usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmsy7.pfb> -Output written on FDL2012.pdf (7 pages, 353282 bytes). +s/type1/public/lm/lmbx9.pfb>< +/usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmmi10.pfb>< +/usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmr5.pfb> +Output written on FDL2012.pdf (8 pages, 445373 bytes). PDF statistics: - 223 PDF objects out of 1000 (max. 8388607) - 186 compressed objects within 2 object streams - 40 named destinations out of 1000 (max. 500000) - 21652 words of extra memory for PDF output out of 24883 (max. 10000000) - + 285 PDF objects out of 1000 (max. 8388607) + 243 compressed objects within 3 object streams + 58 named destinations out of 1000 (max. 500000) + 24228 words of extra memory for PDF output out of 24883 (max. 10000000) + Index: /papers/FDL2012/FDL2012.out =================================================================== --- /papers/FDL2012/FDL2012.out (revision 51) +++ /papers/FDL2012/FDL2012.out (revision 52) @@ -2,13 +2,15 @@ \BOOKMARK [2][-]{subsection.1.1}{ Related Works}{section.1}% 2 \BOOKMARK [1][-]{section.2}{ Our Framework}{}% 3 -\BOOKMARK [2][-]{subsection.2.1}{ AKS generation from CTL Properties}{section.2}% 4 -\BOOKMARK [2][-]{subsection.2.2}{ CEGAR Loop}{section.2}% 5 -\BOOKMARK [1][-]{section.3}{ Abstraction Generation and Refinement}{}% 6 -\BOOKMARK [2][-]{subsection.3.1}{ Generalities}{section.3}% 7 -\BOOKMARK [3][-]{subsubsection.3.1.1}{ Refinement}{subsection.3.1}% 8 -\BOOKMARK [3][-]{subsubsection.3.1.2}{ The Counterexample}{subsection.3.1}% 9 -\BOOKMARK [2][-]{subsection.3.2}{ Pre-processing and pertinency ordering of properties}{section.3}% 10 -\BOOKMARK [2][-]{subsection.3.3}{ Initial abstraction generation}{section.3}% 11 -\BOOKMARK [2][-]{subsection.3.4}{ Abstraction refinement}{section.3}% 12 -\BOOKMARK [1][-]{section.4}{ Experimental results}{}% 13 -\BOOKMARK [1][-]{section.5}{ Conclusion and Future Works}{}% 14 +\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 Index: /papers/FDL2012/FDL2012.tex =================================================================== --- /papers/FDL2012/FDL2012.tex (revision 51) +++ /papers/FDL2012/FDL2012.tex (revision 52) @@ -26,4 +26,6 @@ \newtheorem{definition}{Definition} \newtheorem{property}{Property} +\newcommand{\TODO}[1] {\textcolor{red}{TODO : #1}} +\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}} @@ -57,395 +59,13 @@ \section{Introduction} -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. Generally failures on these systems are unacceptable and have to be avoided. - - -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, indeed, guarantees a certain level of quality in terms of safety and reliabilty while reducing financial risk. - - -The main challenge in model checking is dealing with the state space combinatorial explosion phenomenon. Systems with many components that can interact with each other or systems with data structure that can assume many different values will increase the number of state transition possibilities at a particular instance. In such cases, the number of global states will grow exponentially in function of the complexity of the system and unfortunately may surpasses our computation capacity. - - -In this research we would like to contribute in the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. - - -\subsection{Related Works} - -We are inspired by the compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, we show that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If that's the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. 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 Herzinger and al. presented their successful implementations and case study regarding this approach. - - - -A strategy to overcome the state explosion problem is by abstraction. A method for the construction of an abstract state graph of an arbitrary system automatically was 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. - - -A few years later, 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. - -There have been works related to this PhD research domain in the recent years, for example, Xie and Browne have proposed a method for software verification based on composistion 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. - - -In another research, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL \cite{PMT02compositional_MC}. 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. - - - -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. - - -Several tools using counterexample-guided abstraction refinement technique 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}. - - -Recently, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification \cite{pwk2009-date}. The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In 2011, the electronic design automation group of University of Kaiserslautern suggested a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique \cite{Kunz_al11ipc_abs}. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems. - - -Nevertheless, LIP6 has proposed a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component verifies in 2007 \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}. These work will be the base of the techniques in this paper. - +\input{introduction} \section{Our Framework} -The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. We take into account the structure of the system as a set of synchronous components, each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}. - -\subsection{Overall Description of our methodology} -In CEGAR loop methodology, in order to verify a global property $\Phi$ on a concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is generated and tested in the model-checker. As the abstract model is an upper-approximation of the concrete model and we have restrained our verification to ACTL properties only, if $\Phi$ hold on the the abstract model then we are certain that it holds in the concrete model as well. However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, $\sigma$ given by the model-checker has been analyzed. -%\bigskip -\begin{definition} -The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas are CTL formulas with only universal path quantifiers: AX, AF, AG and AU. -\end{definition} - -TODO : FAUT-IL METTRE CETTE DEFINITION DE $\Phi$ ?? - -\begin{definition} -Given $\widehat{M} = (\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ an abstract model of a concrete model, $M$ and $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows: - -\begin{itemize} -\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed } -\item{$\widehat{M} \nvDash \Phi$ and $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. } -\end{itemize} -\end{definition} - -%\bigskip -We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}. - -\begin{figure}[h!] -% \centering -% \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG} -% \hspace*{-5mm} - \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG} - \caption{\label{cegar} Verification Process } -\end{figure} - -As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\varphi$. The generation of an abstract model in the form of AKS from CTL formulas, based on the works of Braunstein \cite{braunstein07ctl_abstraction}, has been successfully implemented by Bara \cite{bara08abs_composant}. - -In the case where model-checking failed, the counterexample given by the model-checker \cite{ucberkeley96vis} has to be analysed. We use a SATSolver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase. - -\subsection{Definition of the abstraction of a component and of the complete system} - -The abstraction of a component is represented by an Abstract Kripke Structure (AKS for short), derived from a subset of the CTL properties the component satisfies. Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property $\varphi$, simulates all execution trees whose initial state satisfies $\varphi$. In AKS($\varphi$), states are tagged with the truth values of $\varphi$'s atomic propositions, among four truth values : inconsistent, false, true and unknown (or undefined). States with inconsistent truth values are not represented since they refer to non possible assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. - - -%Assume that we have an abstract Kripke structure (AKS) representing the abstract model $\widehat{M}$ of the concrete model of the system M with regard to the property to be verified, $\Phi$. The abstraction method is based on the work described in \cite{ braunstein07ctl_abstraction}. -The AKS associated with a CTL property $\varphi$ whose set of atomic propositions is $AP$ is a 6-tuple, \\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows: - -\begin{definition} -An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of : - -\begin{itemize} -\item { $\widehat{AP}$ : a finite set of atomic propositions} -\item { $\widehat{S}$ : a finite set of states} -\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states} -\item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:} - \begin{itemize} - \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s } - \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s} - \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s} - \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{inconsistent} in} s} - \end{itemize} -\item { $\widehat{R} \subseteq \widehat{S} \times \widehat{S}$ : a transition relation where $ \forall s \in \widehat{S}, \exists s' \in \widehat{S}$ such that $(s,s') \in \widehat{R}$ } -\item { $\widehat{F}$ : a set of fairness constraints TODO : PRECISER LEUR REPRESENTATION ET LES ARBRES ACCEPTES} -\end{itemize} -\end{definition} -%\bigskip - - -As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property. -%\bigskip - -\begin{definition} -Let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$: - -\begin{itemize} -\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $} -\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $} -\item{$ V_{\widehat{C}_j} \subseteq V_{C_j}$ (with $V_{\widehat{C}_j}$ and $V_{C_j}$ are variables of $\widehat{C}_j$ and $C_j$ respectively.) TODO : LES V ICI NE SONT-ELLES PAS L'UNION DES AP DES $\varphi_{C_j^k}$ ???????} -\end{itemize} - -\hspace*{3mm}with :\\ -\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\ -\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component - -\end{definition} -%\bigskip - - - - -\subsection{Characterization of AKS} -TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ?? - -1. Ordering of AKS - -Def : Concrete and abstract variables in AKS - -Def : Concretization of an abstract variable - -Def (dual) : Abstraction of a concrete variable - -Prop : Let A1 and A2 two AKS such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2. - -A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ??? - -2. Negation of states in an AKS - -a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component. - -b) The negation of an configuration may be represented by a set of abstract configurations - -c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS - - +\input{framework} \section{Abstraction Generation and Refinement} -\subsection{Generalities} - -We suppose that our concrete model is a composition of several components and each component has been previously verified. Hence, we have a set of verified properties for each component of the concrete model. The main idea of this technique is that we would like to make use of these properties to generate a better abstract model. Properties of the components that appear to be related to the global property to be verified, $\phi$ are selected to generate the abstract model $\widehat{M}_i$. This method is particularly interesting as it gives a possibility to converge quicker to an abstract model that is sufficient to satisfy the global property $\phi$. - -\subsubsection{Refinement} -The model-checker provides a counterexample when a property failed during model-checking. The counterexample can be \emph{spurious} which means that the path is impossible in the concrete model $M$ or the counterexample is real which implies that $M \nvDash \phi $.When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined. In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ has to be conservative and respects the properties below: - -%\medskip - -\begin{property} -All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. -\end{property} -%\bigskip -\begin{property} -$\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$. -\end{property} - -%\bigskip -%\newpage - -\subsubsection{The Counterexample} - - -The counterexample at a refinement step $i$, $\sigma_i$ is a path in the abstract model $\widehat{M}_i$ which dissatisfy $\phi$. In the counterexample given by the model-checker, the variables' value in each states are boolean. -%\medskip - -\begin{definition} -\textbf{\emph{The counterexample $\sigma_i$ :}} \\ -\\ -Let $\widehat{M}_i =(\widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, \widehat{L}_i, \widehat{R}_i, \widehat{F}_i)$ and let the length of the counterexample, $|\sigma_i| = n$: $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k},$ $s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1], ~s_{\bar{a}i,k} \subseteq s_{i,k} \in \widehat{S}_i, ~s_{\bar{a}i,0} \subseteq s_{i,0} \in \widehat{S}_{0i}$ and $(s_{i,k}, s_{i,k+1}) \in \widehat{R}_i$. \\ -Furthermore, for each state in $\sigma_i$ we have $s_{\bar{a}i,k} = \langle v_{\bar{a}i,k}^1, v_{\bar{a}i,k}^2, ... , v_{\bar{a}i,k}^p, ... , v_{\bar{a}i,k}^q \rangle$, $\forall p \in [1,q], ~v_{\bar{a}i,k}^p \in \widehat{V}_{i,k}$ with $\widehat{V}_{i,k} \in 2^q$. \\ -\\ -(\emph{\underline{Note} :} In AKS $\widehat{M}_i$, the variables are actually 3-valued : $\widehat{V}_{i,k} \in 3^q$. We differenciate the 3-valued variables $v_{i,k}^p$ from boolean variables with $v_{\bar{a}i,k}^p$.)\\ - -%\medskip - -\end{definition} - -%\bigskip - -\begin{definition} -\textbf{\emph{Spurious counterexample :}} \\ -\\ -Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... , v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\ - -\smallskip - -If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}. - -\end{definition} - - - -\subsection{Pre-processing and pertinency ordering of properties} - -Before generating an abstract model to verify a global property $\phi$, the verified properties of all the components in the concrete model are ordered according to their pertinency in comparison to a global property $\phi$. In order to do so, the variable dependency of the variables present in global property $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}. - -%\bigskip - -The ordering of the properties will be based on the variable dependency graph. The variables in the model are weighted according to their dependency level \emph{vis-à-vis} primary variables and the properties will be weighted according to the sum of the weights of the variables present in it. We have decided to allocate a supplementary weight for variables which are present at the interface of a component whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. Here is how we proceed: - - -\begin{enumerate} - -\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\ -Each primary variable will be examined and their dependency graph is elobarated. The maximum graph depth among the primary variable dependency graphs will be identified and used to calibrate the weight of all the variables related to the global property. -Given the primary variables of $\phi$, $V_{\phi} = \langle v_{\phi_0}, v_{\phi_1}, ... , v_{\phi_k}, ... , v_{\phi_n} \rangle$ and $G{\_v_{\phi_k}}$ the dependency graph of primary variable $v_{\phi_k}$, we have the maximum graph depth $max_{d} = max(depth(Gv_{\phi_0}), depth(Gv_{\phi_1}), ... , depth(Gv_{\phi_k}), ... ,$\\$ depth(Gv_{\phi_n})) $. - -} - -\item {\emph{Weight allocation for each variables} \\ -Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows: -\begin{itemize} -\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.} - \\ \hspace*{20mm} $Wv_{max_d} = p$ -\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.} -\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$ -\item{...} -\item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.} - \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$ -\item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.} - \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$ -\end{itemize} - -We can see here that the primary variables are given a considerable ponderation due to their pertinency \emph{vis-à-vis} global property. Furthermore, we will allocate a supplementary weight of $3Wv_{1}$ to variables at the interface of a component as they are the variables which assure the connection between the components if there is at least one variable in the dependency graph established in the previous step in the property. All other non-related variables have a weight equals to $0$. -} - - -\item {\emph{Ordering of the properties} \\ -Properties will be ordered according to the sum of the weight of the variables in it. Therefore, given a property $\varphi_i$ which contains $n+1$ variables, $V_{\varphi_i} = \langle v_{\varphi_{i0}}, v_{\varphi_{i1}}, ... , v_{\varphi_{ik}}, ... , v_{\varphi_{in}} \rangle$, the weight of $\varphi_i$ , $W_{\varphi_i} = \sum_{k=0}^{n} Wv_{\varphi_{ik}}$ . -After this stage, we will check all the properties with weight $>0$ and allocate a supplementary weight of $3Wv_{1}$ for every variable at the interface present in the propery. After this process, the final weight of a property is obtained and the properties will be ordered in a list with the weight decreasing (the heaviest first). We will refer to the ordered list of properties related to the global property $\phi$ as $L_\phi$. - - -} - -\end{enumerate} - -%\bigskip - -\emph{\underline{Example:}} \\ - -For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where: -\begin{itemize} -\item{$p$ is dependent of $a$ and $b$} -\item{$b$ is dependent of $c$} -\item{$q$ is dependent of $x$} -\item{$r$ is independent} -\end{itemize} - -Example with unit weight= 50. -The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\ -The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\ -The tertiary level variable $c$ is weighted $50$. \\ -The weight of a non-related variable is $0$. - -So each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property. - -\bigskip -\begin{figure}[h!] - \centering -% \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG} -% \hspace*{-15mm} - \includegraphics{Dependency_graph_weight_PNG} - \caption{\label{DepGraphWeight} Example of weighting} -\end{figure} - -%Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 
 - - - -After this pre-processing phase, we will have a list of properties $L_\phi $ ordered according to their pertinency in comparison to the global property. - - - - -\subsection{Initial abstraction generation} - -In the initial abstraction generation, all primary variables have to be represented. Therefore the first element(s) in the list where the primary variables are present will be used to generate the initial abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the global property $\phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process. - - - -\subsection{Abstraction refinement} - -The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps: - -\begin{enumerate} - -\item {\emph{\underline{Step 1:}} \\ - -As we would like to ensure the elimination of the counterexample previously found, we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. In order to reach this obective, a Kripke Structure of the counterexample $\sigma_i$, $K(\sigma_i)$ is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies the global property $\phi$. - -\bigskip - -\begin{definition} -\textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\ -Let a counterexample of length $n$, $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1},\\ s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1]$, we have \\ -$K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of : - -\begin{itemize} -\item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ } -\item { $S_{\sigma_i} = \{s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\}$} -\item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$} -\item { $L_{\sigma_i}$ : $S_{\sigma_i} \rightarrow 2^{AP_{\sigma_i}}$ : a labeling function which labels each state with the set of atomic propositions true in that state. } -\item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ } -\end{itemize} -\end{definition} - -%\bigskip -All the properties available are then model-checked on $K(\sigma_i)$. - -If: -\begin{itemize} -\item {\textbf{$K(\sigma_i) \vDash \varphi \Rightarrow \varphi $ will not eliminate $\sigma_i$}} -\item {\textbf{$K(\sigma_i) \nvDash \varphi \Rightarrow \varphi $ will eliminate $\sigma_i$}} -\end{itemize} - -%\bigskip - - -\begin{figure}[h!] - \centering -% \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG} -% \hspace*{-15mm} - \includegraphics{K_sigma_i_S_PNG} - \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} -\end{figure} - -%Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 
 - -%\bigskip - - -\begin{figure}[h!] - \centering - -\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm, - thick] - \tikzstyle{every state}=[fill=none,draw=blue,text=black] - - \node[initial,state] (A) {$s_{\bar{a}i,0}$}; - \node[state] (B) [below of=A] {$s_{\bar{a}i,1}$}; - - \node[state] (C) [below of=B] {$s_{\bar{a}i,k}$}; - - \node[state] (D) [below of=C] {$s_{\bar{a}i,n-1}$}; - \node[state] (E) [below of=D] {$s_{\bar{a}i,n}$}; - - \path (A) edge node {} (B) - (B) edge node {} (C) - (C) edge node {} (D) - (D) edge node {} (E); - -\end{tikzpicture} - - \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} -\end{figure} - - -Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$. - -} -%\bigskip - -\item {\emph{\underline{Step 2:}} \\ - -The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. -%\bigskip - -} -\end{enumerate} - -$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction. - - +\input{abstraction_refinement} Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 52) +++ /papers/FDL2012/abstraction_refinement.tex (revision 52) @@ -0,0 +1,237 @@ +\subsection{Generalities} + +We suppose that our concrete model is a composition of several components and each component has been previously verified. Hence, we have a set of verified properties for each component of the concrete model. The main idea of this technique is that we would like to make use of these properties to generate a better abstract model. Properties of the components that appear to be related to the global property to be verified, $\phi$ are selected to generate the abstract model $\widehat{M}_i$. This method is particularly interesting as it gives a possibility to converge quicker to an abstract model that is sufficient to satisfy the global property $\phi$. + +\subsubsection{Refinement} +The model-checker provides a counterexample when a property failed during model-checking. The counterexample can be \emph{spurious} which means that the path is impossible in the concrete model $M$ or the counterexample is real which implies that $M \nvDash \phi $.When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined. In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ has to be conservative and respects the properties below: + +%\medskip + +\begin{property} +All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$. +\end{property} +%\bigskip +\begin{property} +$\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$. +\end{property} + +%\bigskip +%\newpage + +\subsubsection{The Counterexample} + + +The counterexample at a refinement step $i$, $\sigma_i$ is a path in the abstract model $\widehat{M}_i$ which dissatisfy $\phi$. In the counterexample given by the model-checker, the variables' value in each states are boolean. +%\medskip + +\begin{definition} +\textbf{\emph{The counterexample $\sigma_i$ :}} \\ +\\ +Let $\widehat{M}_i =(\widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, \widehat{L}_i, \widehat{R}_i, \widehat{F}_i)$ and let the length of the counterexample, $|\sigma_i| = n$: $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k},$ $s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1], ~s_{\bar{a}i,k} \subseteq s_{i,k} \in \widehat{S}_i, ~s_{\bar{a}i,0} \subseteq s_{i,0} \in \widehat{S}_{0i}$ and $(s_{i,k}, s_{i,k+1}) \in \widehat{R}_i$. \\ +Furthermore, for each state in $\sigma_i$ we have $s_{\bar{a}i,k} = \langle v_{\bar{a}i,k}^1, v_{\bar{a}i,k}^2, ... , v_{\bar{a}i,k}^p, ... , v_{\bar{a}i,k}^q \rangle$, $\forall p \in [1,q], ~v_{\bar{a}i,k}^p \in \widehat{V}_{i,k}$ with $\widehat{V}_{i,k} \in 2^q$. \\ +\\ +(\emph{\underline{Note} :} In AKS $\widehat{M}_i$, the variables are actually 3-valued : $\widehat{V}_{i,k} \in 3^q$. We differenciate the 3-valued variables $v_{i,k}^p$ from boolean variables with $v_{\bar{a}i,k}^p$.)\\ + +%\medskip + +\end{definition} + +%\bigskip + +\begin{definition} +\textbf{\emph{Spurious counterexample :}} \\ +\\ +Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... , v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\ + +\smallskip + +If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}. + +\end{definition} + + + +\subsection{Pre-processing and pertinency ordering of properties} + +Before generating an abstract model to verify a global property $\phi$, the verified properties of all the components in the concrete model are ordered according to their pertinency in comparison to a global property $\phi$. In order to do so, the variable dependency of the variables present in global property $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}. + +%\bigskip + +The ordering of the properties will be based on the variable dependency graph. +The variables in the model are weighted according to their dependency level +\emph{vis-à-vis} primary variables and the properties will be weighted according to the sum of the weights of the variables present in it. We have decided to allocate a supplementary weight for variables which are present at the interface of a component whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. Here is how we proceed: + + +\begin{enumerate} + +\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\ +Each primary variable will be examined and their dependency graph is elobarated. The maximum graph depth among the primary variable dependency graphs will be identified and used to calibrate the weight of all the variables related to the global property. +Given the primary variables of $\phi$, $V_{\phi} = \langle v_{\phi_0}, v_{\phi_1}, ... , v_{\phi_k}, ... , v_{\phi_n} \rangle$ and $G{\_v_{\phi_k}}$ the dependency graph of primary variable $v_{\phi_k}$, we have the maximum graph depth $max_{d} = max(depth(Gv_{\phi_0}), depth(Gv_{\phi_1}), ... , depth(Gv_{\phi_k}), ... ,$\\$ depth(Gv_{\phi_n})) $. + +} + +\item {\emph{Weight allocation for each variables} \\ +Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows: +\begin{itemize} +\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.} + \\ \hspace*{20mm} $Wv_{max_d} = p$ +\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.} +\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$ +\item{...} +\item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.} + \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$ +\item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.} + \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$ +\end{itemize} + +We can see here that the primary variables are given a considerable +ponderation due to their pertinency \emph{vis-à-vis} global property. Furthermore, we will allocate a supplementary weight of $3Wv_{1}$ to variables at the interface of a component as they are the variables which assure the connection between the components if there is at least one variable in the dependency graph established in the previous step in the property. All other non-related variables have a weight equals to $0$. +} + + +\item {\emph{Ordering of the properties} \\ +Properties will be ordered according to the sum of the weight of the variables in it. Therefore, given a property $\varphi_i$ which contains $n+1$ variables, $V_{\varphi_i} = \langle v_{\varphi_{i0}}, v_{\varphi_{i1}}, ... , v_{\varphi_{ik}}, ... , v_{\varphi_{in}} \rangle$, the weight of $\varphi_i$ , $W_{\varphi_i} = \sum_{k=0}^{n} Wv_{\varphi_{ik}}$ . +After this stage, we will check all the properties with weight $>0$ and allocate a supplementary weight of $3Wv_{1}$ for every variable at the interface present in the propery. After this process, the final weight of a property is obtained and the properties will be ordered in a list with the weight decreasing (the heaviest first). We will refer to the ordered list of properties related to the global property $\phi$ as $L_\phi$. + + +} + +\end{enumerate} + +%\bigskip + +\emph{\underline{Example:}} \\ + +For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where: +\begin{itemize} +\item{$p$ is dependent of $a$ and $b$} +\item{$b$ is dependent of $c$} +\item{$q$ is dependent of $x$} +\item{$r$ is independent} +\end{itemize} + +Example with unit weight= 50. +The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\ +The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\ +The tertiary level variable $c$ is weighted $50$. \\ +The weight of a non-related variable is $0$. + +So each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property. + +\bigskip +\begin{figure}[h!] + \centering +% \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG} +% \hspace*{-15mm} + \includegraphics{Dependency_graph_weight_PNG} + \caption{\label{DepGraphWeight} Example of weighting} +\end{figure} + +%Dans la figure~\ref{étiquette} page~\pageref{étiquette},   + + + +After this pre-processing phase, we will have a list of properties $L_\phi $ ordered according to their pertinency in comparison to the global property. + + + + +\subsection{Initial abstraction generation} + +In the initial abstraction generation, all primary variables have to be represented. Therefore the first element(s) in the list where the primary variables are present will be used to generate the initial abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the global property $\phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process. + + + +\subsection{Abstraction refinement} + +The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps: + +\begin{enumerate} + +\item {\emph{\underline{Step 1:}} \\ + +As we would like to ensure the elimination of the counterexample previously found, we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. In order to reach this obective, a Kripke Structure of the counterexample $\sigma_i$, $K(\sigma_i)$ is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies the global property $\phi$. + +\bigskip + +\begin{definition} +\textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\ +Let a counterexample of length $n$, $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1},\\ s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1]$, we have \\ +$K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of : + +\begin{itemize} +\item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ } +\item { $S_{\sigma_i} = \{s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\}$} +\item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$} +\item { $L_{\sigma_i}$ : $S_{\sigma_i} \rightarrow 2^{AP_{\sigma_i}}$ : a labeling function which labels each state with the set of atomic propositions true in that state. } +\item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ } +\end{itemize} +\end{definition} + +%\bigskip +All the properties available are then model-checked on $K(\sigma_i)$. + +If: +\begin{itemize} +\item {\textbf{$K(\sigma_i) \vDash \varphi \Rightarrow \varphi $ will not eliminate $\sigma_i$}} +\item {\textbf{$K(\sigma_i) \nvDash \varphi \Rightarrow \varphi $ will eliminate $\sigma_i$}} +\end{itemize} + +%\bigskip + + +\begin{figure}[h!] + \centering +% \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG} +% \hspace*{-15mm} + \includegraphics{K_sigma_i_S_PNG} + \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} +\end{figure} + +%Dans la figure~\ref{étiquette} page~\pageref{étiquette},   + +%\bigskip + + +\begin{figure}[h!] + \centering + +\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm, + thick] + \tikzstyle{every state}=[fill=none,draw=blue,text=black] + + \node[initial,state] (A) {$s_{\bar{a}i,0}$}; + \node[state] (B) [below of=A] {$s_{\bar{a}i,1}$}; + + \node[state] (C) [below of=B] {$s_{\bar{a}i,k}$}; + + \node[state] (D) [below of=C] {$s_{\bar{a}i,n-1}$}; + \node[state] (E) [below of=D] {$s_{\bar{a}i,n}$}; + + \path (A) edge node {} (B) + (B) edge node {} (C) + (C) edge node {} (D) + (D) edge node {} (E); + +\end{tikzpicture} + + \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} +\end{figure} + + +Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$. + +} +%\bigskip + +\item {\emph{\underline{Step 2:}} \\ + +The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. +%\bigskip + +} +\end{enumerate} + +$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction. + + Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 52) +++ /papers/FDL2012/framework.tex (revision 52) @@ -0,0 +1,117 @@ +The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. We take into account the structure of the system as a set of synchronous components, each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}. + +\subsection{Overall Description of our methodology} +In CEGAR loop methodology, in order to verify a global property $\Phi$ on a +concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is +generated and tested in the model-checker. As the abstract model is an +upper-approximation of the concrete model and we have restrained our +verification to ACTL properties only, if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well. +However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, +$\sigma$ given by the model-checker has been analyzed. \remark{Cecile}{cite +Grumberg ovver-approx et ACTL poperties} +%\bigskip +%\begin{definition} +%The property to be verified, $\Phi$ is an ACTL formula. ACTL formulas +%are CTL formulas with only universal path quantifiers: AX, AF, AG and AU. +%\end{definition} +\remark{Cecile}{remettre la défintion du modÚle concret} +\begin{definition} +Given $\widehat{M} = (\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ an abstract model of a concrete model, $M$ and $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows: + +\begin{itemize} +\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed } +\item{$\widehat{M} \nvDash \Phi$ and $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. } +\end{itemize} +\end{definition} + +%\bigskip +We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}. + +\begin{figure}[h!] +% \centering +% \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG} +% \hspace*{-5mm} + \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG} + \caption{\label{cegar} Verification Process } +\end{figure} + +As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\varphi$. The generation of an abstract model in the form of AKS from CTL formulas, based on the works of Braunstein \cite{braunstein07ctl_abstraction}, has been successfully implemented by Bara \cite{bara08abs_composant}. + +In the case where model-checking failed, the counterexample given by the model-checker \cite{ucberkeley96vis} has to be analysed. We use a SATSolver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase. + +\subsection{Definition of the abstraction of a component and of the complete system} + +The abstraction of a component is represented by an Abstract Kripke Structure (AKS for short), derived from a subset of the CTL properties the component satisfies. Roughly speaking, AKS($\varphi$), the AKS derived from a CTL property $\varphi$, simulates all execution trees whose initial state satisfies $\varphi$. In AKS($\varphi$), states are tagged with the truth values of $\varphi$'s atomic propositions, among four truth values : inconsistent, false, true and unknown (or undefined). States with inconsistent truth values are not represented since they refer to non possible assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. + + +%Assume that we have an abstract Kripke structure (AKS) representing the abstract model $\widehat{M}$ of the concrete model of the system M with regard to the property to be verified, $\Phi$. The abstraction method is based on the work described in \cite{ braunstein07ctl_abstraction}. +The AKS associated with a CTL property $\varphi$ whose set of atomic propositions is $AP$ is a 6-tuple, \\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows: + +\begin{definition} +An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of : + +\begin{itemize} +\item { $\widehat{AP}$ : a finite set of atomic propositions} +\item { $\widehat{S}$ : a finite set of states} +\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states} +\item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:} + \begin{itemize} + \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s } + \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s} + \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s} + \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{inconsistent} in} s} + \end{itemize} +\item { $\widehat{R} \subseteq \widehat{S} \times \widehat{S}$ : a transition relation where $ \forall s \in \widehat{S}, \exists s' \in \widehat{S}$ such that $(s,s') \in \widehat{R}$ } +\item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi +acceptance condition)} +\end{itemize} +\end{definition} +%\bigskip + + +As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property. +%\bigskip + +\begin{definition} +Let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$: + +\begin{itemize} +\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $} +\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $} +\item{$ V_{\widehat{C}_j} \subseteq V_{C_j}$ (with $V_{\widehat{C}_j}$ and $V_{C_j}$ are variables of $\widehat{C}_j$ and $C_j$ respectively.) TODO : LES V ICI NE SONT-ELLES PAS L'UNION DES AP DES $\varphi_{C_j^k}$ ???????} +\end{itemize} + +\hspace*{3mm}with :\\ +\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\ +\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component + +\end{definition} +%\bigskip + + + + +\subsection{Characterization of AKS} +TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ?? + +1. Ordering of AKS + +Def : Concrete and abstract variables in AKS + +Def : Concretization of an abstract variable + +Def (dual) : Abstraction of a concrete variable + +Prop : Let A1 and A2 two AKS such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2. + +A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ??? + +2. Negation of states in an AKS + +a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component. + +b) The negation of an configuration may be represented by a set of abstract configurations + +c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS + + Index: /papers/FDL2012/introduction.tex =================================================================== --- /papers/FDL2012/introduction.tex (revision 52) +++ /papers/FDL2012/introduction.tex (revision 52) @@ -0,0 +1,42 @@ +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. Generally failures on these systems are unacceptable and have to be avoided. + + +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, indeed, guarantees a certain level of quality in terms of safety and reliabilty while reducing financial risk. + + +The main challenge in model checking is dealing with the state space combinatorial explosion phenomenon. Systems with many components that can interact with each other or systems with data structure that can assume many different values will increase the number of state transition possibilities at a particular instance. In such cases, the number of global states will grow exponentially in function of the complexity of the system and unfortunately may surpasses our computation capacity. + + +In this research we would like to contribute in the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. + + +\subsection{Related Works} + +We are inspired by the compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, we show that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If that's the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. 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 Herzinger and al. presented their successful implementations and case study regarding this approach. + + + +A strategy to overcome the state explosion problem is by abstraction. A method for the construction of an abstract state graph of an arbitrary system automatically was 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. + + +A few years later, 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. + +There have been works related to this PhD research domain in the recent years, for example, Xie and Browne have proposed a method for software verification based on composistion 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. + + +In another research, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL \cite{PMT02compositional_MC}. 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. + + + +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. + + +Several tools using counterexample-guided abstraction refinement technique 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}. + + +Recently, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification \cite{pwk2009-date}. The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In 2011, the electronic design automation group of University of Kaiserslautern suggested a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique \cite{Kunz_al11ipc_abs}. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems. + + +Nevertheless, LIP6 has proposed a method to build abstractions of components into AKS (Abstract Kripke Structure), based on the set of the properties (CTL) each component verifies in 2007 \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}. These work will be the base of the techniques in this paper. + +