Loading...
Please wait, while we are loading the content...
Similar Documents
A simple method for extracting models from protocol code (2001)
| Content Provider | CiteSeerX |
|---|---|
| Author | Lie, David Dill, David L. Engler, Dawson Chou, Andy |
| Description | in Proceedings of the 28th Annual International Symposium on Computer Architecture In Proceedings of the 28th Annual International Symposium on Computer Architecture IN PROCEEDINGS OF THE 28TH ANNUAL INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE |
| Abstract | The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used despite its advantages. In this paper, we present a method for automatically extracting models from low level software implementations. Our method is based on the use of an extensible compiler system, xg++, to perform the extraction. The extracted model is combined with a model of the hardware, a description of correctness, and an initial state. The whole model is then checked with the Mur ยข model checker. As a case study, we apply our method to the cache coherence protocols of the Stanford FLASH multiprocessor. Our system has a number of advantages. First, it reduces the cost of creating models, which allows model checking to be used more frequently. Second, it increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation. We found a total of 8 errors using our system. Two errors were global resource errors, which would be difficult to find through any other means. We feel the approach is applicable to other low level systems. 1 |
| File Format | |
| Publisher Date | 2001-01-01 |
| Access Restriction | Open |
| Subject Keyword | Global Resource Error Mur Model Checker Stanford Flash Multiprocessor Underlying System Protocol Code Low Level System Underlying Implementation Cache Coherence Protocol Extensible Compiler System Whole Model Extracted Model Low Level Software Implementation |
| Content Type | Text |
| Resource Type | Proceeding Conference Proceedings |
