Changeset 101 for papers/FDL2012


Ignore:
Timestamp:
Jul 19, 2012, 11:44:48 AM (12 years ago)
Author:
syed
Message:

final

Location:
papers/FDL2012
Files:
8 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r95 r101  
    3232\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
    3333
    34 
     34%\vspace*{-15mm}
    3535 \title{ An efficient refinement strategy exploiting component properties in a CEGAR process}
    36 % \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ}
     36 \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ}
    3737% \thanks{This work was supported by...}}
    38 % \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
    39 %                 LIP6-SOC (CNRS UMR 7606), \\
    40 %                            4, place Jussieu, \\
    41 %                75005 Paris, FRANCE. }
    42 \name{Removed for blind review}
    43 \address{ }
     38 \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
     39                 LIP6-SOC (CNRS UMR 7606), \\
     40                            4, place Jussieu, \\
     41                75005 Paris, FRANCE. }
     42%\name{Removed for blind review}
     43%\address{ }
    4444
    4545\begin{document}
    … …  
    4949
    5050\begin{abstract}
    51 Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have conducted several preliminary experimentations which shows that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS \cite{ucberkeley96vis}.
     51Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have conducted several preliminary experimentations which show that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS \cite{ucberkeley96vis}.
    5252\end{abstract}
    5353
    … …  
    9090which is well adapted for compositional embedded systems. This verification
    9191technique is compatible and suits well in the natural development process of
    92 complex systems. Our preliminary experimental results shows an interesting
    93 performance in terms of duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.
     92complex systems. Our preliminary experimental results show an interesting
     93performance in terms of duration of abstraction generation and the number of refinement iteration. Furthermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.
    9494
    9595Nevertheless, in order to function well, this refinement technique requires a
    96 complete specification of every components of the concrete model. Futhermore,
     96well constituted specification of every components of the concrete model. Furthermore,
    9797it may be possible that none of the properties available is capable of
    9898eliminating the counterexample which is probably due to an incomplete
    … …  
    100100local properties. In this case, other refinement techniques such as the
    101101refinement by eliminating the counterexample only, or the identification of a
    102 good set of local properties to be integreted simultaneously, should be considered.
     102good set of local properties to be integrated simultaneously, should be considered.
    103103We are currently investigating other complementary techniques to overcome these particular cases.
    104 A complementary approach consists in improving the specification of the
    105 model~: at the component level, or for groups of components. The work of
    106 Kroening \cite{pwk2009-date} could help us in this direction.
     104The work of Kroening \cite{pwk2009-date}, for example, could also help us in improving the specification of the
     105model: at the component level, or for groups of components.
    107106
    108 %footnote for Table 1
    109 \footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
     107%A complementary approach consists in improving the specification of the
     108%model~: at the component level, or for groups of components. The work of
     109%Kroening \cite{pwk2009-date} could help us in this direction.
     110
     111
     112
    110113
    111114%\begin{thebibliography}
    … …  
    118121%\end{thebibliography}
    119122
    120 
     123%footnote for Table 1
     124\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM}
    121125
    122126\end{document}

  • papers/FDL2012/abstraction_refinement.tex

    r93 r101  
    2626$\widehat{M}_i$ ensure item 2. Concretization can be performed by
    2727modifying the AKS of $\widehat{M}_i$ by changing some abstract value to
    28 concrete ones. However, this approach is rude : in order to ensure item 1,
     28concrete ones. However, this approach is rude: in order to ensure item 1,
    2929the concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
    3030%Another way to concretize some variables at selected instants is to compose
    … …  
    3232
    3333We propose to compose the abstraction with another AKS to build a good refinement
    34 according to definition \ref{def:goodrefinement}.
    35 We have  several options. The most straightforward consists in building
    36 an AKS representing all possible executions except the  spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
     34according to Definition \ref{def:goodrefinement}.
     35We have several options. The most straightforward method consists in building
     36an AKS representing all possible executions except the  spurious counterexample; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones: first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
    3737
    3838
    … …  
    4343counterexample given by the model-checker, the variable configuration in each
    4444state is Boolean. We name $\widehat{L_i}$ this new labeling.
    45 The spurious counterexample $\sigma$ is defined such that :
     45The spurious counterexample $\sigma$ is defined such that:
    4646\begin{definition}
    4747Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
    … …  
    7070counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
    7171\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
    72 \widehat{F}_{\overline{\sigma}} \rangle$ is such that :
     72\widehat{F}_{\overline{\sigma}} \rangle$ is such that:
    7373\vspace*{-2mm}
    7474\begin{itemize}
    … …  
    9898The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
    9999configurations {\it but} the one of $s_i$. This last set may not be representable by
    100 the labeling function defined in def \ref{def-aks}. State labeling is treated
     100the labeling function defined in Definition \ref{def-aks}. State labeling is treated
    101101in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}.
    102102%The size of this structure is linear with the size of the counter-example.
    … …  
    139139model. The strengthening of the abstraction $\widehat{M}_i$ with the
    140140addition of AKS of already verified local CTL properties eliminates sets of
    141 behaviors and guarantees the over-approximation (property
     141behaviors and guarantees the over-approximation (Property
    142142\ref{prop:concrete_compose}) but does not guarantee the elimination of the counterexample. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counterexample.
    143143

  • papers/FDL2012/exp_results.tex

    r93 r101  
    1313\begin{table*} [ht]
    1414\hspace*{15mm}
    15 \small
     15%\small
     16\footnotesize
    1617\begin{tabular}{cclcccc}
    1718
    … …  
    4647\bottomrule 
    4748%\bottomrule
    48 
    4949\end{tabular}
    50 
    5150\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform}
    5251\end{table*}
    … …  
    128127$\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger
    129128version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of
    130 26 verifed components properties to be selected in VCI-PI platform.
     12926 verified components properties to be selected in the VCI-PI platform.
    131130In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
    132131
    … …  
    139138to verify both global properties without refinement.
    140139
    141 Globally, we can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding  more connected components, in contrary to the other two methods, our computation time remains stable.
     140Globally, we can see that our technique, for these examples, systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding  more connected components, in contrary to the other two methods, our computation time remains stable. This is mainly due to the fact that for small number of properties, our abstraction is generated almost instantly and as only pertinent properties are selected, not many refinement iterations are required in order to complete the verification process. It is also important to note that the properties tested are simple and we have in our property selection list the local properties required to satisfy the global property.
    142141
    143142

  • papers/FDL2012/framework.tex

    r93 r101  
    11The model-checking technique we propose is based on the Counterexample-guided
    22Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
    3 description of our methodology is shown in figure \ref{cegar}.
     3description of our methodology is shown in Figure \ref{cegar}.
    44We take into account the structure of the system as a set of synchronous components,
    55each of which has been previously verified and a set of CTL properties is
    … …  
    211211\end{itemize}
    212212\vspace*{-2mm}
    213 By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
     213By Property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
    214214$\widehat{M}_i$ and by
    215215the property of parallel composition,

  • papers/FDL2012/introduction.tex

    r95 r101  
    1 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 and catastrophic consequences.
     1The embedded systems correspond to the integration into the same electronic circuit, a huge number of complex functionalities performed by several heterogeneous 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 and catastrophic consequences.
    22
    33
    … …  
    2828
    2929
    30  Xie and Browne have proposed a method for software verification based on composition 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 has been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}.
     30 Xie and Browne have proposed a method for software verification based on composition 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 has been successful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}.
    3131
    3232
    33 In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. 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. Since, there have been other works on construction of components from interval temporal logic properties which could be used to speed up verification process \cite{SNBE06property_based} \cite{Kunz_al11ipc_abs}.
     33In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specifications are in ACTL. 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. Since, there have been other works on construction of components from interval temporal logic properties which could be used to speed up verification process \cite{SNBE06property_based} \cite{Kunz_al11ipc_abs}.
    3434
    3535%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.
    … …  
    5151
    5252%\subsection{Contribution}
    53 \textbf{\emph{Contribution :}} In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. We propose a technique to classify component properties according to their pertinency towards the global property, thus, enabling a better selection of properties for the initial abstraction generation. Futhermore, in the case where the verification is not conclusive, we propose a technique guided by the counterexample given by the model-checker to select supplementary properties to improve the abstraction.   
     53\textbf{\emph{Contribution :}} In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. We propose a technique to classify component properties according to their pertinency towards the global property, thus, enabling a better selection of properties for the initial abstraction generation. Furthermore, in the case where the verification is not conclusive, we propose a technique guided by the counterexample given by the model-checker to select supplementary properties to improve the abstraction.   
    5454
    5555

  • papers/FDL2012/myBib.bib

    r92 r101  
    1010
    1111@ARTICLE{clarke94model,
    12   author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
    13   title = {{Model Checking and Abstraction}},
     12  author = {E. M.~Clarke and O.~Grumberg and D.E.~Long},
     13  title = {Model Checking and Abstraction},
    1414  journal = {ACM Transactions on Programming Languages and Systems},
    15   year = {1994},
    1615  volume = {16},
    1716  pages = {1512--1542},
    … …  
    2120  issn = {0164-0925},
    2221  keywords = {model cheking, abstraction, CTL, preservation},
    23   publisher = {ACM Press}
    24 }
     22  publisher = {ACM Press},
     23  year = {1994}
     24}
     25
     26
    2527@PHDTHESIS{braunstein_phd07,
    2628  author = {C.~Braunstein},
    … …  
    2830        Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
    2931        Puce"},
    30   school = {{Universitée Pierre et Marie Curie (Paris 6)}},
     32  school = {Université Pierre et Marie Curie},
    3133  year = {2007},
    32   address = {LIP6/SOC},
     34  address = {LIP6-SOC},
    3335  owner = {cecile},
    3436  timestamp = {2007.04.16}
    … …  
    4648@conference{ ClarkeEmerson81temporal_logic,
    4749   author = "E. M. Clarke and  E. A. Emerson",
    48    title = "Design and systhesis of synchronization  skeletons using branching time temporal logic",
    49    booktitle = "In Logic of Programs Workshop",
     50   title = "Design and systhesis of synchronization skeletons using branching time temporal logic",
     51   booktitle = "Logic of Programs Workshop",
    5052   volume = 131,
    5153   address = "Yorktown Heights, New York",
    52    year = 1981,
    5354   month = May,
    54    publisher = "LNCS 131, Springer "
     55   publisher = "LNCS 131, Springer",
     56   year = 1981
    5557}
    5658
    … …  
    6264   number = 2,
    6365   pages = {244-263},
    64    year = 1986,
    65    month = Apr
     66   year = 1986
    6667}
    6768
    … …  
    6970   author = "E. M. Clarke and  O. Grumberg and S. Jha and Y. Lu and H. Veith",
    7071   title = "{Counterexample-guided Abstraction Refinement}",
    71    booktitle = "Computer Aided Verification (CAV '00)",
     72   booktitle = "CAV'00",
    7273   address = "Chicago, IL",
    73    year = 2000,
    74    publisher = "LNCS"
     74   publisher = "LNCS",
     75   year = 2000
    7576}
    7677
    … …  
    7879   author = "J. P. Queille and J. Sifakis",
    7980   title = "Specification and verification of concurrent systems in CESAR",
    80    booktitle = "In Proceedings of the 5th International Symposium on Programming",
     81   booktitle = "Proceedings of the 5th International Symposium on Programming",
    8182   volume = 137,
    8283   address = "Turin, Italy",
    83    year = 1982,
    8484   month = April,
    85    publisher = "LNCS 137, Springer "
     85   publisher = "LNCS 137, Springer",
     86   year = 1982
    8687}
    8788
    … …  
    9091@conference{ BCCFZ04SMC_with_SAT,
    9192    author = "A. Biere and A. Cimatti and E. Clarke and M.Fujita and Y. Zhu",
    92     title = "{ Symbolic Model  Checking using SAT procedures instead of BDDs}",
     93    title = "{Symbolic Model  Checking using SAT procedures instead of BDDs}",
    9394     booktitle = {Proceedings: Design Automation Conference (DAC '99)},
    9495    pages = {317-320},
    95     year = 1999,
    9696    month = February,
     97    year = 1999
    9798}
    9899
    … …  
    101102    author = "The VIS Group",
    102103    title = "{VIS: A system for Verification and Synthesis}",
    103     journal = {Springer Lecture Notes in Computer Science},
     104    journal = {Springer LNCS},
    104105    volume = 1102,
    105     number = 1102,
    106106    pages = {428-432},
    107107    year = 1996
    … …  
    114114     booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
    115115    pages = {519-522},
    116     year = 2004,
    117116    month = Jul,
    118     publisher = "LNCS 3114"
     117    publisher = "LNCS 3114",
     118    year = 2004
    119119}
    120120
    … …  
    154154   author = "C. Roux and  E. Encrenaz ",
    155155   title = "{CTL} may be ambigous when model-checking {Moore Machines} ",
    156    booktitle = " IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
     156   booktitle = "IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
    157157   volume = 2860,
    158158   address = "Italy",
    159    year = 2003,
    160159   month = Nov,
    161    publisher = "LNCS"
     160   publisher = "LNCS",
     161   year = 2003
    162162}
    163163
    … …  
    166166   author = "F. Xie and J.C. Browne ",
    167167   title = "{Verified Systems by Composition from Verified Components} ",
    168    booktitle = " In ESEC/FSE 2003: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference",
     168   booktitle = "ESEC/FSE 2003: 11th ACM SIGSOFT Symposium on Foundations of Software Eng. Conf.",
    169169   pages = {227-286},
    170    address = "Helsinki, Finland",
    171    year = 2003,
    172    publisher = "ACM Press"
     170   address = "Finland",
     171   publisher = "ACM Press",
     172   year = 2003
    173173}
    174174
    … …  
    177177   author = "J. Li and X. Sun and F. Xie and X. Song",
    178178   title = "{Component-Based Abstraction Refinement} ",
    179    booktitle = "In Proc. of 10th International Conference on Software Reuse (ICSR)",
     179   booktitle = "10th Int. Conf. on Software Reuse (ICSR)",
    180180   pages = {39-51},
    181    address = "Beijing, China",
    182    year = 2008,
    183    publisher = "Springer-Verlag"
     181   address = "China",
     182   publisher = "Springer-Verlag",
     183   year = 2008
    184184}
    185185
    … …  
    189189   author = "H. Peng and Y. Mokhtari and S. Tahar ",
    190190   title = "{Environment Synthesis for Compositional Model Checking} ",
    191    booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design",
     191   booktitle = "ICCD’02: 20th Int. Conference on Computer Design",
    192192   pages = {70-75},
    193193   address = "Freiburg, Germany",
    194    year = 2002,
    195    publisher = "IEEE Computer Society"
     194   publisher = "IEEE Computer Society",
     195   year = 2002
    196196}
    197197
    … …  
    200200   author = "M. Schickel  and V. Nimbler and M. Braun and H. Eveking ",
    201201   title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ",
    202    booktitle = "In FDL’06: Proceedings of Forum on specification and Design Languages",
     202   booktitle = "FDL’06: Forum on specification and Design Languages",
    203203   year = 2006
    204204}
    … …  
    207207@conference{ CiardoLS00mdd_async,
    208208   author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu",
    209    title = "{ Efficient symbolic state-space construction for asynchronous systems} ",
    210    booktitle = "In Proc. of ICATPN '2000",
     209   title = "{Efficient symbolic state-space construction for asynchronous systems} ",
     210   booktitle = "Proc. of ICATPN '2000",
    211211   volume = 1825,
    212212   pages = {103-122},
    213    year = 2000,
    214    publisher = "LNCS, Springer Verlag"
     213   publisher = "LNCS, Springer Verlag",
     214   year = 2000
    215215}
    216216
    217217@conference{ CTM05hdd,
    218218   author = "J-M. Couvreur and Y. Thierry-Mieg",
    219    title = "{ Hierarchical Decision Diagrams to Exploit Model Structure} ",
    220    booktitle = "In FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems",
     219   title = "{Hierarchical Decision Diagrams to Exploit Model Structure} ",
     220   booktitle = "FORTE: 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems",
    221221   volume = 3731,
    222222   pages = {443-457},
    223223   address = "Taipei, Taiwan",
    224    year = 2005,
    225    publisher = "LNCS, Springer"
     224   publisher = "LNCS, Springer",
     225   year = 2005
    226226}
    227227
    … …  
    229229@conference{ HQR98assume_guarantee,
    230230   author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
    231    title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
    232    booktitle = "CAV’98: Proceedings of the 10th Int. Conference on Computer Aided Verification",
     231   title = "{You Assume, We Guarantee: Methodology and Case Studies} ",
     232   booktitle = "CAV’98",
    233233   volume = 1427,
    234234   pages = {440-451},
    235    address = "Vancouver, Canada",
    236    year = 1998,
    237    publisher = " LNCS, Springer-Verlag"
     235   address = "Canada",
     236   publisher = "Springer-Verlag",
     237   year = 1998
    238238}
    239239
    240240
    241241@conference{ GrumbergLong91assume_guarantee,
    242    author = " O. Grumberg and D. E. Long",
    243    title = "{  Model Checking and Modular Verification} ",
    244    booktitle = " In International Conference on Concurency Theory",
     242   author = "O. Grumberg and D. E. Long",
     243   title = "{Model Checking and Modular Verification}",
     244   booktitle = "Int. Conference on Concurency Theory",
    245245   volume = 527,
    246246   pages = {250-263},
    247    year = 1991,
    248    publisher = " LNCS, Springer-Verlag"
     247   publisher = "Springer-Verlag",
     248   year = 1991
    249249}
    250250
    251251
    252252@conference{ GrafSaidi97abstract_construct,
    253    author = "  S. Graf and H. Saïdi",
    254    title = "{ Construction of Abstract State Graphs with PVS} ",
    255    booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
     253   author = "S. Graf and H. Saïdi",
     254   title = "{Construction of Abstract State Graphs with PVS}",
     255   booktitle = "Computer Aided Verification (CAV’97)",
    256256   volume = 1254,
    257    year = 1997,
    258    publisher = " LNCS, Springer"
     257   publisher = "LNCS, Springer",
     258   year = 1997
    259259}
    260260
    … …  
    262262
    263263@conference{ PardoHachtel97autoAbsMC,
    264    author = "  S. Pardo and G. Hachtel",
    265    title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
    266    booktitle = " In CAV ’97",
     264   author = "S. Pardo and G. Hachtel",
     265   title = "{Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
     266   booktitle = "CAV’97",
    267267   volume = 1254,
    268268   pages = {12-23},
    269    year = 1997,
    270    publisher = " LNCS, Springer-Verlag"
     269   publisher = "Springer-Verlag",
     270   year = 1997
    271271}
    272272
    … …  
    274274@conference{ PardoHachtel98incremCTLMC,
    275275   author = "  S. Pardo and G. Hachtel",
    276    title = "{ Incremental CTL Model Checking Using BDD Subsetting} ",
    277    booktitle = " In DAC ’98: 35th Design Automation Conference ",
     276   title = "{Incremental CTL Model Checking Using BDD Subsetting} ",
     277   booktitle = "DAC ’98: 35th Design Automation Conference ",
    278278   pages = {457-462},
    279    year = 1998,
     279   year = 1998
    280280}
    281281
    … …  
    283283@conference{ Burch_al91smc_part_transition,
    284284   author = " J. R. Burch and E. M. Clarke and D. E. Long",
    285    title = "{ Symbolic Model Checking with Partitioned Transition Relations} ",
     285   title = "{Symbolic Model Checking with Partitioned Transition Relations} ",
    286286   booktitle = "Proceedings of the 1991 International Conference on VLSI",
    287287   pages = {49-58},
    288288   month = August,
    289    year = 1991,
     289   year = 1991
    290290}
    291291
    292292
    293293@conference{ Burch_al93smc_circuit_verif,
    294    author = " J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli",
    295    title = "{ Symbolic Model Checking for Sequential Circuit Verification} ",
    296    booktitle = " IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
     294   author = "J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli",
     295   title = "{Symbolic Model Checking for Sequential Circuit Verification} ",
     296   booktitle = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
    297297   volume = {13(4)},
    298298   pages = {401-424},
    299    year = 1993,
     299   year = 1993
    300300}
    301301
    302302
    303303@conference{ Kroening_al07vcegar,
    304    author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke",
    305    title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
    306    booktitle = " In TACAS '07 ",
    307    year = 2007,
     304   author = " H. Jain and D. Kroening and N. Sharygina and E. Clarke",
     305   title = "{VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
     306   booktitle = "TACAS'07 ",
     307   year = 2007
    308308}
    309309
    310310
    311311@ARTICLE { Sharygina_al12PreciseApprox,
    312     AUTHOR = { Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich },
    313     TITLE = { {An Abstraction Refinement Approach Combining Precise and Approximated Techniques} },
    314     JOURNAL = { International Journal on Software Tools for Technology Transfer (STTT) },
     312    AUTHOR = {N. Sharygina and S. Tonetta and A. Tsitovich},
     313    TITLE = {An Abstraction Refinement Approach Combining Precise and Approximated Techniques},
     314    JOURNAL = {International Journal on Software Tools for Technology Transfer},
    315315    VOLUME = {14},
    316316    PAGES ={1-14},
    317     YEAR = { 2012},
     317    YEAR = {2012}
    318318}
    319319
    320320
    321321@conference{ microsoft04SLAM,
    322    author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani",
    323    title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
    324    booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)",
     322   author = "T. Ball and B. Cook and V. Levin and S. K. Rajamani",
     323   title = "{SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
     324   booktitle = "4th Int. Conf. on Integrated Formal Methods",
    325325   volume = 2999,
    326326   pages = {1-20},
    327    year = 2004,
    328    publisher = " LNCS, Springer"
     327   publisher = "Springer",
     328   year = 2004
    329329}
    330330
    331331
    332332@conference{ berkeley07BLAST,
    333    author = "  Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
    334    title = "{ The Software Model Checker Blast: Applications to software engineering.} ",
    335    booktitle = " International Journal on Software Tools for Technology Transfer",
     333   author = "D. Beyer and T. A. Henzinger and R. Jhala and R. Majumdar",
     334   title = "{The Software Model Checker Blast: Applications to software engineering} ",
     335   booktitle = "Int. Journal on Software Tools for Technology Transfer",
    336336   volume = {9 (5-6)},
    337337   pages = {505-525},
    338    year = 2007,
     338   year = 2007
    339339}
    340340
    341341
    342342@inproceedings{pwk2009-date,
    343   AUTHOR    = { Mitra Purandare and Thomas Wahl and Daniel Kroening },
    344   TITLE     = { Strengthening Properties using Abstraction Refinement },
    345   BOOKTITLE = { Proceedings of DATE 2009 },
    346   YEAR      = { 2009 },
    347   PUBLISHER = { ACM },
    348   PAGES     = { 1692-1697 },
     343  AUTHOR    = {M. Purandare and T. Wahl and D. Kroening},
     344  TITLE     = {Strengthening Properties using Abstraction Refinement},
     345  BOOKTITLE = {Proceedings of DATE 2009},
     346  PUBLISHER = {ACM},
     347  PAGES     = {1692-1697},
     348  YEAR      = {2009}
    349349}
    350350
    351351
    352352@conference{ Kunz_al11ipc_abs,
    353    author = " Minh D. Nguyen and Markus Wedler and Dominik Stoffel and Wolfgang Kunz ",
    354    title = "{ Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}",
    355    booktitle = "48th Proc. Design Automation Conference (DAC '11)",
     353   author = "M. D. Nguyen and M. Wedler and D. Stoffel and W. Kunz ",
     354   title = "{Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}",
     355   booktitle = "Design Automation Conference (DAC'11)",
    356356   address = "San Diego, USA",
    357    year = 2011,
     357   year = 2011
    358358}
    359359
    … …  
    363363 publisher = "Addison-Wesley",
    364364 title     = "The {\TeX}book",
    365  year      =  1984,
    366  isbn      = ""
     365 year      =  1984
    367366}
    368367

  • papers/FDL2012/ordering_filter_properties.tex

    r94 r101  
    1  We propose an
     1 We propose a
    22heuristic to order the properties  depending on the structure
    33of each component.
    … …  
    3535Note that a variable may belong to more than one dependency graph, in that case
    3636we consider the minimum depth.
    37 \item Give a weight to each variable (see algorithm  \ref{algo:weight}).
    38 \item Compute the weight of properties for each component~: sum of the
     37\item Give a weight to each variable (see Algorithm  \ref{algo:weight}).
     38\item Compute the weight of properties for each component: sum of the
    3939property variables weight.
    4040\end{enumerate}
    4141
    42 The algorithm \ref{algo:weight} gives weight according to the variable distance to the
     42The Algorithm \ref{algo:weight} gives weight according to the variable distance to the
    4343primary variable with extra weight for interface variable and primary variable.
    4444
    … …  
    250250property holds then the property will not eliminate the counterexample.
    251251Hence this property is not a good candidate for refinement.
    252 Therefore the highest weighted property not satisfied in $K(\sigma)$ is choosen to be
     252Therefore the highest weighted property not satisfied in $K(\sigma)$ is chosen to be
    253253integrated in the next refinement step. This process is iterated for each
    254254refinement step.
    … …  
    274274$AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$
    275275otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS
    276 definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate
    277 $\sigma$.
     276definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate $\sigma$.
    278277\end{enumerate}
    279278\end{proof}
    … …  
    281280\vspace*{-2mm}
    282281The proposed approach ensures that the refinement excludes the counterexample
    283 and  respects the definition \ref{def:goodrefinement}.
    284 We will show in our experiments that first the time needed to build an AKS is
     282and  respects the Definition \ref{def:goodrefinement}.
     283We will show in our experiments that first, the time needed to build an AKS is
    285284negligible and secondly the refinement converges rapidly.
    286285%The property at the top of the list (not yet selected and excluding the properties
Note: See TracChangeset for help on using the changeset viewer.