Loading...
Please wait, while we are loading the content...
Similar Documents
A New Scheme for Memory-eecient Probabilistic Veriication a New Scheme for Memory-eecient Probabilistic Veriication
| Content Provider | Semantic Scholar |
|---|---|
| Author | Dill, David L. |
| Copyright Year | 1996 |
| Abstract | In veri cation by explicit state enumeration, for each reachable state of the protocol being veri ed the full state descriptor is stored in a state table. Two probabilistic methods { bitstate hashing and hash compaction { have been proposed in the literature that store much fewer bits for each state but come at the price of some probability that not all reachable states will be explored during the search, and that the veri er may thus produce false positives. Holzmann introduced bitstate hashing and derived an approximation formula for the average probability that a particular state is not omitted during the search, but this formula does not give a bound on the probability of false positives. In contrast, the analysis for hash compaction, introduced by Wolper and Leroy and improved upon by Stern and Dill, yielded a bound on the probability that not even one state is omitted during the search, thus providing a bound on the probability of false positives. In this paper, we propose and analyze a new scheme for probabilistic veri cation that is a variation of the improved hash compaction scheme. The main di erence is that a tighter bound on the probability of false positives is calculated by reasoning about a longest path in the breadthrst search tree of the reachable state space. In addition, the new scheme employs ordered hashing to reduce the omission probability when inserting into the state table. In the industrial protocols we examined, the new scheme yielded an exponential reduction in the bound on the probability of false positives, which enabled a roughly 50% reduction in the number of bits needed for a compressed state. Furthermore, we propose a memory e cient way to store the information needed for error trace generation. The outcomes of experiments using the new scheme con rmed the analysis. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://sprout.stanford.edu/PAPERS/SD96A.ps |
| Alternate Webpage(s) | http://verify.stanford.edu/PAPERS/SD96A.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
