Changeset 52


Ignore:
Timestamp:
Mar 7, 2012, 5:10:31 PM (13 years ago)
Author:
cecile
Message:

Decomposition de papier en fichier

Location:
papers/FDL2012
Files:
3 added
4 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/FDL2012.aux

    r48 r52  
    4242\citation{braunstein07ctl_abstraction}
    4343\@writefile{toc}{\contentsline {section}{\numberline {2} Our Framework}{2}{section.2}}
    44 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1} AKS generation from CTL Properties}{2}{subsection.2.1}}
     44\@writefile{toc}{\contentsline {subsection}{\numberline {2.1} Overall Description of our methodology}{2}{subsection.2.1}}
    4545\citation{braunstein07ctl_abstraction}
    4646\citation{bara08abs_composant}
    4747\citation{ucberkeley96vis}
    48 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2} CEGAR Loop}{3}{subsection.2.2}}
    4948\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces  Verification Process }}{3}{figure.1}}
    5049\newlabel{cegar}{{1}{3}{Verification Process\relax }{figure.1}{}}
    51 \@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{3}{section.3}}
    52 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{3}{subsection.3.1}}
     50\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} Definition of the abstraction of a component and of the complete system}{3}{subsection.2.2}}
     51\@writefile{toc}{\contentsline {subsection}{\numberline {2.3} Characterization of AKS}{4}{subsection.2.3}}
     52\@writefile{toc}{\contentsline {section}{\numberline {3} Abstraction Generation and Refinement}{4}{section.3}}
     53\@writefile{toc}{\contentsline {subsection}{\numberline {3.1} Generalities}{4}{subsection.3.1}}
    5354\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1} Refinement}{4}{subsubsection.3.1.1}}
    5455\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.2} The Counterexample}{4}{subsubsection.3.1.2}}
    55 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{4}{subsection.3.2}}
    56 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Example of weighting}}{5}{figure.2}}
    57 \newlabel{DepGraphWeight}{{2}{5}{Example of weighting\relax }{figure.2}{}}
    58 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{5}{subsection.3.3}}
    59 \@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{5}{subsection.3.4}}
     56\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Pre-processing and pertinency ordering of properties}{5}{subsection.3.2}}
     57\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Example of weighting}}{6}{figure.2}}
     58\newlabel{DepGraphWeight}{{2}{6}{Example of weighting\relax }{figure.2}{}}
     59\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Initial abstraction generation}{6}{subsection.3.3}}
     60\@writefile{toc}{\contentsline {subsection}{\numberline {3.4} Abstraction refinement}{6}{subsection.3.4}}
    6061\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.3}}
    6162\newlabel{AKSNegCex}{{3}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.3}{}}
    62 \@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{6}{figure.4}}
    63 \newlabel{AKSNegCex}{{4}{6}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}}
    64 \@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{6}{section.4}}
    65 \@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{6}{section.5}}
    6663\bibstyle{IEEEbib}
    6764\bibdata{myBib}
     65\bibcite{GrumbergLong91assume_guarantee}{1}
     66\bibcite{HQR98assume_guarantee}{2}
     67\bibcite{GrafSaidi97abstract_construct}{3}
     68\bibcite{clarke00cegar}{4}
     69\bibcite{XieBrowne03composition_soft}{5}
     70\bibcite{PMT02compositional_MC}{6}
     71\bibcite{SNBE06property_based}{7}
     72\bibcite{microsoft04SLAM}{8}
     73\bibcite{berkeley07BLAST}{9}
     74\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$}}{7}{figure.4}}
     75\newlabel{AKSNegCex}{{4}{7}{Kripke Structure of counterexample $\sigma _i$, $K(\sigma _i)$\relax }{figure.4}{}}
     76\@writefile{toc}{\contentsline {section}{\numberline {4} Experimental results}{7}{section.4}}
     77\@writefile{toc}{\contentsline {section}{\numberline {5} Conclusion and Future Works}{7}{section.5}}
     78\@writefile{toc}{\contentsline {section}{\numberline {6} References}{7}{section.6}}
     79\bibcite{Kroening_al07vcegar}{10}
     80\bibcite{pwk2009-date}{11}
     81\bibcite{Kunz_al11ipc_abs}{12}
     82\bibcite{braunstein07ctl_abstraction}{13}
     83\bibcite{bara08abs_composant}{14}
     84\bibcite{ucberkeley96vis}{15}
  • papers/FDL2012/FDL2012.log

    r49 r52  
    1 This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2011) (format=pdflatex 2012.2.19)  5 MAR 2012 17:30
     1This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2011) (format=pdflatex 2012.2.19)  7 MAR 2012 16:44
    22entering extended mode
    33 restricted \write18 enabled.
     
    10751075\openout1 = `FDL2012.aux'.
    10761076
    1077 LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 38.
    1078 LaTeX Font Info:    ... okay on input line 38.
    1079 LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 38.
    1080 LaTeX Font Info:    ... okay on input line 38.
    1081 LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 38.
    1082 LaTeX Font Info:    ... okay on input line 38.
    1083 LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 38.
    1084 LaTeX Font Info:    ... okay on input line 38.
    1085 LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 38.
    1086 LaTeX Font Info:    ... okay on input line 38.
    1087 LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 38.
    1088 LaTeX Font Info:    ... okay on input line 38.
    1089 LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 38.
    1090 LaTeX Font Info:    Try loading font information for TS1+cmr on input line 38.
     1077LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 40.
     1078LaTeX Font Info:    ... okay on input line 40.
     1079LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 40.
     1080LaTeX Font Info:    ... okay on input line 40.
     1081LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 40.
     1082LaTeX Font Info:    ... okay on input line 40.
     1083LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 40.
     1084LaTeX Font Info:    ... okay on input line 40.
     1085LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 40.
     1086LaTeX Font Info:    ... okay on input line 40.
     1087LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 40.
     1088LaTeX Font Info:    ... okay on input line 40.
     1089LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 40.
     1090LaTeX Font Info:    Try loading font information for TS1+cmr on input line 40.
    10911091 (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd
    10921092File: ts1cmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
    10931093)
    1094 LaTeX Font Info:    ... okay on input line 38.
    1095 LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 38.
    1096 LaTeX Font Info:    ... okay on input line 38.
    1097 LaTeX Font Info:    Try loading font information for T1+lmr on input line 38.
     1094LaTeX Font Info:    ... okay on input line 40.
     1095LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 40.
     1096LaTeX Font Info:    ... okay on input line 40.
     1097LaTeX Font Info:    Try loading font information for T1+lmr on input line 40.
    10981098
    10991099(/usr/share/texlive/texmf-dist/tex/latex/lm/t1lmr.fd
     
    11011101)
    11021102\AtBeginShipoutBox=\box57
    1103 Package hyperref Info: Link coloring OFF on input line 38.
     1103Package hyperref Info: Link coloring OFF on input line 40.
    11041104
    11051105(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
     
    11111111\c@section@level=\count139
    11121112)
    1113 LaTeX Info: Redefining \ref on input line 38.
    1114 LaTeX Info: Redefining \pageref on input line 38.
    1115 LaTeX Info: Redefining \nameref on input line 38.
     1113LaTeX Info: Redefining \ref on input line 40.
     1114LaTeX Info: Redefining \pageref on input line 40.
     1115LaTeX Info: Redefining \nameref on input line 40.
    11161116
    11171117(./FDL2012.out) (./FDL2012.out)
     
    11491149))
    11501150ABD: EveryShipout initializing macros
    1151 LaTeX Info: Redefining \degres on input line 38.
     1151LaTeX Info: Redefining \degres on input line 40.
    11521152
    11531153
    11541154Package frenchb.ldf Warning: The definition of \@makecaption has been changed,
    11551155(frenchb.ldf)                frenchb will NOT customise it;
    1156 (frenchb.ldf)                reported on input line 38.
    1157 
    1158 LaTeX Info: Redefining \dots on input line 38.
    1159 LaTeX Info: Redefining \up on input line 38.
    1160 LaTeX Info: Redefining \microtypecontext on input line 38.
     1156(frenchb.ldf)                reported on input line 40.
     1157
     1158LaTeX Info: Redefining \dots on input line 40.
     1159LaTeX Info: Redefining \up on input line 40.
     1160LaTeX Info: Redefining \microtypecontext on input line 40.
    11611161Package microtype Info: Generating PDF output.
    11621162Package microtype Info: Character protrusion enabled (level 2).
     
    11751175(RS)
    11761176)
    1177 LaTeX Font Info:    Try loading font information for OT1+lmr on input line 42.
     1177LaTeX Font Info:    Try loading font information for OT1+lmr on input line 44.
    11781178
    11791179(/usr/share/texlive/texmf-dist/tex/latex/lm/ot1lmr.fd
    11801180File: ot1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
    11811181)<<ot1.cmap>>
    1182 LaTeX Font Info:    Try loading font information for OML+lmm on input line 42.
     1182LaTeX Font Info:    Try loading font information for OML+lmm on input line 44.
    11831183
    11841184(/usr/share/texlive/texmf-dist/tex/latex/lm/omllmm.fd
    11851185File: omllmm.fd 2009/10/30 v1.6 Font defs for Latin Modern
    11861186)
    1187 LaTeX Font Info:    Try loading font information for OMS+lmsy on input line 42.
     1187LaTeX Font Info:    Try loading font information for OMS+lmsy on input line 44.
    11881188
    11891189
     
    11911191File: omslmsy.fd 2009/10/30 v1.6 Font defs for Latin Modern
    11921192)
    1193 LaTeX Font Info:    Try loading font information for OMX+lmex on input line 42.
     1193LaTeX Font Info:    Try loading font information for OMX+lmex on input line 44.
    11941194
    11951195
     
    11981198)
    11991199LaTeX Font Info:    External font `lmex10' loaded for size
    1200 (Font)              <12> on input line 42.
     1200(Font)              <12> on input line 44.
    12011201LaTeX Font Info:    External font `lmex10' loaded for size
    1202 (Font)              <8> on input line 42.
     1202(Font)              <8> on input line 44.
    12031203LaTeX Font Info:    External font `lmex10' loaded for size
    1204 (Font)              <6> on input line 42.
    1205 LaTeX Font Info:    Try loading font information for U+msa on input line 42.
     1204(Font)              <6> on input line 44.
     1205LaTeX Font Info:    Try loading font information for U+msa on input line 44.
    12061206
    12071207(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd
     
    12111211File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS)
    12121212)
    1213 LaTeX Font Info:    Try loading font information for U+msb on input line 42.
     1213LaTeX Font Info:    Try loading font information for U+msb on input line 44.
    12141214
    12151215(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd
     
    12191219File: mt-msb.cfg 2005/06/01 v1.0 microtype config. file: AMS symbols (b) (RS)
    12201220)
     1221(./introduction.tex
    12211222LaTeX Font Info:    External font `lmex10' loaded for size
    1222 (Font)              <10> on input line 73.
     1223(Font)              <10> on input line 15.
    12231224LaTeX Font Info:    External font `lmex10' loaded for size
    1224 (Font)              <7> on input line 73.
     1225(Font)              <7> on input line 15.
    12251226LaTeX Font Info:    External font `lmex10' loaded for size
    1226 (Font)              <5> on input line 73.
    1227 
    1228 
    1229 LaTeX Warning: Citation `GrumbergLong91assume_guarantee' on page 1 undefined on
    1230  input line 73.
    1231 
    1232 
    1233 LaTeX Warning: Citation `HQR98assume_guarantee' on page 1 undefined on input li
    1234 ne 73.
    1235 
    1236 [1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map}
     1227(Font)              <5> on input line 15.
     1228 [1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map}
    12371229
    12381230
    12391231
    12401232]
    1241 
    1242 LaTeX Warning: Citation `GrafSaidi97abstract_construct' on page 2 undefined on
    1243 input line 77.
    1244 
    1245 
    1246 LaTeX Warning: Citation `clarke00cegar' on page 2 undefined on input line 80.
    1247 
    1248 
    1249 Overfull \hbox (1.1072pt too wide) in paragraph at lines 80--81
     1233Overfull \hbox (1.1072pt too wide) in paragraph at lines 22--23
    12501234[]\T1/lmr/m/n/10 (-20) A few years later, an in-ter-est-ing abstraction-refinem
    12511235ent
    12521236 []
    12531237
    1254 
    1255 LaTeX Warning: Citation `XieBrowne03composition_soft' on page 2 undefined on in
    1256 put line 82.
    1257 
    1258 
    1259 LaTeX Warning: Citation `PMT02compositional_MC' on page 2 undefined on input li
    1260 ne 85.
    1261 
    1262 
    1263 LaTeX Warning: Citation `SNBE06property_based' on page 2 undefined on input lin
    1264 e 89.
    1265 
    1266 
    1267 LaTeX Warning: Citation `microsoft04SLAM' on page 2 undefined on input line 92.
    1268 
    1269 
    1270 
    1271 LaTeX Warning: Citation `berkeley07BLAST' on page 2 undefined on input line 92.
    1272 
    1273 
    1274 
    1275 LaTeX Warning: Citation `Kroening_al07vcegar' on page 2 undefined on input line
    1276  92.
    1277 
    1278 
    1279 LaTeX Warning: Citation `pwk2009-date' on page 2 undefined on input line 95.
    1280 
    1281 
    1282 LaTeX Warning: Citation `Kunz_al11ipc_abs' on page 2 undefined on input line 95
    1283 .
    1284 
    1285 
    1286 LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 2 undefined on in
    1287 put line 98.
    1288 
    1289 
    1290 LaTeX Warning: Citation `bara08abs_composant' on page 2 undefined on input line
    1291  98.
    1292 
    1293 
    1294 LaTeX Warning: Citation `clarke00cegar' on page 2 undefined on input line 104.
    1295 
    1296 
    1297 LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 2 undefined on in
    1298 put line 108.
    1299 
    1300 LaTeX Font Info:    Try loading font information for TS1+lmr on input line 114.
    1301 
    1302 (/usr/share/texlive/texmf-dist/tex/latex/lm/ts1lmr.fd
     1238) (./framework.tex [2]
     1239LaTeX Font Info:    Try loading font information for TS1+lmr on input line 23.
     1240 (/usr/share/texlive/texmf-dist/tex/latex/lm/ts1lmr.fd
    13031241File: ts1lmr.fd 2009/10/30 v1.6 Font defs for Latin Modern
    1304 ) [2]
    1305 LaTeX Font Info:    Try loading font information for U+bbold on input line 144.
    1306 
    1307  (./Ubbold.fd)
    1308 <our_CEGAR_Loop_Enhanced_2S_PNG.png, id=88, 238.64156pt x 119.69719pt>
     1242)
     1243<our_CEGAR_Loop_Enhanced_2S_PNG.png, id=122, 238.64156pt x 119.69719pt>
    13091244File: our_CEGAR_Loop_Enhanced_2S_PNG.png Graphic file (type png)
    13101245
    13111246<use our_CEGAR_Loop_Enhanced_2S_PNG.png>
    13121247Package pdftex.def Info: our_CEGAR_Loop_Enhanced_2S_PNG.png used on input line
    1313 182.
     124835.
    13141249(pdftex.def)             Requested size: 238.64096pt x 119.69688pt.
    1315 
    1316 
    1317 LaTeX Warning: Citation `braunstein07ctl_abstraction' on page 3 undefined on in
    1318 put line 190.
    1319 
    1320 
    1321 LaTeX Warning: Citation `bara08abs_composant' on page 3 undefined on input line
    1322  190.
    1323 
    1324 
    1325 LaTeX Warning: Citation `ucberkeley96vis' on page 3 undefined on input line 192
    1326 .
    1327 
    1328 [3 <./our_CEGAR_Loop_Enhanced_2S_PNG.png>]
    1329 Underfull \hbox (badness 10000) in paragraph at lines 224--230
     1250 [3 <./our_CEGAR_Loop_Enhanced_2S_PNG.png>]
     1251LaTeX Font Info:    Try loading font information for U+bbold on input line 86.
     1252 (./Ubbold.fd)) (./abstraction_refinement.tex
     1253Underfull \hbox (badness 10000) in paragraph at lines 28--34
    13301254
    13311255 []
    13321256
    13331257
    1334 Underfull \hbox (badness 10000) in paragraph at lines 224--230
     1258Underfull \hbox (badness 10000) in paragraph at lines 28--34
    13351259
    13361260 []
    13371261
    13381262
    1339 Underfull \hbox (badness 10000) in paragraph at lines 224--230
     1263Underfull \hbox (badness 10000) in paragraph at lines 28--34
    13401264
    13411265 []
    13421266
    13431267
    1344 Underfull \hbox (badness 10000) in paragraph at lines 238--241
     1268Underfull \hbox (badness 10000) in paragraph at lines 42--45
    13451269
    13461270 []
    13471271
    13481272
    1349 Underfull \hbox (badness 10000) in paragraph at lines 238--241
     1273Underfull \hbox (badness 10000) in paragraph at lines 42--45
    13501274
    13511275 []
    13521276
    1353 
    1354 Overfull \hbox (0.81122pt too wide) in paragraph at lines 244--245
     1277[4]
     1278Overfull \hbox (0.81122pt too wide) in paragraph at lines 48--49
    13551279[]\T1/lmr/m/it/10 (-20) If $\OMS/lmsy/m/n/10 8\OML/lmm/m/it/10 k$ \T1/lmr/m/it/
    1356128010 (-20) we have $[] \OMS/lmsy/m/n/10 ^^R \OML/lmm/m/it/10 V[]$ \T1/lmr/m/it/10
     
    13601284
    13611285
    1362 Overfull \hbox (3.01537pt too wide) in paragraph at lines 261--264
     1286Overfull \hbox (3.01537pt too wide) in paragraph at lines 67--70
    13631287\OML/lmm/m/it/10 max\OT1/lmr/m/n/10 (-20) (\OML/lmm/m/it/10 depth\OT1/lmr/m/n/1
    136412880 (-20) (\OML/lmm/m/it/10 Gv[]\OT1/lmr/m/n/10 (-20) )\OML/lmm/m/it/10 ; depth\O
     
    13681292 []
    13691293
    1370 [4]
    1371 Underfull \hbox (badness 10000) in paragraph at lines 296--297
     1294
     1295Underfull \hbox (badness 10000) in paragraph at lines 103--104
    13721296
    13731297 []
    13741298
    1375 <Dependency_graph_weight_PNG.png, id=118, 112.16907pt x 167.12437pt>
     1299[5] <Dependency_graph_weight_PNG.png, id=165, 112.16907pt x 167.12437pt>
    13761300File: Dependency_graph_weight_PNG.png Graphic file (type png)
    13771301
    13781302<use Dependency_graph_weight_PNG.png>
    1379 Package pdftex.def Info: Dependency_graph_weight_PNG.png used on input line 319
     1303Package pdftex.def Info: Dependency_graph_weight_PNG.png used on input line 126
    13801304.
    13811305(pdftex.def)             Requested size: 112.16878pt x 167.12395pt.
    13821306
    1383 Underfull \hbox (badness 10000) in paragraph at lines 344--345
     1307Underfull \hbox (badness 10000) in paragraph at lines 151--152
    13841308
    13851309 []
    13861310
    1387 [5 <./Dependency_graph_weight_PNG.png>]
    1388 Overfull \hbox (11.93875pt too wide) in paragraph at lines 357--358
     1311
     1312Overfull \hbox (11.93875pt too wide) in paragraph at lines 164--165
    13891313[]$\OML/lmm/m/it/10 S[] \OT1/lmr/m/n/10 (-20) = \OMS/lmsy/m/n/10 f\OML/lmm/m/it
    13901314/10 s[]; s[]; s[]; :::; s[]; s[]; :::; s[]\OMS/lmsy/m/n/10 g$
    13911315 []
    13921316
    1393 <K_sigma_i_S_PNG.png, id=126, 33.12375pt x 213.79875pt>
     1317<K_sigma_i_S_PNG.png, id=166, 33.12375pt x 213.79875pt>
    13941318File: K_sigma_i_S_PNG.png Graphic file (type png)
    13951319
    13961320<use K_sigma_i_S_PNG.png>
    1397 Package pdftex.def Info: K_sigma_i_S_PNG.png used on input line 380.
     1321Package pdftex.def Info: K_sigma_i_S_PNG.png used on input line 187.
    13981322(pdftex.def)             Requested size: 33.12366pt x 213.79822pt.
    13991323
     
    14011325LaTeX Warning: `!h' float specifier changed to `!ht'.
    14021326
    1403 
    1404 Underfull \hbox (badness 10000) in paragraph at lines 420--421
     1327[6 <./Dependency_graph_weight_PNG.png> <./K_sigma_i_S_PNG.png>]
     1328Underfull \hbox (badness 10000) in paragraph at lines 227--228
    14051329
    14061330 []
    14071331
    1408 
    1409 Underfull \hbox (badness 10000) in paragraph at lines 436--437
     1332)
     1333Underfull \hbox (badness 10000) in paragraph at lines 75--76
    14101334
    14111335 []
    14121336
    1413 [6 <./K_sigma_i_S_PNG.png>]
    1414 No file FDL2012.bbl.
    1415 Package atveryend Info: Empty hook `BeforeClearDocument' on input line 462.
    1416 [7
     1337(./FDL2012.bbl [7])
     1338Package atveryend Info: Empty hook `BeforeClearDocument' on input line 101.
     1339 [8
    14171340
    14181341]
    1419 Package atveryend Info: Empty hook `AfterLastShipout' on input line 462.
     1342Package atveryend Info: Empty hook `AfterLastShipout' on input line 101.
    14201343 (./FDL2012.aux)
    1421 Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 462.
    1422 Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 462.
     1344Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 101.
     1345Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 101.
    14231346Package rerunfilecheck Info: File `FDL2012.out' has not changed.
    1424 (rerunfilecheck)             Checksum: BA9407F3BD913632A2377663C2D85E5A;965.
    1425 
    1426 
    1427 LaTeX Warning: There were undefined references.
     1347(rerunfilecheck)             Checksum: 0706271851781CA86C089B6E9054600F;1151.
    14281348
    14291349
     
    14321352 )
    14331353Here is how much of TeX's memory you used:
    1434  18495 strings out of 492508
    1435  332547 string characters out of 3115493
    1436  452738 words of memory out of 3000000
    1437  21197 multiletter control sequences out of 15000+200000
    1438  69857 words of font info for 127 fonts, out of 3000000 for 9000
     1354 18602 strings out of 492508
     1355 333954 string characters out of 3115493
     1356 452425 words of memory out of 3000000
     1357 21205 multiletter control sequences out of 15000+200000
     1358 80503 words of font info for 162 fonts, out of 3000000 for 9000
    14391359 1648 hyphenation exceptions out of 8191
    1440  56i,10n,68p,951b,935s stack positions out of 5000i,500n,10000p,200000b,50000s
    1441 {/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texl
    1442 ive/texmf-dist/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/share/texlive/texmf-dist/
    1443 fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/
    1444 lm-mathit.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ec.enc}{/usr
     1360 56i,10n,68p,1177b,935s stack positions out of 5000i,500n,10000p,200000b,50000s
     1361{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-ec.enc}{/usr/share/texli
     1362ve/texmf-dist/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texlive/texmf-dist/font
     1363s/enc/dvips/lm/lm-mathsy.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/
     1364lm-rm.enc}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-mathit.enc}{/usr
    14451365/share/texlive/texmf-dist/fonts/enc/dvips/lm/lm-mathex.enc}<./bbold10.pfb></usr
    14461366/share/texlive/texmf-dist/fonts/type1/public/lm/lmbx10.pfb></usr/share/texlive/
    14471367texmf-dist/fonts/type1/public/lm/lmbx12.pfb></usr/share/texlive/texmf-dist/font
    1448 s/type1/public/lm/lmbxi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
    1449 /lm/lmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmmi10.pfb>
    1450 </usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmmi5.pfb></usr/share/texl
    1451 ive/texmf-dist/fonts/type1/public/lm/lmmi7.pfb></usr/share/texlive/texmf-dist/f
    1452 onts/type1/public/lm/lmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
    1453 c/lm/lmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmr5.pfb></
    1454 usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmr7.pfb></usr/share/texlive
    1455 /texmf-dist/fonts/type1/public/lm/lmri10.pfb></usr/share/texlive/texmf-dist/fon
    1456 ts/type1/public/lm/lmri12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
    1457 /lm/lmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmsy5.pfb><
    1458 /usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmsy7.pfb></usr/share/texli
    1459 ve/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texliv
    1460 e/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb>
    1461 Output written on FDL2012.pdf (7 pages, 353282 bytes).
     1368s/type1/public/lm/lmbx9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/l
     1369m/lmbxi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmex10.pfb><
     1370/usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmmi10.pfb></usr/share/texl
     1371ive/texmf-dist/fonts/type1/public/lm/lmmi5.pfb></usr/share/texlive/texmf-dist/f
     1372onts/type1/public/lm/lmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
     1373c/lm/lmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmr12.pfb><
     1374/usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmr5.pfb></usr/share/texliv
     1375e/texmf-dist/fonts/type1/public/lm/lmr7.pfb></usr/share/texlive/texmf-dist/font
     1376s/type1/public/lm/lmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm
     1377/lmri10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/lm/lmri12.pfb></u
     1378sr/share/texlive/texmf-dist/fonts/type1/public/lm/lmri9.pfb></usr/share/texlive
     1379/texmf-dist/fonts/type1/public/lm/lmsy10.pfb></usr/share/texlive/texmf-dist/fon
     1380ts/type1/public/lm/lmsy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
     1381lm/lmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols
     1382/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/
     1383msbm10.pfb>
     1384Output written on FDL2012.pdf (8 pages, 445373 bytes).
    14621385PDF statistics:
    1463  223 PDF objects out of 1000 (max. 8388607)
    1464  186 compressed objects within 2 object streams
    1465  40 named destinations out of 1000 (max. 500000)
    1466  21652 words of extra memory for PDF output out of 24883 (max. 10000000)
    1467 
     1386 285 PDF objects out of 1000 (max. 8388607)
     1387 243 compressed objects within 3 object streams
     1388 58 named destinations out of 1000 (max. 500000)
     1389 24228 words of extra memory for PDF output out of 24883 (max. 10000000)
     1390
  • papers/FDL2012/FDL2012.out

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

    r50 r52  
    2626\newtheorem{definition}{Definition}
    2727\newtheorem{property}{Property}
     28\newcommand{\TODO}[1] {\textcolor{red}{TODO : #1}}
     29\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
    2830
    2931
     
    5759\section{Introduction}
    5860
    59 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.
    60 
    61 
    62 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.
    63 
    64 
    65 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.
    66 
    67 
    68 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.
    69 
    70 
    71 \subsection{Related Works}
    72 
    73 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.
    74 
    75 
    76 
    77 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.
    78 
    79 
    80 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.
    81 
    82 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.
    83 
    84 
    85 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.
    86 
    87 
    88 
    89 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.
    90 
    91 
    92 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}.
    93 
    94 
    95 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.
    96 
    97 
    98 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.
    99 
     61\input{introduction}
    10062
    10163
    10264\section{Our Framework}
    10365
    104 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}.
    105 
    106 \subsection{Overall Description of our methodology}
    107 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.
    108 %\bigskip
    109 \begin{definition}
    110 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.
    111 \end{definition}
    112 
    113 TODO : FAUT-IL METTRE CETTE DEFINITION DE $\Phi$ ??
    114 
    115 \begin{definition}
    116 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:
    117 
    118 \begin{itemize}
    119 \item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
    120 \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. }
    121 \end{itemize}
    122 \end{definition}
    123 
    124 %\bigskip
    125 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}.
    126 
    127 \begin{figure}[h!]
    128 %   \centering
    129 %   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
    130 %     \hspace*{-5mm}
    131      \includegraphics{our_CEGAR_Loop_Enhanced_2S_PNG}
    132    \caption{\label{cegar} Verification Process }
    133 \end{figure}
    134 
    135 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}.
    136 
    137 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.
    138 
    139 \subsection{Definition of the abstraction of a component and of the complete system}
    140 
    141 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.
    142 
    143  
    144 %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}.
    145 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:
    146 
    147 \begin{definition}
    148 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 :
    149 
    150 \begin{itemize}
    151 \item { $\widehat{AP}$ : a finite set of atomic propositions}   
    152 \item { $\widehat{S}$ : a finite set of states}
    153 \item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
    154 \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:}
    155                 \begin{itemize}
    156                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
    157                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
    158                         \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
    159                   \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
    160                 \end{itemize}
    161 \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}$ }
    162 \item { $\widehat{F}$ : a set of fairness constraints TODO : PRECISER LEUR REPRESENTATION ET LES ARBRES ACCEPTES}
    163 \end{itemize}
    164 \end{definition}
    165 %\bigskip
    166 
    167 
    168 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.
    169 %\bigskip
    170 
    171 \begin{definition}
    172 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]$:
    173 
    174 \begin{itemize}
    175 \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
    176 \item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
    177 \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}$ ???????}
    178 \end{itemize}
    179 
    180 \hspace*{3mm}with :\\
    181 \hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
    182 \hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
    183 
    184 \end{definition}
    185 %\bigskip
    186 
    187 
    188 
    189 
    190 \subsection{Characterization of AKS}
    191 TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
    192 
    193 1. Ordering of AKS
    194 
    195 Def : Concrete and abstract variables in AKS
    196 
    197 Def : Concretization of an abstract variable
    198 
    199 Def (dual) : Abstraction of a concrete variable
    200 
    201 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.
    202 
    203 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 ???
    204  
    205 2. Negation of states in an AKS
    206 
    207 a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
    208 
    209 b) The negation of an configuration may be represented by a set of abstract configurations
    210 
    211 c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
    212 
    213 
     66\input{framework}
    21467\section{Abstraction Generation and Refinement}
    21568
    216 \subsection{Generalities}
    217 
    218 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$.
    219 
    220 \subsubsection{Refinement}
    221 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:
    222 
    223 %\medskip
    224 
    225 \begin{property}
    226 All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$.
    227 \end{property}
    228 %\bigskip
    229 \begin{property}
    230 $\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$.
    231 \end{property}
    232 
    233 %\bigskip
    234 %\newpage
    235 
    236 \subsubsection{The Counterexample}
    237 
    238 
    239 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.
    240 %\medskip
    241 
    242 \begin{definition}
    243 \textbf{\emph{The counterexample $\sigma_i$ :}} \\
    244 \\
    245 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$. \\
    246 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$. \\
    247 \\
    248 (\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$.)\\
    249 
    250 %\medskip
    251 
    252 \end{definition}
    253 
    254 %\bigskip
    255 
    256 \begin{definition}
    257 \textbf{\emph{Spurious counterexample :}} \\
    258 \\
    259 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'}$.\\
    260 
    261 \smallskip
    262 
    263 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}.
    264 
    265 \end{definition}
    266 
    267 
    268 
    269 \subsection{Pre-processing and pertinency ordering of properties}
    270 
    271 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}.
    272 
    273 %\bigskip
    274 
    275 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:
    276 
    277 
    278 \begin{enumerate}
    279 
    280 \item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
    281 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.
    282 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})) $.
    283 
    284 }
    285 
    286 \item {\emph{Weight allocation for each variables} \\
    287 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:
    288 \begin{itemize}
    289 \item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
    290  \\ \hspace*{20mm} $Wv_{max_d} = p$
    291 \item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
    292 \\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
    293 \item{...}
    294 \item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
    295  \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
    296 \item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
    297  \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
    298 \end{itemize}
    299 
    300 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$.
    301 }
    302 
    303 
    304 \item {\emph{Ordering of the properties} \\
    305 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}}$ .
    306 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$.
    307 
    308 
    309 }
    310 
    311 \end{enumerate}
    312 
    313 %\bigskip
    314 
    315 \emph{\underline{Example:}}  \\
    316 
    317 For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
    318 \begin{itemize}
    319 \item{$p$ is dependent of $a$ and $b$}
    320 \item{$b$ is dependent of $c$}
    321 \item{$q$ is dependent of $x$}
    322 \item{$r$ is independent}
    323 \end{itemize}
    324 
    325 Example with unit weight= 50.
    326 The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
    327 The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
    328 The tertiary level variable $c$ is weighted $50$. \\
    329 The weight of a non-related variable is $0$.
    330 
    331 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.
    332 
    333 \bigskip
    334 \begin{figure}[h!]
    335    \centering
    336 %   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
    337 %     \hspace*{-15mm}
    338      \includegraphics{Dependency_graph_weight_PNG}
    339    \caption{\label{DepGraphWeight} Example of weighting}
    340 \end{figure}
    341 
    342 %Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 

    343 
    344 
    345 
    346 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.
    347 
    348 
    349 
    350 
    351 \subsection{Initial abstraction generation}
    352 
    353 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.
    354 
    355 
    356 
    357 \subsection{Abstraction refinement}
    358 
    359 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
    360 
    361 \begin{enumerate}
    362 
    363 \item {\emph{\underline{Step 1:}} \\
    364 
    365 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$.
    366 
    367 \bigskip
    368 
    369 \begin{definition}
    370 \textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
    371 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 \\
    372 $K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :
    373 
    374 \begin{itemize}
    375 \item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }     
    376 \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}\}$}
    377 \item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
    378 \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. }
    379 \item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
    380 \end{itemize}
    381 \end{definition}
    382 
    383 %\bigskip
    384 All the properties available are then model-checked on $K(\sigma_i)$.
    385 
    386 If:
    387 \begin{itemize}
    388 \item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
    389 \item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
    390 \end{itemize}
    391 
    392 %\bigskip
    393 
    394 
    395 \begin{figure}[h!]
    396    \centering
    397 %   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
    398 %     \hspace*{-15mm}
    399      \includegraphics{K_sigma_i_S_PNG}
    400    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    401 \end{figure}
    402 
    403 %Dans la figure~\ref{étiquette} page~\pageref{étiquette}, 

    404 
    405 %\bigskip
    406 
    407 
    408 \begin{figure}[h!]
    409    \centering
    410 
    411 \begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm,
    412                     thick]
    413   \tikzstyle{every state}=[fill=none,draw=blue,text=black]
    414 
    415   \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
    416   \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};
    417 
    418   \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};
    419 
    420   \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
    421   \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};
    422 
    423   \path (A) edge              node {} (B)
    424             (B) edge       node {} (C)
    425             (C) edge             node {} (D)
    426             (D) edge             node {} (E);
    427 
    428 \end{tikzpicture}
    429 
    430    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    431 \end{figure}
    432 
    433 
    434 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$.
    435 
    436 }
    437 %\bigskip
    438 
    439 \item {\emph{\underline{Step 2:}} \\
    440 
    441 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}$.
    442 %\bigskip
    443 
    444 }
    445 \end{enumerate}
    446 
    447 $\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.
    448 
    449 
     69\input{abstraction_refinement}
    45070
    45171
Note: See TracChangeset for help on using the changeset viewer.