Index: papers/FDL2012/FDL2012.tex =================================================================== --- papers/FDL2012/FDL2012.tex (revision 95) +++ papers/FDL2012/FDL2012.tex (revision 101) @@ -32,14 +32,14 @@ \newcommand{\remark}[2]{\textcolor{blue}{#1: #2}} - +%\vspace*{-15mm} \title{ An efficient refinement strategy exploiting component properties in a CEGAR process} -% \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ} + \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ} % \thanks{This work was supported by...}} -% \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\ -% LIP6-SOC (CNRS UMR 7606), \\ -% 4, place Jussieu, \\ -% 75005 Paris, FRANCE. } -\name{Removed for blind review} -\address{ } + \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\ + LIP6-SOC (CNRS UMR 7606), \\ + 4, place Jussieu, \\ + 75005 Paris, FRANCE. } +%\name{Removed for blind review} +%\address{ } \begin{document} @@ -49,5 +49,5 @@ \begin{abstract} -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}. +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 show that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS \cite{ucberkeley96vis}. \end{abstract} @@ -90,9 +90,9 @@ which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of -complex systems. Our preliminary experimental results shows an interesting -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. +complex systems. Our preliminary experimental results show an interesting +performance 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. Nevertheless, in order to function well, this refinement technique requires a -complete specification of every components of the concrete model. Futhermore, +well constituted specification of every components of the concrete model. Furthermore, it may be possible that none of the properties available is capable of eliminating the counterexample which is probably due to an incomplete @@ -100,12 +100,15 @@ local properties. In this case, other refinement techniques such as the refinement by eliminating the counterexample only, or the identification of a -good set of local properties to be integreted simultaneously, should be considered. +good set of local properties to be integrated simultaneously, should be considered. We are currently investigating other complementary techniques to overcome these particular cases. -A complementary approach consists in improving the specification of the -model~: at the component level, or for groups of components. The work of -Kroening \cite{pwk2009-date} could help us in this direction. +The work of Kroening \cite{pwk2009-date}, for example, could also help us in improving the specification of the +model: at the component level, or for groups of components. -%footnote for Table 1 -\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM} +%A complementary approach consists in improving the specification of the +%model~: at the component level, or for groups of components. The work of +%Kroening \cite{pwk2009-date} could help us in this direction. + + + %\begin{thebibliography} @@ -118,5 +121,6 @@ %\end{thebibliography} - +%footnote for Table 1 +\footnotetext[1]{Computed on a calculation server: 2x Xeon X5650, 72Go RAM} \end{document} Index: papers/FDL2012/abstraction_refinement.tex =================================================================== --- papers/FDL2012/abstraction_refinement.tex (revision 95) +++ papers/FDL2012/abstraction_refinement.tex (revision 101) @@ -26,5 +26,5 @@ $\widehat{M}_i$ ensure item 2. Concretization can be performed by modifying the AKS of $\widehat{M}_i$ by changing some abstract value to -concrete ones. However, this approach is rude : in order to ensure item 1, +concrete ones. However, this approach is rude: in order to ensure item 1, the 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. %Another way to concretize some variables at selected instants is to compose @@ -32,7 +32,7 @@ We propose to compose the abstraction with another AKS to build a good refinement -according to definition \ref{def:goodrefinement}. -We have several options. The most straightforward consists in building -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$. +according to Definition \ref{def:goodrefinement}. +We have several options. The most straightforward method consists in building +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$. @@ -43,5 +43,5 @@ counterexample given by the model-checker, the variable configuration in each state is Boolean. We name $\widehat{L_i}$ this new labeling. -The spurious counterexample $\sigma$ is defined such that : +The spurious counterexample $\sigma$ is defined such that: \begin{definition} Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, @@ -70,5 +70,5 @@ counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, -\widehat{F}_{\overline{\sigma}} \rangle$ is such that : +\widehat{F}_{\overline{\sigma}} \rangle$ is such that: \vspace*{-2mm} \begin{itemize} @@ -98,5 +98,5 @@ The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all configurations {\it but} the one of $s_i$. This last set may not be representable by -the labeling function defined in def \ref{def-aks}. State labeling is treated +the labeling function defined in Definition \ref{def-aks}. State labeling is treated in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}. %The size of this structure is linear with the size of the counter-example. @@ -139,5 +139,5 @@ model. The strengthening of the abstraction $\widehat{M}_i$ with the addition of AKS of already verified local CTL properties eliminates sets of -behaviors and guarantees the over-approximation (property +behaviors and guarantees the over-approximation (Property \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. Index: papers/FDL2012/exp_results.tex =================================================================== --- papers/FDL2012/exp_results.tex (revision 95) +++ papers/FDL2012/exp_results.tex (revision 101) @@ -13,5 +13,6 @@ \begin{table*} [ht] \hspace*{15mm} -\small +%\small +\footnotesize \begin{tabular}{cclcccc} @@ -46,7 +47,5 @@ \bottomrule %\bottomrule - \end{tabular} - \caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform} \end{table*} @@ -128,5 +127,5 @@ $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of -26 verifed components properties to be selected in VCI-PI platform. +26 verified components properties to be selected in the VCI-PI platform. In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. @@ -139,5 +138,5 @@ to verify both global properties without refinement. -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. +Globally, 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. Index: papers/FDL2012/framework.tex =================================================================== --- papers/FDL2012/framework.tex (revision 95) +++ papers/FDL2012/framework.tex (revision 101) @@ -1,5 +1,5 @@ The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall -description of our methodology is shown in figure \ref{cegar}. +description of our methodology is shown in Figure \ref{cegar}. 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 @@ -211,5 +211,5 @@ \end{itemize} \vspace*{-2mm} -By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than +By Property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than $\widehat{M}_i$ and by the property of parallel composition, Index: papers/FDL2012/introduction.tex =================================================================== --- papers/FDL2012/introduction.tex (revision 95) +++ papers/FDL2012/introduction.tex (revision 101) @@ -1,3 +1,3 @@ -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. +The 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. @@ -28,8 +28,8 @@ - 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}. + 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}. -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}. +In \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}. %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. @@ -51,5 +51,5 @@ %\subsection{Contribution} -\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. +\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. Index: papers/FDL2012/myBib.bib =================================================================== --- papers/FDL2012/myBib.bib (revision 95) +++ papers/FDL2012/myBib.bib (revision 101) @@ -10,8 +10,7 @@ @ARTICLE{clarke94model, - author = {E.M.~Clarke and O.~Grumberg and D.E.~Long}, - title = {{Model Checking and Abstraction}}, + author = {E. M.~Clarke and O.~Grumberg and D.E.~Long}, + title = {Model Checking and Abstraction}, journal = {ACM Transactions on Programming Languages and Systems}, - year = {1994}, volume = {16}, pages = {1512--1542}, @@ -21,6 +20,9 @@ issn = {0164-0925}, keywords = {model cheking, abstraction, CTL, preservation}, - publisher = {ACM Press} -} + publisher = {ACM Press}, + year = {1994} +} + + @PHDTHESIS{braunstein_phd07, author = {C.~Braunstein}, @@ -28,7 +30,7 @@ Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur Puce"}, - school = {{Universitée Pierre et Marie Curie (Paris 6)}}, + school = {Université Pierre et Marie Curie}, year = {2007}, - address = {LIP6/SOC}, + address = {LIP6-SOC}, owner = {cecile}, timestamp = {2007.04.16} @@ -46,11 +48,11 @@ @conference{ ClarkeEmerson81temporal_logic, author = "E. M. Clarke and E. A. Emerson", - title = "Design and systhesis of synchronization skeletons using branching time temporal logic", - booktitle = "In Logic of Programs Workshop", + title = "Design and systhesis of synchronization skeletons using branching time temporal logic", + booktitle = "Logic of Programs Workshop", volume = 131, address = "Yorktown Heights, New York", - year = 1981, month = May, - publisher = "LNCS 131, Springer " + publisher = "LNCS 131, Springer", + year = 1981 } @@ -62,6 +64,5 @@ number = 2, pages = {244-263}, - year = 1986, - month = Apr + year = 1986 } @@ -69,8 +70,8 @@ author = "E. M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith", title = "{Counterexample-guided Abstraction Refinement}", - booktitle = "Computer Aided Verification (CAV '00)", + booktitle = "CAV'00", address = "Chicago, IL", - year = 2000, - publisher = "LNCS" + publisher = "LNCS", + year = 2000 } @@ -78,10 +79,10 @@ author = "J. P. Queille and J. Sifakis", title = "Specification and verification of concurrent systems in CESAR", - booktitle = "In Proceedings of the 5th International Symposium on Programming", + booktitle = "Proceedings of the 5th International Symposium on Programming", volume = 137, address = "Turin, Italy", - year = 1982, month = April, - publisher = "LNCS 137, Springer " + publisher = "LNCS 137, Springer", + year = 1982 } @@ -90,9 +91,9 @@ @conference{ BCCFZ04SMC_with_SAT, author = "A. Biere and A. Cimatti and E. Clarke and M.Fujita and Y. Zhu", - title = "{ Symbolic Model Checking using SAT procedures instead of BDDs}", + title = "{Symbolic Model Checking using SAT procedures instead of BDDs}", booktitle = {Proceedings: Design Automation Conference (DAC '99)}, pages = {317-320}, - year = 1999, month = February, + year = 1999 } @@ -101,7 +102,6 @@ author = "The VIS Group", title = "{VIS: A system for Verification and Synthesis}", - journal = {Springer Lecture Notes in Computer Science}, + journal = {Springer LNCS}, volume = 1102, - number = 1102, pages = {428-432}, year = 1996 @@ -114,7 +114,7 @@ booktitle = {16th Conference on Computer Aided Verification (CAV '04)}, pages = {519-522}, - year = 2004, month = Jul, - publisher = "LNCS 3114" + publisher = "LNCS 3114", + year = 2004 } @@ -154,10 +154,10 @@ author = "C. Roux and E. Encrenaz ", title = "{CTL} may be ambigous when model-checking {Moore Machines} ", - booktitle = " IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)", + booktitle = "IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)", volume = 2860, address = "Italy", - year = 2003, month = Nov, - publisher = "LNCS" + publisher = "LNCS", + year = 2003 } @@ -166,9 +166,9 @@ author = "F. Xie and J.C. Browne ", title = "{Verified Systems by Composition from Verified Components} ", - booktitle = " In ESEC/FSE 2003: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference", + booktitle = "ESEC/FSE 2003: 11th ACM SIGSOFT Symposium on Foundations of Software Eng. Conf.", pages = {227-286}, - address = "Helsinki, Finland", - year = 2003, - publisher = "ACM Press" + address = "Finland", + publisher = "ACM Press", + year = 2003 } @@ -177,9 +177,9 @@ author = "J. Li and X. Sun and F. Xie and X. Song", title = "{Component-Based Abstraction Refinement} ", - booktitle = "In Proc. of 10th International Conference on Software Reuse (ICSR)", + booktitle = "10th Int. Conf. on Software Reuse (ICSR)", pages = {39-51}, - address = "Beijing, China", - year = 2008, - publisher = "Springer-Verlag" + address = "China", + publisher = "Springer-Verlag", + year = 2008 } @@ -189,9 +189,9 @@ author = "H. Peng and Y. Mokhtari and S. Tahar ", title = "{Environment Synthesis for Compositional Model Checking} ", - booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design", + booktitle = "ICCD’02: 20th Int. Conference on Computer Design", pages = {70-75}, address = "Freiburg, Germany", - year = 2002, - publisher = "IEEE Computer Society" + publisher = "IEEE Computer Society", + year = 2002 } @@ -200,5 +200,5 @@ author = "M. Schickel and V. Nimbler and M. Braun and H. Eveking ", title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ", - booktitle = "In FDL’06: Proceedings of Forum on specification and Design Languages", + booktitle = "FDL’06: Forum on specification and Design Languages", year = 2006 } @@ -207,21 +207,21 @@ @conference{ CiardoLS00mdd_async, author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu", - title = "{ Efficient symbolic state-space construction for asynchronous systems} ", - booktitle = "In Proc. of ICATPN '2000", + title = "{Efficient symbolic state-space construction for asynchronous systems} ", + booktitle = "Proc. of ICATPN '2000", volume = 1825, pages = {103-122}, - year = 2000, - publisher = "LNCS, Springer Verlag" + publisher = "LNCS, Springer Verlag", + year = 2000 } @conference{ CTM05hdd, author = "J-M. Couvreur and Y. Thierry-Mieg", - title = "{ Hierarchical Decision Diagrams to Exploit Model Structure} ", - booktitle = "In FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems", + title = "{Hierarchical Decision Diagrams to Exploit Model Structure} ", + booktitle = "FORTE: 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems", volume = 3731, pages = {443-457}, address = "Taipei, Taiwan", - year = 2005, - publisher = "LNCS, Springer" + publisher = "LNCS, Springer", + year = 2005 } @@ -229,32 +229,32 @@ @conference{ HQR98assume_guarantee, author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani", - title = "{ You Assume, We Guarantee : Methodology and Case Studies} ", - booktitle = "CAV’98: Proceedings of the 10th Int. Conference on Computer Aided Verification", + title = "{You Assume, We Guarantee: Methodology and Case Studies} ", + booktitle = "CAV’98", volume = 1427, pages = {440-451}, - address = "Vancouver, Canada", - year = 1998, - publisher = " LNCS, Springer-Verlag" + address = "Canada", + publisher = "Springer-Verlag", + year = 1998 } @conference{ GrumbergLong91assume_guarantee, - author = " O. Grumberg and D. E. Long", - title = "{ Model Checking and Modular Verification} ", - booktitle = " In International Conference on Concurency Theory", + author = "O. Grumberg and D. E. Long", + title = "{Model Checking and Modular Verification}", + booktitle = "Int. Conference on Concurency Theory", volume = 527, pages = {250-263}, - year = 1991, - publisher = " LNCS, Springer-Verlag" + publisher = "Springer-Verlag", + year = 1991 } @conference{ GrafSaidi97abstract_construct, - author = " S. Graf and H. Saïdi", - title = "{ Construction of Abstract State Graphs with PVS} ", - booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification", + author = "S. Graf and H. Saïdi", + title = "{Construction of Abstract State Graphs with PVS}", + booktitle = "Computer Aided Verification (CAV’97)", volume = 1254, - year = 1997, - publisher = " LNCS, Springer" + publisher = "LNCS, Springer", + year = 1997 } @@ -262,11 +262,11 @@ @conference{ PardoHachtel97autoAbsMC, - author = " S. Pardo and G. Hachtel", - title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ", - booktitle = " In CAV ’97", + author = "S. Pardo and G. Hachtel", + title = "{Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ", + booktitle = "CAV’97", volume = 1254, pages = {12-23}, - year = 1997, - publisher = " LNCS, Springer-Verlag" + publisher = "Springer-Verlag", + year = 1997 } @@ -274,8 +274,8 @@ @conference{ PardoHachtel98incremCTLMC, author = " S. Pardo and G. Hachtel", - title = "{ Incremental CTL Model Checking Using BDD Subsetting} ", - booktitle = " In DAC ’98: 35th Design Automation Conference ", + title = "{Incremental CTL Model Checking Using BDD Subsetting} ", + booktitle = "DAC ’98: 35th Design Automation Conference ", pages = {457-462}, - year = 1998, + year = 1998 } @@ -283,77 +283,77 @@ @conference{ Burch_al91smc_part_transition, author = " J. R. Burch and E. M. Clarke and D. E. Long", - title = "{ Symbolic Model Checking with Partitioned Transition Relations} ", + title = "{Symbolic Model Checking with Partitioned Transition Relations} ", booktitle = "Proceedings of the 1991 International Conference on VLSI", pages = {49-58}, month = August, - year = 1991, + year = 1991 } @conference{ Burch_al93smc_circuit_verif, - author = " J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli", - title = "{ Symbolic Model Checking for Sequential Circuit Verification} ", - booktitle = " IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems", + author = "J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli", + title = "{Symbolic Model Checking for Sequential Circuit Verification} ", + booktitle = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems", volume = {13(4)}, pages = {401-424}, - year = 1993, + year = 1993 } @conference{ Kroening_al07vcegar, - author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke", - title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ", - booktitle = " In TACAS '07 ", - year = 2007, + author = " H. Jain and D. Kroening and N. Sharygina and E. Clarke", + title = "{VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ", + booktitle = "TACAS'07 ", + year = 2007 } @ARTICLE { Sharygina_al12PreciseApprox, - AUTHOR = { Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich }, - TITLE = { {An Abstraction Refinement Approach Combining Precise and Approximated Techniques} }, - JOURNAL = { International Journal on Software Tools for Technology Transfer (STTT) }, + AUTHOR = {N. Sharygina and S. Tonetta and A. Tsitovich}, + TITLE = {An Abstraction Refinement Approach Combining Precise and Approximated Techniques}, + JOURNAL = {International Journal on Software Tools for Technology Transfer}, VOLUME = {14}, PAGES ={1-14}, - YEAR = { 2012}, + YEAR = {2012} } @conference{ microsoft04SLAM, - author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani", - title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ", - booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)", + author = "T. Ball and B. Cook and V. Levin and S. K. Rajamani", + title = "{SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ", + booktitle = "4th Int. Conf. on Integrated Formal Methods", volume = 2999, pages = {1-20}, - year = 2004, - publisher = " LNCS, Springer" + publisher = "Springer", + year = 2004 } @conference{ berkeley07BLAST, - author = " Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar", - title = "{ The Software Model Checker Blast: Applications to software engineering.} ", - booktitle = " International Journal on Software Tools for Technology Transfer", + author = "D. Beyer and T. A. Henzinger and R. Jhala and R. Majumdar", + title = "{The Software Model Checker Blast: Applications to software engineering} ", + booktitle = "Int. Journal on Software Tools for Technology Transfer", volume = {9 (5-6)}, pages = {505-525}, - year = 2007, + year = 2007 } @inproceedings{pwk2009-date, - AUTHOR = { Mitra Purandare and Thomas Wahl and Daniel Kroening }, - TITLE = { Strengthening Properties using Abstraction Refinement }, - BOOKTITLE = { Proceedings of DATE 2009 }, - YEAR = { 2009 }, - PUBLISHER = { ACM }, - PAGES = { 1692-1697 }, + AUTHOR = {M. Purandare and T. Wahl and D. Kroening}, + TITLE = {Strengthening Properties using Abstraction Refinement}, + BOOKTITLE = {Proceedings of DATE 2009}, + PUBLISHER = {ACM}, + PAGES = {1692-1697}, + YEAR = {2009} } @conference{ Kunz_al11ipc_abs, - author = " Minh D. Nguyen and Markus Wedler and Dominik Stoffel and Wolfgang Kunz ", - title = "{ Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}", - booktitle = "48th Proc. Design Automation Conference (DAC '11)", + author = "M. D. Nguyen and M. Wedler and D. Stoffel and W. Kunz ", + title = "{Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}", + booktitle = "Design Automation Conference (DAC'11)", address = "San Diego, USA", - year = 2011, + year = 2011 } @@ -363,6 +363,5 @@ publisher = "Addison-Wesley", title = "The {\TeX}book", - year = 1984, - isbn = "" + year = 1984 } Index: papers/FDL2012/ordering_filter_properties.tex =================================================================== --- papers/FDL2012/ordering_filter_properties.tex (revision 95) +++ papers/FDL2012/ordering_filter_properties.tex (revision 101) @@ -1,3 +1,3 @@ - We propose an + We propose a heuristic to order the properties depending on the structure of each component. @@ -35,10 +35,10 @@ Note that a variable may belong to more than one dependency graph, in that case we consider the minimum depth. -\item Give a weight to each variable (see algorithm \ref{algo:weight}). -\item Compute the weight of properties for each component~: sum of the +\item Give a weight to each variable (see Algorithm \ref{algo:weight}). +\item Compute the weight of properties for each component: sum of the property variables weight. \end{enumerate} -The algorithm \ref{algo:weight} gives weight according to the variable distance to the +The Algorithm \ref{algo:weight} gives weight according to the variable distance to the primary variable with extra weight for interface variable and primary variable. @@ -250,5 +250,5 @@ property holds then the property will not eliminate the counterexample. Hence this property is not a good candidate for refinement. -Therefore the highest weighted property not satisfied in $K(\sigma)$ is choosen to be +Therefore the highest weighted property not satisfied in $K(\sigma)$ is chosen to be integrated in the next refinement step. This process is iterated for each refinement step. @@ -274,6 +274,5 @@ $AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$ otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS -definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate -$\sigma$. +definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate $\sigma$. \end{enumerate} \end{proof} @@ -281,6 +280,6 @@ \vspace*{-2mm} The proposed approach ensures that the refinement excludes the counterexample -and respects the definition \ref{def:goodrefinement}. -We will show in our experiments that first the time needed to build an AKS is +and respects the Definition \ref{def:goodrefinement}. +We will show in our experiments that first, the time needed to build an AKS is negligible and secondly the refinement converges rapidly. %The property at the top of the list (not yet selected and excluding the properties