![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
- Timestamp:
- Apr 4, 2012, 2:01:08 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 3 edited
-
FDL2012.tex (modified) (1 diff)
-
exp_results.tex (modified) (6 diffs)
-
introduction.tex (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.tex
r75 r80 47 47 48 48 \begin{abstract} 49 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 .49 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}. 50 50 \end{abstract} 51 51 -
papers/FDL2012/exp_results.tex
r75 r80 1 We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our test platforms requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process. 1 We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. There several abstraction-refinement techniques implemented in VIS accessible via \emph{approximate\_model\_check}, \emph{iterative\_model\_check}, \emph{check\_invariant} and \emph{incremental\_ctl\_model\_check} commands. However, among the techniques available, \emph{incremental\_ctl\_model\_check} is the only abstraction-refinement technique that supports CTL formulas and fairness constraints which are necessary in our test platforms. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. 2 2 3 3 4 We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes on a CAN bus. Table \ref{StatsVCI_PI} and Table \ref{StatsCAN_Bus} give the size and the statistics concerning the VCI-PI platform and CAN bus platform respectively. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory. 4 5 6 5 7 \begin{table*} [ht] 6 \hspace*{1 0mm}7 \begin{tabular}{clcccc c}8 \hspace*{17mm} 9 \begin{tabular}{clcccc} 8 10 9 11 \toprule 10 \multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{ FSM} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\11 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Depth}& \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\12 \multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 13 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 12 14 \midrule 13 15 \midrule 14 & 1 Master-1 Slave & 308 & 599& 33 442 & 3.64116e+06 & 41.49 \\15 Concrete & 2 Masters-1 Slave & 4 39 & 186 & 75 210 & 7.3282e+04 & 14.36\\16 Model & 4 Masters-1 Slave & 7 09 & 408 & 156 657 & 2.15076e+07 & 414.38\\17 & 4 Masters-2 Slaves & 883 & 597 & 217 797 & 3.22215e+10 & 4064.09\\16 & 1 Master-1 Slave & 308 & 33 442 & 3.64116e+06 & 41.49 \\ 17 Concrete & 2 Masters-1 Slave & 453 & 140297 & 2.42518e+11 & 1922.75 \\ 18 Model & 4 Masters-1 Slave & 737 & N/A & N/A & >3days \\ 19 & 4 Masters-2 Slaves & 911 & N/A & N/A & >3days \\ 18 20 \midrule 19 21 \midrule 20 Final & 1 Master-1 Slave & 197 & 2& 76 & 5.03316e+07 & 0.01 \\21 Abstract & 2 Masters-1 Slave & 301 & 2& 99 & 4.12317e+11 & 0.02 \\22 Model & 4 Masters-1 Slave & 501 & 2& 147 & 3.45876e+18 & 0.03\\23 for $\phi_1$ & 4 Masters-2 Slaves & 589 & 2& 167 & 7.08355e+21 & 0.04 \\22 Final & 1 Master-1 Slave & 197 & 76 & 5.03316e+07 & 0.01 \\ 23 Abstract & 2 Masters-1 Slave & 301 & 99 & 4.12317e+11 & 0.02 \\ 24 Model & 4 Masters-1 Slave & 501 & 147 & 3.45876e+18 & 0.03\\ 25 for $\phi_1$ & 4 Masters-2 Slaves & 589 & 167 & 7.08355e+21 & 0.04 \\ 24 26 \midrule 25 Final & 1 Master-1 Slave & 194 & 1& 50 & 2.62144e+07 & 0 \\26 Abstract & 2 Masters-1 Slave & 298 & 1& 73 & 2.14748e+11 & 0.01 \\27 Model & 4 Masters-1 Slave & 498 & 1& 121 & 1.80144e+18 & 0.02 \\28 for $\phi_2$ & 4 Masters-2 Slaves & 586 & 1& 141 & 3.68935e+21 & 0.02 \\27 Final & 1 Master-1 Slave & 194 & 50 & 2.62144e+07 & 0 \\ 28 Abstract & 2 Masters-1 Slave & 298 & 73 & 2.14748e+11 & 0.01 \\ 29 Model & 4 Masters-1 Slave & 498 & 121 & 1.80144e+18 & 0.02 \\ 30 for $\phi_2$ & 4 Masters-2 Slaves & 586 & 141 & 3.68935e+21 & 0.02 \\ 29 31 \bottomrule 30 32 \bottomrule … … 36 38 37 39 40 38 41 \begin{table*} [ht] 39 \hspace*{1 2mm}40 \begin{tabular}{ccccc c}42 \hspace*{15mm} 43 \begin{tabular}{ccccc} 41 44 42 45 \toprule 43 \textbf{CAN Bus} & \emph{Number of} & \emph{FSM}& \emph{BDD} & \emph{Number of } & \emph{Analysis}\\44 \textbf{Platform} &\emph{BDD Variables} & \emph{Depth}& \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\46 \textbf{CAN Bus} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 47 \textbf{Platform} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 45 48 \midrule 46 49 \midrule 47 Concrete Model & 838 & 182 & 212550 & 2.87296e+08 & 167.9\\50 Concrete Model & 822 & 140586 & 3.7354e+07 & 294.6 \\ 48 51 \midrule 49 52 \midrule 50 Final Abstract Model for $\phi_1$ & xx & 2 & xxx & xxx & xxxx\\53 Final Abstract Model for $\phi_1$ & 425 & 187 & 1.66005e+12 & 0.03 \\ 51 54 \midrule 52 Final Abstract Model for $\phi_2$ & xx & 2 & xxx & xxx & xxxx\\55 Final Abstract Model for $\phi_2$ & 425 & 187 & 1.66005e+12 & 0.04 \\ 53 56 \bottomrule 54 57 \bottomrule … … 57 60 \caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform} 58 61 \end{table*} 62 63 59 64 60 65 … … 80 85 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 81 86 & Prop. Selection & 1 & 2.0 \\ 82 $\phi_1$ & Incremental & 0 & 1.3\\83 & Standard MC & - & 1.5\\87 $\phi_1$ & Incremental & 0 & 107.7 \\ 88 & Standard MC & - & 1181.8 \\ 84 89 \midrule 85 90 & Prop. Selection & 0 & 1.0 \\ 86 $\phi_2$ & Incremental & 0 & 15.3\\87 & Standard MC & - & 14.6\\91 $\phi_2$ & Incremental & 0 & 108.5 \\ 92 & Standard MC & - & 1103.3 \\ 88 93 \midrule 89 94 \midrule 90 95 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 91 96 & Prop. Selection & 1 & 2.1 \\ 92 $\phi_1$ & Incremental & 0 & 6.8\\93 & Standard MC & - & 175.5\\97 $\phi_1$ & Incremental & N/A & >3 days \\ 98 & Standard MC & - & >3 days \\ 94 99 \midrule 95 100 & Prop. Selection & 0 & 1.0 \\ 96 $\phi_2$ & Incremental & 0 & 7.5\\97 & Standard MC & - & 195.1\\101 $\phi_2$ & Incremental & N/A & >3 days \\ 102 & Standard MC & - & >3 days \\ 98 103 \midrule 99 104 \midrule 100 105 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 101 106 & Prop. Selection & 1 & 2.2 \\ 102 $\phi_1$ & Incremental & N/A & > 1 day\\103 & Standard MC & - & 2231.3\\107 $\phi_1$ & Incremental & N/A & >3 days \\ 108 & Standard MC & - & >3 days \\ 104 109 \midrule 105 110 & Prop. Selection & 0 & 1.1\\ 106 $\phi_2$ & Incremental & N/A & > 1 day\\107 & Standard MC & - & 12814.1\\111 $\phi_2$ & Incremental & N/A & >3 days \\ 112 & Standard MC & - & >3 days\\ 108 113 \bottomrule 109 114 \bottomrule … … 126 131 \midrule 127 132 \midrule 128 & Prop. Selection & xxx & xxx\\129 $\phi_3$ & Incremental & N/A & >1 day\\130 & Standard MC & - & 51.9\\133 & Prop. Selection & 0 & 1.02 \\ 134 $\phi_3$ & Incremental & N/A & N/A \\ 135 & Standard MC & - & N/A \\ 131 136 \midrule 132 & Prop. Selection & xxx & xxx\\133 $\phi_4$ & Incremental & 0 & 57.3\\134 & Standard MC & - & 2.2\\137 & Prop. Selection & 0 & 1.01\\ 138 $\phi_4$ & Incremental & N/A & N/A \\ 139 & Standard MC & - & N/A \\ 135 140 \bottomrule 136 141 … … 142 147 143 148 144 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), incremental\_ctl\_verification (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\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)))$ whereas for the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)) -> AF((s = 1)*(r = 1))$ and $\phi_4 = AG(((p'=1)*(q'=1)) -> AG(r' = 0))$. 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 the more connected components, in contrary to the other two methods, our computation time remains stable. 149 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), incremental\_ctl\_verification (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\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 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. 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. 150 151 152 In the case of the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)*AF(r_1=1)) -> AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) -> AG((s_2=0)*(t_2=0)))$. We have at our disposal 103 verified component properties and after the selection process, 3 selected component properties were sufficient to verify both global properties. 153 154 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 the more connected components, in contrary to the other two methods, our computation time remains stable. 145 155 146 156 -
papers/FDL2012/introduction.tex
r78 r80 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. Generally failures on these systems are unacceptable and have to be avoided.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. 2 2 3 3 … … 10 10 11 11 %\subsection{Related Works} 12 \emph{Related Works:} 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 wasproposed 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.12 A strategy to overcome the state explosion problem is by performing abstraction. A method for the construction of an abstract state graph of an arbitrary system automatically was first 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. 13 13 14 14 15 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.15 In 2000, 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. 16 16 17 17 18 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}. 18 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}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive. 19 19 20 20 21 The compositionalstrategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, it is shown 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 this is 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.21 An alternative method to get over the state explosion problem is the compositional strategy. The 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, it is shown 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 this is 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. 22 22 23 23 24 25 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 have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. 24 \textbf{\emph{Related Works:}} 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 have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. 26 25 27 26 … … 41 40 42 41 %\subsection{Contribution} 43 \ emph{Contribution :} We would like to contribute to 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. 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.42 \textbf{\emph{Contribution :}} We would like to contribute to 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. 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. 44 43 45 44 In the next section, we will give an overview of our framework and introduce the notations that will be used later. The rest of the paper is organized as follows: section 3 details our strategy of refinement. Section 4 presents the experimentation results and finally, section 5 draws the conclusions and summarize our possible future works.
Note: See TracChangeset
for help on using the changeset viewer.
